Implementations
If you don’t know which FTS model checker to use, take SNIP; it’s the most elaborate and easy to use.
Overview
Here is an overview and side-by-side comparison of the tools we produced so far.
| Haskell library | NuSMV extension | SNIP | |
|---|---|---|---|
| First release | September 2009 | January 2010 | November 2010 |
| Development status | Abandoned | Stable | Stable & maintained |
| Modelling language | FTS | fSMV | fPromela |
| – style | Automata, expressed as Haskell data structures | Declarative, boolean transition relation is specified directly | Procedural, very intuitive |
| – features | Annotative | Aspectual | Annotative |
| – feature models | No | No | Yes, using TVL |
| Logic | LTL | CTL | LTL |
| Algorithm | Explicit | Symbolic | Semi-symbolic, on-the-fly |
| Platform | Haskell (Hugs or GHC) | NuSMV (C++) | C |
SNIP, the definitive FTS implementation
SNIP is a model checker for FTS that we implemented from scratch. The focus for SNIP was usability and intuitive modelling. Its specification language is based on Promela, from the well known SPIN model checker. Properties can be expressed in LTL or as never claims. Features used in a model have to be declared in a feature diagram, for which the TVL language is used. SNIP is not just a prototype; it is meant to be usable by third parties.
NuSMV extension for symbolic CTL model checking
This 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. This tool implementes the fCTL model checking algorithms of our ICSE 2011 paper.
Haskell library
This was our first prototype FTS implementation. The tool is a library for the functional programming language Haskell. It implements the LTL model checking algorithms of the ICSE 2010 paper. It has been superseded by SNIP.