The Security Analysis Of Rail Transport Operations Scenarios Based On Model Checking

The rail transit train contrlo system is extremely strict to real-time.To guarantee the security of rail transport operations, you need for the systematic security checking that orient to operational scenarios, while ensure the security system requires not only behavior meet security requirements,but also its reachable behavior meet the corresponding safety time constraints.Model checking technology is an effective technology of system security checking,its principle is build system behavior that use automaton model,and use temporal logic to represent the properties that needed to verify,then use checking algorithm to check whether this model meet the properties.Reachability analysis algorithm is the foundation of model checking. State space explosion is accelerated due to the time constraints of timed automata, therefore, the complexity of reachability analysis algorithm has increased. The existing timed automata reachability analysis methods can be divided into two types:the first type is the state space traversal algorithm based on equivalent time region map or difference bounded matrices (DBM) using a semi-symbol time constraints structure; the other is a state space traversal method based on BDD structure using full-symbol time constraints. Unfortunately, both types of methods split the symbol correlation of state transition expression and time constraints expression, therefore they are difficult to be applied into a large case study.The main work in this paper is:1) Use the common checking tool------UPPAAL to check the function security and time contraints security of typical rail transport operational scenarios,so that can be achieve the security analysis of system model.2) Propose a full-symbolic reachability analysis method,state transition space of timed automata and time constraints are represented under the same BDD structure,and give the operation series algorithm of time constraints on the basis of the reachable state full-symbolic operation,and give the reachability analysis algorithm of single automata and product automata.Finally,an example is used to verify the correctness of the algorithm.In this way,we can implement the full-symbolic reachability analysis of timed automata,and provide the analysis basis of full-symbolic time system model checking.