Skip to content

PimW/spins

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

505 Commits
doc
doc
 
 
lib
lib
 
 
src
src
 
 
tests
tests
 
 
.gitignore
.gitignore
 
 
README.html
README.html
 
 
spins.sh
spins.sh
 
 

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

Readme
Activity

Stars

0 stars

Watchers

2 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages

  • Java 35.1%
  • Other 33.1%
  • Perl 10.8%
  • Propeller Spin 9.7%
  • TeX 6.0%
  • C 1.9%
  • Other 3.4%