A Verification Method for Software Safety Requirement by Combining Model Checking and FTA

DOI

10.2991/iiicec-15.2015.301How to use a DOI?

Keywords

Model Checking; Software Safety; Formal Method; Fault Tree Analysis

Abstract

Formal verification for safety-critical software requirements is used to improve the safety of software system. Model checking precisely verifies the related properties of software system, but there still exist limitations in properties extraction which is traditionally obtained by artificial definition. In this paper, a combined technology of model checking and FTA (Fault Tree Analysis) is applied to the software safety requirements verification, mainly to solve the problem of properties extraction in model checking. First the software system model is described in finite state machine (FSM). Second the safety properties are achieved by combining FTA and Computational Tree Logic (CTL) of model checking. Next the open source tool of model checker NuSMV is applied to implement the verification of software safety requirements. Finally this methodology is illustrated with an application to an ABP (Alternating Bit Protocol) instance. The application results can show the effectiveness of the method.

Copyright

© 2015, 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  - Congcong Chen
AU  - Fuping Zeng
AU  - Minyan Lu
PY  - 2015/03
DA  - 2015/03
TI  - A Verification Method for Software Safety Requirement by Combining Model Checking and FTA
BT  - Proceedings of the 2015 International Industrial Informatics and Computer Engineering Conference
PB  - Atlantis Press
SP  - 1359
EP  - 1364
SN  - 2352-538X
UR  - https://doi.org/10.2991/iiicec-15.2015.301
DO  - 10.2991/iiicec-15.2015.301
ID  - Chen2015/03
ER  -