Skip to content

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.