Downloads :

Releases

How to use it :

• $ tar xvzf atomicSpin-DATE.tar.gz (DATE is the date of the release using the format YYMMDD)
• $ cd atomicSpin-DATE (DATE is the same as above)
• $ make
• edit the spinCheck.sh file and modify it in order to fit your configuration
• $ ./atomicSpin [file] (working examples are in the tests directory)
• for any help or comment please send email to : rousseau@cnam.fr

TODO :

• implement blocking statement exchange
• implement guard check

Known bugs :

• semi colon at end of a sequence not accepted

Related papers :

2008

• C. Pajault, J.-F Pradat-Peyre and P. Rousseau Adapting Petri Nets Reductions to Promela Specifications. submitted to FORTE'08. Tokyo, Japan, june 2008.

  Abstract : The interleaving of concurrent processes actions leads to the well-known combinatorial explosion problem. Petri nets theory provides some structural reductions to tackle this phenomenon by agglomerating sequences of transitions into a single atomic transition. These reductions are easily checkable and preserve deadlocks, Petri nets liveness and any LTL formula that does not observe the modified transitions. Furthermore, they can be combined with other kinds of reductions such as partial-order techniques to improve the efficiency of state space re-duction. We present in this paper an adaptation of these reductions for Promela specifications and propose simple rules to automatically infer atomic steps in the Promela model while preserving the checked property. We demonstrate on typical examples the efficiency of this approach and propose some perspectives of this work in the scope of software model checking.