Skip to content

SNIP

SNIP is a model checker for FTS that we implemented from scratch. The focus for SNIP is 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.

Reference

The definitive paper on SNIP was published in volume 14 number 5 of the International Journal on Software Tools for Technology Transfer (STTT), September 2009. Most questions about SNIP (from tool usage to architecture) should be answered in this paper.

Download & Installation

SNIP is distributed in source code form, licensed under GPL. It compiles and runs on Linux and Mac OS X; we haven’t tested it under Windows yet.

To instal, unzip the archive, cd into src and execute the build.sh file. This will build SNIP and all its dependencies (minisat, cudd and ltl2ba). If everything goes well, an executable file snip will have been created. Launching snip without any arguments will print the command-line usage instructions.

Features

The main features of SNIP are:

  • Intuitive specification language based on Promela (backward-compatible, covering most constructs of Promela)
  • Integrated with TVL, a feature modelling language: constraints between features can be specified in TVL and are taken into account by the model checking algorithms in SNIP
  • Other feature modelling languages can be plugged in easily
  • Support for C preprocessor directives
  • Model checking of LTL (more generally, omega-regular) properties using the explicit-state FTS algorithm from our ICSE’10 paper
  • Assertion checking (using the FTS algorithm)
  • Deadlock checking (using the FTS algorithm)
  • Exhaustive checking of the above, meaning search continues after a violation was found (with several optimisations)

Quick introduction

SNIP is a model checker for software product lines.  The approach that we have taken for the specification language is very close to what is arguably a very common method for implementing product lines: conditional statements (be it if(feature) or #ifdef feature).  To be able to use some features, e.g. “Foo” and “Bar”, inside the model, they have to be declared as follows:

// Declare list of features inside the special type "features"
typedef features {
bool Foo;
bool Bar
};
// Declare an instance of this type
features f;

Now any statement inside the model can be guarded by features Foo and Bar using the new gd statement:

active proctype toto() {
int i = 0;
// Increment i only if feature Foo or feature Bar is selected.
gd :: f.Foo || f.Bar -> i++;
:: else -> skip;
dg;
// Test assertion
assert(i == 1);
}

The principal difference wrt. SPIN is that SNIP does not treat features as regular variables. If the above were executed with SPIN (with the gd replaced by an if), it would assume Foo and Bar to be Boolean variables with the fixed value false. SNIP instead considers all possible values (and value combinations) for Foo and Bar. It does this by interpreting the Promela model as an FTS instead of a regular transition system.

When you execute SNIP on the above example, it will claim that products without Foo and without Bar violate the assertion. It will also give an execution that ends with this assertion violation. In the command line, this looks as follows:

$ ./snip -check -fm ../examples/website-bad.tvl ../examples/website.pml
No never claim, checking only asserts and deadlocks..
Assertion at line 17 violated [explored 5 states, re-explored 0].
- Products by which it is violated (as feature expression):
(!Foo & !Bar)
 
- Stack trace:
features                       = /
toto                           @ NL13
toto.i                         = 0

features                       = (!Foo & !Bar)
toto                           @ NL14

features                       = (!Foo & !Bar)
toto                           @ NL17

In addition to the Promela specification, SNIP requires the features to be defined in a feature model. For instance, the feature model could be (in TVL):

root Website group oneOf {
Foo,
Bar
}

That is, either Foo or Bar has to be in each product. If SNIP is executed with this feature model, it will not report an assertion violation. Since the feature model requires that one of both features be present in each product, i will always be incremented, and no execution can violate the assertion:

$ ./snip -check -fm ../examples/website-good.tvl ../examples/website.pml
No never claim, checking only asserts and deadlocks..
No assertion violations or deadlocks found [explored 3 states, re-explored 0].

This and other examples are distributed with SNIP, and can be found in the examples folder. Every example consists of a .pml file (the fPromela specification), a .tvl file with the feature diagram and sometimes a file .out.txt with the command to be executed and the expected output.