An Research for Formal Verification of Safety-Critical Software

DOI

10.2991/iccasm.2012.212How to use a DOI?

Keywords

SafetyCritical Software, FSM, LTL, UML

Abstract

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.

Copyright

© 2012, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Weigang Ma
AU  - Xinhong Hei
PY  - 2012/08
DA  - 2012/08
TI  - An Research for Formal Verification of Safety-Critical Software
BT  - Proceedings of the 2012 International Conference on Computer Application and System Modeling (ICCASM 2012)
PB  - Atlantis Press
SP  - 836
EP  - 839
SN  - 1951-6851
UR  - https://doi.org/10.2991/iccasm.2012.212
DO  - 10.2991/iccasm.2012.212
ID  - Ma2012/08
ER  -