Research On UML Modeling And Model Checking Of CTCS-3 Train Control System

CTCS-3 Train Control System is a system which is based on GSM-R wareless transmission system for delivering bidirectional safe control information,and is a very important component part of China Train Control System(CTCS).In order for the localization of the passenger dedicated line Train Control System,It is necessary to investigate the technical specification and key technology of CTCS-3 Train Control System of passenger dedicated line,forming the technical system of China high speed passenger dedicated line Train Control System.Modeling is a very important method and prerequisite in system design.First, model must be easy for designer to understand and use.Secondly,model need to reflect the system requirements correctly. Safety of the model of Train Control System is also a issue need to pay attention to.UML is a universal visual modeling lauguage, It is suited for teamwork design as it is easy to understand and master. However,UML doesn't offer a method to check the correctness of the model itself.Thus,UML model need to be checked by other means. Symbolic Model Checking is a very significant method of formal verification.It is widely used,with high speed and runs automatically.The thesis use Symbolic Model Checking to check the UML model.After checking the UML model,SMV model of the system is obtained.The thesis then carry out some safety analysis of the SMV model by using fault injection.First,The thesis analyse the level switch scene of CTCS-3 Train Control System,Then build the UML model to get UML class diagram and UML state diagram.UML class diagram is expanded to include the input and out event which express the interaction of the components of the system.UML state diagram represent that the state of object tranfer to another state on the trigger of input event and the object generate output event.Before checking the UML model,The UML model need to be tranlated to SMV model.A Class in UML class diagram correspond to a SMV module of the SMV model.And state transfer of the object of the class is represented by the update of the state variable in SMV module.The thesis establish general rules of the translation.In Symbolic Model Checking,System property is expressed by Computation Tree Logic.The Symbolic Model verifier make the SMV model and system property as its input,then the system property such as reachability and liveness can be checked.If the result of the checking is True,the system satisfy the property,otherwise error exist in the SMV model or UML model.The counterexample can be analyzed to find the error.After the SMV model satisfy all the system property,fault can be injected into the model.The safety property can also be expressed by CTL formula,then the safety property can be checked.The structure function of the fault tree is a boolean function,the truth table of the boolean function can be obtained by using Symbolic Model verifier.Finally a fault tree can be constructed.