SpinS

For the LTSmin toolset, we extended SpinJa to generate C code adhering to the PINS interface. The otiginal SpinJa code generated Java from Promela models. Since the resulting tool is incompatible with other parts of SpinJa, we renamed the tool to SpinS.

Additionally, SpinS was extended with a great many new features available in the Promela language. To give a quick overview:

• An advanced preprocessor, crucial to handle many case studies
• Custom type structs
• Remote refs
• Channel actions and expressions (random, rendez-vous, polling)
• d_step options and communication
• Atomicity with loss of atomicity
• Special variables: _pid only

The result is that we are now able to handle many large case studies with LTSmin. But more significantly, the semantics models is so close that the state counts, error counts and transition counts are equal to those of SPIN for many of these large case studies. An overview is given by the scripts in the test directory.

Moreover, due to the functionality of the PINS interface, we are able to add a rich set of analysis algorithms to the PROMELA world. These are available as the generic, but efficient tools of LTSmin, and include:

• Semi-symbolic reachability and CTL model checking with reordering, saturation and chaining (paper).
• Scalable multi-core reachability (paper) and LTL model checking algorithms (paper) with leading explicit state compression techniques (paper).
• Guard-based partial order reduction, competitive to SPINs ample set approach (paper).

Most of these features are described in SpinS: Extending LTSmin with Promela through SpinJa. The original SpinJa documentation can be found at: http://code.google.com/p/spinja/.

Files

• README.html: this file
• spins.jar: SpinS compiler
• spins.sh: SpinS compiler shell script
• tests/: directory with Promela examples and test scripts
• lib/: additional Java library: the JavaCC compiler generator
• src/: complete Java source of SpinS
• doc/: Documentation, licence and generated Java doc

Compilation

Should be handled by LTSmin compilation scripts.

Known issues

Promela

• unless statement
• communication: sorted send (!!)
• special variables: np_ and pc_value
• Channel references, e.g. channel references in channels.

The following things we would like to (and are able to) add in the future:

• Promela's C code extensions (e.g., c_code, c_expr)
• Type structs in channels
• Timeouts

License

People

• Alfons Laarman: Extension of Promela capabilities and implementation of PINS POR matrices
• Freark van der Berg: original adaptation of SpinJa to PINS

• Marc de Jonge: principal designer of SpinJa 0.8.
• Theo Ruys: supervisor of SpinJa project.

Further Reading

• Freark van der Berg and Alfons Laarman.
  SpinS: Extending LTSmin with Promela through SpinJa.
  PDMC 2012.
  This paper describes SpinS: the adaptation of SpinJa to LTSmin.


• Marc de Jonge.
  The SpinJ Model Checker - A fast, extensible, object-oriented model checker.
  MSc Thesis, University of Twente, The Netherlands, September 2008.
  This MSc thesis describes the design and implementation of SpinS 0.8 in detail.


• Mark Kattenbelt.
  Towards an Explicit-State Model Checking Framework.
  MSc Thesis, University of Twente, The Netherlands, September 2006.
  This MSc this presents a layered, object-oriented design for explicit-state model checkers. SpinS's design is based on this approach.

Version history