<meta http-equiv="content-type" content="text/html; charset=iso-8859-1">
<meta name="author" content="Theo Ruys">
<meta name="keywords" content="SpinS, model checking, Promela, SPIN">
<meta name="description" content="readme documentation for SpinS">
<title>SpinS - README.html documentation</title>

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).

All of these techniques should work nicely together with Promela semantics on assertion violations, deadlocks, never claims and valid end states. Note that some combinations, like POR and never claims, require some alternative approaches for now. The LTL formula can for example be loaded directly in LTSmin.

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

The spins folder contains the following 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

SpinS does not yet support the full Promela language.
Currently, the following aspects of Promela are not yet implemented:

• 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

SpinS is released under the Apache 2.0 license.

People

SpinS was developed by:

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

SpinJa was developed by:

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

Further Reading

For general documentation on Promela and the model checker SPIN, please consult the SPIN website, which hosts a wealth of information on the subjects.

More specific information on the design and implementation of SpinS can be found in the following two MSc theses.

• 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

1.0	2013.02.05	Release in LTSmin 2.0 (renamed to SpinS)
0.9.9	2012.02.22	Some improvements to SpinS
0.9	2011.06.23	First public release of SpinS within LTSmin 1.7 (called SpinJa).