English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

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.

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