C3+ATO Function Simulation and Verification Analysis Based on Timed Automata

C3+ATO system plays an important role in controlling train operation and its function is related to the safety of train automatic operation. A simulation and verification method based on timed automata is proposed to verify the function of high-speed railway C3+ATO system. The functional requirements in the C3+ATO system specification are extracted and the timed automata models are established and then the timed automata network model is formed. The message sequence charts are generated and system safety, reachability, existence are verified. As a result, the models meet the functional requirements of the system which provide theoretical reference for the subsequent C3+ATO system design and development, test and measurement, practical application and related specification improvement.

Research on the Structure of Authentication Protocol Analysis Based on MSCs/Promela

To discover the existing or possibly existing vulnerability of present authentication protocol, we proposed a structure of authentication protocol analysis, which consist of white box analysis, black box analysis and indicator system as the three main functional components. White box analysis makes use of the transformation from MSCs (Message Sequence Charts) to Promela (Process Meta Language), the input language of the remarkable model checker SPIN; black box analysis is based on the attack platform of authentication protocol analysis; indicator system is decided by deducibility restraint methods. Compared with the UML modeling methods based on Promela, the MSC2Promela methods we figured out on the context have more advantages than its disadvantages. Finally, we proposed a structure of authentication protocol analysis based on the transformation from MSC2Promela, which makes sense to the later work on the area of authentication protocol analysis.