Modeling And Analysis Method Of Railway Signal System Safety Critical Software

Railway signal system is a key technology for commanding and controlling the safety train operation,which improves the passing capacity of sections and stations.With the development of science and technology such as computer and infomation,many control logics have gradually shifted to software,and more and more important safety critical functions are gradually fulfilled by software,and the safety critical software has become an important part of railway signal system.As the structure of railway signal system is getting more and more complex and the degree of automation is getting higher and higher,the scale of railway signaling system safety critical software is becoming larger and larger,and the logic is becoming more and more complex.Operation interruption,even rear collision and derailment causing heavy casualties and property losses will happen when these softwares fail.The correctness and safety of railway signaling system safety critical software must be strictly analyzed and verified,whose risk should be controlled within an acceptable range.Formal modeling and analysis is an important way to verify the correctness and safety of software logic,and guide software design,development and risk analysis.EN 50128 strongly recommends formal methods for the safety critical software with SIL 3 and SIL 4.Many formal modeling and analysis methods,including time automata,UML Statecharts and petri network,have been widely used in software modeling and analysis fields.However,due to the complex logic of the software and high requirements for real-time and safety,the current formal methods can not be used to model the function logic,clock constraint,and risk of railway signal system safety critical software completely and systematically.Formal modeling and analysis methods are selected independently,and many formal models are established among the software activities such as safety analysis,requirements analysis,design and testing.Lacking systematic description of the software function logic,clock constraint and risk,it is easy to result in inconsistency between models,and cause developers in different stages cannot understand each other's model,bringing safety hazards into the software.Therefore,a formal modeling and analysis method,which can fully describe the function logic,clock constraint and risk characteristics,has a certain theoretical and practical significance for the development of railway signal system safety critical software.This dissertation aims at a formal modeling and analysis methods which can model and analyze function logic,clock constraint and risk of railway signal system safety critical software,and the main work is listed as below:(1)The requirement of formal modeling and analysis method of railway signal system safety critical software is analyzed,and SyncCharts is selected as a study basis,according to whose advantages of hierarchical,concurrency and priority preemption mechanism.(2)Focusing on the problem that SyncCharts fails to describe clock constraint,a clock element is introduced into the SyncCharts,and a timed SyncCharts method is proposed to meet the modeling requirements of function logic and clock constraint of railway signal system safety critical software,whose basic elements and structure are described by Z specification language.(3)Focusing on the problem that SyncCharts fails to describe risk,based on the timed SyncCharts,frequency and failure consequence severity elements are introduced to describe the transition frequency between the software functions and the consequence severity level when the software functions fail.The modeling method of risk timed SyncCharts is put forward for describing risk characteristic,whose definition,macro step mechanism and meta model are given,meeting the modeling requirements of function logic,clock constraint and risk of railway signal system safety critical software.(4)Focusing on the model checking of risk timed SyncCharts,a model transformation method from risk timed SyncCharts to UTA is proposed,realizing the model checking of risk timed SyncCharts through UTA model checking algorithm,and fulfilling the analysis of function logic and clock constraint.A model transformation method from risk timed SyncCharts to MDP is proposed,realizing the probabilistic model checking of risk timed SyncCharts through MDP probabilistic model checking algorithm,and fulfilling the analysis of probability and risk.(5)Aiming to verify the feasibility of risk timed SyncCharts for modeling and analyzing railway signal system safety critical software,the safety critical software of computer based interlocking switch module is taken as an example.First,the risk timed SyncCharts models of the function logic,clock constraint and risk of the software are established;then these models are transformed into UTA and MDP models;finally,the function logic,clock constraint and risk characteristic of the switch models are analyzed by model checking and probabilistic model checking respectively.