An Research for Formal Verification of Safety-Critical Software
Weigang Ma, Xinhong Hei · 2012
A verification methodology is presented for railway interlocking system which is regarded as a safety-critical system.The methodology utilizes UML to model the function requirement and LTL to verify the safety requirements of the specification.The device specifications of railway interlocking system are modeled with UML, then translate into FSM.The safety specification is translated LTL 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.