Modeling And Verification Of Computer Based Interlocking System Based On SCADE

CBI (Computer based Interlocking) system aimed to achieve a goal of safety is an important part of railway signal system,which requires a high safety requirement for any failure may cause casualties and properties loss. The traditional development of CBI mainly depends on manual coding,and the software quality is ensured manually through methods such as code walkthrough, preview and testing. Due to the subjectivity of these methods, this development fails to fulfill the safety requirements of CBI.Formal modeling is emerged as a promising method of safety critical system development,which has advantages of modeling precisely and reasoning automatically for its rigorous mathematical basis. SCADE is a safety critical software development environment based on formal modeling, which can describe software function clearly and completely, using the Safe State Machine and Data Flow Diagram methods provided; combining visual simulation and formal verification, the subjectivity of developers is avoided largely; after ensuring the correctness and safety of models, the project-oriented C code can be generated automatically.In this paper, the CBI software development method based on SCADE is studied. The methods of SCADE such as requirement management, formal modeling, visual simulation,formal verification are taken to ensure the correctness and safety of CBI, including:(1) SCADE software development mode is introduced, and the requirement management,modeling methods based on Safe State Machine and Data Flow Diagram, simulation, formal verification and code generation are analyzed in detail.(2) The basic structure, characteristics and software functionalities of CBI are analyzed;based on the system requirements, the route control process is divided into six stages of route selection, route locking, signals open and keep opening, normal unlock and manual unlock,and the modeling requirements of every stage are concluded.(3) Based on SSM and Data Flow Diagram, the formal models of CBI are established.(4) To ensure the CBI models have completely covered the system requirements and design requirements, using SCADE requirement management method, the traceability among the system requirements, design requirements and CBI models is analyzed.(5) After checking the correctness of CBI models by visual simulation, the safety properties are modeled, based on which, formal verification are performed; then the project-oriented C code is generated through code generator.