A Scalable Approach to Detecting Safety Requirements Inconsistencies for Railway Systems
- 9 July 2024
- journal article
- research article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Intelligent Transportation Systems
- Vol. 25 (8) , 8375-8386
Abstract
Dealing with the ever-growing complexity of railway systems requires scalable approaches for detecting inconsistent safety requirements in practice. Despite significant efforts to automate the requirements consistency detection, current inconsistency analysis techniques of railway safety requirements still suffer from scalability issues. This paper proposes a two-layer approach for detecting inconsistencies in time-related safety requirements of railway systems, integrating two distinct formal methods from a pragmatic perspective. At the SafeNL layer, we employ an SMT-based approach to extract conflict patterns and use them to filter out inconsistent requirements descriptions, thus avoiding the more expensive general use of the SMT-based approach. At the CCSL layer, temporal dependencies in requirements are transformed into causal relations, which are then detected for circular inconsistencies using a graph search technique. Our evaluations demonstrate the utility and scalability of our approach.Keywords
Funding Information
- National Natural Science Foundation of China (62192731, 62272166, 62192730)
This publication has 26 references indexed in Scilit:
- Formally verifying consistency of sequence diagrams for safety critical systemsScience of Computer Programming, 2022
- Automating Consistency Verification of Safety Requirements for Railway Interlocking Systems2019
- Scalable Analysis of Real-Time Requirements2019
- SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language2019
- Consistency of Property Specification Patterns with Boolean and Constrained Numerical Signals2018
- Requirements Capture and Analysis in ASSERT(TM)2017
- SpeAR v2.0: Formalized Past LTL Specification and Analysis of Requirements2017
- Fast, flexible MUS enumerationConstraints, 2015
- Easy Approach to Requirements Syntax (EARS)2009
- Clock constraint specification language: specifying clock constraints with UML/MARTEInnovations in Systems and Software Engineering, 2008