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

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.