FSAP
The FSAP/NuSMV-SA platform aims at supporting the formal analysis and safety assessment of (complex) systems. The platform is based on a set of tools (including an extension of the NuSMV model checker) and is based on the concept of a repository. The repository contains the information necessary for the design and safety assessment of systems and is shared between the design engineer (the actor responsible for the design of the complex system) and the safety engineer (the actor responsible for performing safety analysis on the complex system).
The platform is designed to support different phases of the development and safety assessment process and to support different development and safety assessment practices. To achieve these goals, FSAP/NuSMV-SA provides a set of basic functions. These basic functions can be combined in different ways to perform complex tasks. The major benefits from the use of FSAP/NuSMV-SA are the following:
- The platform supports a tight integration between the design and the safety teams;
- The platform automates (some of) the activities related both to the verification and to the safety analysis of systems in a uniform environment;
- The use of the platform is compatible with an incremental development approach, based on iterative releases of the system model at different levels of detail.
The main features of the FSAP are:
- Support for SAT XML format
- Full support to GFML (Generic Failure Mode Library): failure modes can be defined in the GFML, used from FSAP, and automatically injected into the model.
- Full support to GSRL (Generic Safety Requirements Library): safety patterns can be defined in the GSRL, used from FSAP, and loaded at the user request.
- Analysis task manager
- Automatic model extension.
- Possibility of defining custom failures directly into the system model.
- Highlighting of changes: parts of the SAT that are changed appear in red.
- Quick search of Safety Requirements and Failure Modes.
- Integration with NuSMV-SA.
- Result Displayer, for accessing in an integrated way all the results of the analyses.
- Fault Tree Displayer, that reads files in Fault Tree Plus tabular format.
- Viewer of traces in tabular and graphical form (through GnuPlot).
- Data Dictionary
NuSMV-SA
NuSMV-SA is the model checking engine used by FSAP for Safety Analysis. NuSMV-SA is an extension of the symbolic model checker NuSMV. NuSMV provides different model checking capabilities, among them: check properties, in CTL (Computational tree logic) or LTL (Linear temporal logic); or invariant formula simulation. Also for some analyses the use of either the BDD or SAT-based model checking engine is available. NuSMV-SA expands on the strengths of NuSMV for the safety analysis domain.
The main features of NuSMV-SA are:
- Monotonic and non-monotonic fault tree construction
- Generation of traces for each minimal cut set of a fault tree
- Possibility of choosing different model checker engine: either BDD or SAT-based model checker
- Ordering analysis on minimal cut sets
- Construction of fault trees, generation of traces, ordering analysis, simulation, and verification of properties are integrated with FSAP
- Calculation of the probability for a Top Level Event of a Fault Tree given the probability of the basic events.
- All NuSMV2 commands available from textual interface
NuSMV-SA is run within FSAP and its output is integrated with FSAP in the Results Displayer. NuSMV-SA can also be run on the command-line, both interactively or in batch mode.