-
Notifications
You must be signed in to change notification settings - Fork 4
/
README.html
225 lines (186 loc) · 7.62 KB
/
README.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
<!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>