-
Notifications
You must be signed in to change notification settings - Fork 4
utwente-fmt/spins
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> <html> <head> <style type="text/css"> body {font-family: "lucida grande", lucida, verdana, sans-serif;} body {margin: 20px 50px 0px 50px;} body {background: #f5f5f5;} body {line-height: 140%;} a, a:link, a:visited {text-decoration: none; color: #0082ae;} a:hover {border-color: #0082ae; border-width: 0 0 1px 0; border-style: solid;} h1, h2, h3 {color: #A00; padding-top:15px;} h1, h2 {border-bottom: 2px solid #a1a5a9; padding-bottom: 6px;} h3 {font-style:italic; font-size:100%;} code, pre {font-size: 110%;} table {border-collapse: collapse; } td {border:1px solid #a1a5a9; padding:10px; font-size: 90%; vertical-align: top;} span.lastchanged {color: #AAA; font-size: 20%;} </style> <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> </head> <body> <h1>SpinS</h1> <p> For the <a href="http://fmt.cs.utwente.nl/tools/ltsmin/">LTSmin</a> toolset, we extended SpinJa to generate C code adhering to the <a href="http://eprints.eemcs.utwente.nl/15703/">PINS interface</a>. 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. <p/> <p> Additionally, SpinS was extended with a great many new features available in the <a href="http://spinroot.com/spin/Man/grammar.html">Promela</a> language. To give a quick overview: <ul> <li>An advanced preprocessor, crucial to handle many case studies</li> <li>Custom type structs</li> <li>Remote refs</li> <li>Channel actions and expressions (random, rendez-vous, polling)</li> <li>d_step options and communication</li> <li>Atomicity with loss of atomicity</li> <li>Special variables: _pid only</li> </ul> </p> <p> 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. </p> <p> 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: <ul> <li>Semi-symbolic reachability and CTL model checking with reordering, saturation and chaining (<a href="http://eprints.eemcs.utwente.nl/15703/">paper</a>).</li> <li>Scalable multi-core reachability (<a href="http://www.foldr.org/~michaelw/papers/fmcad-2010-shared-hash.pdf">paper</a>) and LTL model checking algorithms (<a href="http://fmt.cs.utwente.nl/tools/ltsmin/papers/atva-2011-mcndfs.pdf">paper</a>) with leading explicit state compression techniques (<a href="http://fmt.cs.utwente.nl/tools/ltsmin/papers/spin-2011-tree-compression.pdf">paper</a>).</li> <li>Guard-based partial order reduction, competitive to SPINs ample set approach (<a href="http://essay.utwente.nl/61036/1/MSc_E_Pater.pdf">paper</a>).</li> </ul> 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. </p> <p> Most of these features are described in <a href="http://eprints.eemcs.utwente.nl/22042/"> SpinS: Extending LTSmin with Promela through SpinJa</a>. The original SpinJa documentation can be found at: <a href="http://code.google.com/p/spinja/">http://code.google.com/p/spinja/</a>. </p> <h2>Files</h2> The spins folder contains the following files: <ul> <li><code>README.html</code>: this file</li> <li><code>spins.jar</code>: SpinS compiler</li> <li><code>spins.sh</code>: SpinS compiler shell script</li> <li><code>tests/</code>: directory with Promela examples and test scripts</li> <li><code>lib/</code>: additional Java library: the <a href="https://javacc.dev.java.net/">JavaCC</a> compiler generator</li> <li><code>src/</code>: complete Java source of SpinS</li> <li><code>doc/</code>: Documentation, licence and generated Java doc</li> </ul> <h2>Compilation</h2> <p> Should be handled by LTSmin compilation scripts. </p> <h2>Known issues</h2> <h3>Promela</h3> SpinS does not yet support the full Promela language. <br> Currently, the following aspects of Promela are <em>not</em> yet implemented: <ul> <li><code>unless</code> statement</li> <li>communication: sorted send (<code>!!</code>)</li> <li>special variables: <code>np_</code> and <code>pc_value</code></li> <li>Channel references, e.g. channel references in channels.</li> </ul> <p> The following things we would like to (and are able to) add in the future: <ul> <li>Promela's C code extensions (e.g., <code>c_code</code>, <code>c_expr</code>)</li> <li>Type structs in channels</li> <li>Timeouts</li> </ul> </p> <h2>License</h2> SpinS is released under the <a href="http://www.apache.org/licenses/LICENSE-2.0.html"> Apache 2.0 license</a>. <h2>People</h2> SpinS was developed by: <ul> <li>Alfons Laarman: Extension of Promela capabilities and implementation of PINS POR matrices</li> <li>Freark van der Berg: original adaptation of SpinJa to PINS</li> </ul> SpinJa was developed by: <ul> <li>Marc de Jonge: principal designer of SpinJa 0.8.</li> <li>Theo Ruys: supervisor of SpinJa project.</li> </ul> <h2>Further Reading</h2> For general documentation on Promela and the model checker SPIN, please consult the <a href="spinroot.com">SPIN</a> 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. <ul> <li> Freark van der Berg and Alfons Laarman.<br> <a href="http://eprints.eemcs.utwente.nl/22042/"> SpinS: Extending LTSmin with Promela through SpinJa</a>.<br> PDMC 2012.<br> <em>This paper describes SpinS: the adaptation of SpinJa to LTSmin.</em> </li><br> <li> Marc de Jonge.<br> <a href="http://fmt.cs.utwente.nl/msc-completed/jonge-msc-thesis.pdf"> The SpinJ Model Checker - A fast, extensible, object-oriented model checker</a>.<br> MSc Thesis, University of Twente, The Netherlands, September 2008.<br> <em>This MSc thesis describes the design and implementation of SpinS 0.8 in detail.</em> </li><br> <li>Mark Kattenbelt.<br> <a href="http://fmt.cs.utwente.nl/msc-completed/kattenbelt-msc-thesis.pdf"> Towards an Explicit-State Model Checking Framework</a>.<br> MSc Thesis, University of Twente, The Netherlands, September 2006.<br> <em>This MSc this presents a layered, object-oriented design for explicit-state model checkers. SpinS's design is based on this approach.</em> </li> </ul> <h2>Version history</h2> <table> <tr><td>1.0</td> <td>2013.02.05</td> <td>Release in LTSmin 2.0 (renamed to SpinS)</td> </tr> <tr><td>0.9.9</td> <td>2012.02.22</td> <td>Some improvements to SpinS</td> </tr> <tr><td>0.9</td> <td>2011.06.23</td> <td>First public release of SpinS within LTSmin 1.7 (called SpinJa).</td> </tr> </table> </body> </html>
About
No description, website, or topics provided.
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published