Skip to content

NuSMV extension

This prototype tool is based on the NuSMV model checker.   It performs symbolic CTL model checking of FTS specified with the fSMV language by Plath and Ryan.  The download does not contain NuSMV.

The tool is actually a tool chain consisting of:

  • A composition script written in PHP.  This script will parse and compose a base system with a feature.
  • A NuSMV preprocessing script written in PHP. This script basically adds (syntactic) universal quantification to the NuSMV input language. For instance, you can write[forall i=1..n]foobar%i% : boolean;[/forall]

    and the preprocessor will expand this for n = 4 into

    foobar1 : boolean;

    foobar2 : boolean;

    foobar3 : boolean;

    foobar4 : boolean;

    This script is a standalone script that is independent from our NuSMV FTS extension. But since quantifiers are used in some of the examples it is included in the distribution.

  • A patch for NuSMV.  The patch adds a new command line switch -fbdd to NuSMV.
  • For the NuSMV 2.4.3 version: A postprocessing script written in PHP.  This script takes the -fbdd output of NuSMV and pretty-prints it.  In the NuSMV 2.5.0 version, the pretty-printing is done by NuSMV itself.

The PHP scripts work on text and can be chained with pipes.  Their parameter signature is shown if they are executed without any parameters.  The composition script is also able to do normal composition as defined in the paper by Plath and Ryan.

More information about this is available in the paper and in the technical report.