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.
safety-critical software FSM DR1S LTL UML
Wei-gang Ma Xin-hong Hei
School of Computer Science and Engineering Xian University of Technology Xian, Shaanxi 710071, Chi School of Computer Science and Engineering Xian University of Technology Xian, Shaanxi 710071, Chi
国际会议
太原
英文
264-268
2010-10-22（万方平台首次上网日期，不代表论文的发表时间）