An approach for design and formal verification of safety-critical software

A modeling and verification methodology is presented for railway interlocking system which is regarded as a safety-critical system. The methodology utilizes UML (Unified Modeling Language) to model the function requirement and FSM (Finite State Machine) to verify the safety requirements of the specification. The device specifications of railway interlocking system are modeled with UML, and dynamic behaviors of the device and whole system are modeled with FSM, the safety specification is translated LTL (Linear Temporal Logic) and analyzed with NuSMV. We try to show the feasibility of improving the reliability and reducing revalidation efforts when designing and developing a decentralized railway signaling system.