Skip to content
Oct 5 11

Simulation in FTS

by acs

We just added a technical report exploring the notions of simulation and abstraction for FTS. You might want to check it out.

Jul 28 11

Update: snip-r753-20110728

by acs

A new version is available for download, the changes wrt. the previous are:

  • Added an alias for the if..fi statement: gd..dg, which stands for “guard”.  This is mainly to make models easier to understand.
  • Updated most of the example models.

Dowload here.

Jun 30 11

Update: snip-r752-20110630

by acs

A new version is available for download, the changes wrt. the previous are:

  • Fixed an error in the website.pml example (this was a modification done for a demo which slipped into the last release by accident).

Dowload here.

May 3 11

Talk at ICSE

by acs

For those coming to ICSE in Hawaii later this month: I (Andreas) will present our work on symbolic model checking for product lines on Thursday, May 26, 1:45PM, at the model checking session.

Mar 23 11

Update: snip-r727-20110323

by acs

A new version is available for download, the changes wrt. the previous are:

  • Added new command line parameter -ospin. It is similar to -spin, but statements whose guard evaluates to false are removed from the model before model checking. The input is thus interpreted as fPromela (not exactly as SPIN would do). This is normally more efficient than -spin.
  • Fixed some bugs related to assignment of channel variables to channel IDs.

Dowload here.

Mar 16 11

Update: snip-r722-20110316

by acs

A new version is available for download, the changes wrt. the previous are:

  • Added bitwise & bit shifting operators.
  • Lifted some restrictions related to the use of labels and gotos inside atomic blocks.
  • Fixed two bugs (one related to the -fdlc option, and one related to the timeout keyword).

Dowload here.

Feb 2 11

CRC of ICSE 2011 paper

by acs

We just submitted the camera ready copy of the ICSE 2011 paper. You can download it here. The abstract is:

We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics.

We recently proposed featured transition systems (FTS), a compact representation for SPL behaviour, and defined algorithms for model checking FTS against linear temporal properties. Although they showed to outperform individual system verifications, they still face a state explosion problem as they enumerate and visit system states one by one.

In this paper, we tackle this latter problem by using symbolic representations of the state space. This lead us to consider computation tree logic (CTL) which is supported by the industry-strength symbolic model checker NuSMV. We first lay the foundations for symbolic SPL model checking by defining a feature-oriented version of CTL and its dedicated algorithms. We then describe an implementation that adapts the NuSMV language and tool infrastructure. Finally, we propose theoretical and empirical evaluations of our results. The benchmarks show that for certain properties, our algorithm is over a hundred times faster than model checking each system with the standard algorithm.

Just to be clear, this paper is not related to SNIP; it revolves around symbolic model checking and the tool presented in the paper is a modified version of NuSMV.  SNIP, in contrast is a semi-symbolic model checker with an entirely different input language. A paper about SNIP is currently under revision.

Jan 21 11

Update: snip-r611-20110121

by acs

A new version is available for download, the changes wrt. the previous are:

  • Added a document that explains in detail the differences between SNIP/fPromela and SPIN/Promela.
  • Added two new examples: a subset of the CCSDS File Delivery Protocol (CFDP), and an elevator model.
  • Implemented an optimisation for atomic sequences.
  • Fixed a segmentation fault that occurred in very large models.
  • The generated parser sources are now distributed with the code, so you don’t need flex or bison to build SNIP.

Dowload here.

Jan 11 11

Update: snip-r552-20110111

by acs

A new version is available for download.  There are no new features, mostly fixes and improvements of the features introduced in snip-r549.  SNIP is now more than twice as fast on most properties.  In detail, the changes wrt. the previous are:

  • Revised the optimisation released in snip-r549, did some refactoring (prettier, more concise, more efficient).
  • Improved the handling of -fdlc deadlocks (broken in previous version).
  • Fixed a segfault in channel sends.
  • Updated the examples.

Dowload here.

Jan 7 11

Update: snip-r549-20110107

by acs

A new version is available for download, changes wrt. the previous are:

  • Implemented a major optimisation for the exhaustive search (statistics will follow).
  • Several enhancements in the printing of traces:
    • Added parameter -st: prints shorter traces by ignoring the states in which no variables change.
    • Added parameter -nt: does not print any traces, only information about the violating or satisfying products.
    • Full copies (not only the diffs) of the loop start state and of the final state are explicitly printed.
    • The location of the never claim is now printed as well.
  • Reformatted the usage instructions (should be clearer now) and removed the obsolete -v parameter.
  • Small optimisation in never claims: transitions leading to accept states are now always evaluated first.
  • Some bugfixes:
    • The  variable _last now works correctly.
    • Removed restriction that feature labels cannot be used in atomic blocks.
    • When detecting a deadlock in normal reachability checking, the trace would stop one short of the deadlock state; fixed that.

Dowload here.