Design And Formal Validation Of Wayside Safety Computer In CBTC

With computers widely applying in the safety-critical systems, whether computers can safety, reliable, steady running became the focus of people. This situation urges more and more people start to study and design safety computer. The safety of a system must be fully concerned, for fear the disfigurement of design will be result in the hidden safety trouble existing in the system. According to the safety critical system development framework, applying the formal method to build the system model , analyze the safety of the system and validate the design of the system is necessary.ZC and DSU of CBTC system are the backgrounds of this paper, illustrating the safety computers used in ZC and DSU. Firstly we analyzed the requirements of safety computer in details. On the base , we confirmed the structure of safety computer and then designed the hardware and software scheduling strategy.The Colored Petri Nets (CPN) was brought in to build the model of safety computer platform basing on safety design idea in the design phase. The modeling method was introduced firstly, and then the hierarchical models of the safety computer were built based on the structure design. The model contains the top model and son models which are comprised of model of 'host' and 'standby' channel, model of single machine, model of FTSM, model of communicate controller, etc.On the basis of the models, the state space analysis and simulation analysis are applying in our model were studied. The dynamic characteristics and right logic of the FTSM model were validated by using the states spaces analysis. The performance analysis was carried out in the synchronization course of system by simulation method, and the average synchronization time parameter was obtained. It provided the guidance of system scheduling time parameter choice. With the help of the verification and analysis, the system design would be modified and consummated.