Warning: this page and the FSAP tool are no longer maintained
Please visit the xSAP Web Page
The Formal Safety Analysis Platform


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).

FSAP screenshot

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 main features of the FSAP are:



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:

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.