Research On Consistency Verification Of Safety Requirements For Railway Interlocking Systems

For safety-critical systems such as railway interlocking systems,ensuring the safety of the system is its most important task,and the quality of safety requirements is the top priority among them.Since safety requirements documents are usually written in natural language,it is difficult to accurately analyze them.However,many industrial safety standards strongly recommend the use of formal methods in safety-critical systems.Formal methods are based on a large number of complex mathematical knowledge,which hinders its direct use in the industry.In order to facilitate the use of formal methods by domain experts,this thesis proposes a safety requirements pattern language for railway interlocking systems,and based on the Clock Constraint Specification Language（CCSL）to provide formal semantics.An SMT-based consistency verification method for safety requirements is defined.The main work of this thesis includes:The safety requirements pattern language Safe NL is defined,consisting of its syntax and semantics.From the safety requirements documents,the basic components of the language,events and states are extracted,and 8 simple sentence patterns and2 combined sentence patterns are constructed according to the relationships between events and states.The grammer is implemented based on the framework Xtext.Events,states and the relations between are described as clock based relations,for providing a semantic interpretation of Safe NL.A clock based safety requirements inconsistency detection method is proposed.The transformations rules from Safe NL documents to CCSL constraints are defined,the definitions of global inconsistency and partial inconsistency are given,and based on the analysis tool of CCSL,My CCSL,verification methods are given for these two kinds of inconsistencies.A localization algorithm for the least inconsistent set of partial inconsistency is proposed.At last,to support our methods proposed,a requirements consistency verification platform Safe NLConsistency is implemented.Based on 8 actual case experiments,a benchmark for inconsistent safety requirements verification is defined.A series of method evaluations are carried out,which show the validity of our approach.