Abstract
| Original language | Undefined |
|---|---|
| Title of host publication | 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 |
| Editors | K. Heljanko, W.J. Knottenbelt |
| Place of Publication | Amsterdam |
| Publisher | Open Publishing Association |
| Pages | 95-105 |
| Number of pages | 8 |
| DOIs | |
| Publication status | Published - 17 Sep 2012 |
| Event | 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 - London, United Kingdom Duration: 17 Sep 2012 → 17 Sep 2012 Conference number: 11 http://anna.fi.muni.cz/PDMC/PDMC12/ |
Publication series
| Name | Electronic Notes in Theoretical Computer Science |
|---|---|
| Publisher | Elsevier |
| Volume | 296 |
| ISSN (Print) | 1571-0661 |
| ISSN (Electronic) | 2075-2180 |
Workshop
| Workshop | 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 |
|---|---|
| Abbreviated title | PDMC |
| Country | United Kingdom |
| City | London |
| Period | 17/09/12 → 17/09/12 |
| Internet address |
Keywords
- METIS-287929
- FMT-MC: MODEL CHECKING
- EWI-22042
- IR-80839
Cite this
}
SpinS: Extending LTSmin with Promela through SpinJa. / van der Berg, Freark; van der Berg, Freark Iwert; Laarman, Alfons.
11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012. ed. / K. Heljanko; W.J. Knottenbelt. Amsterdam : Open Publishing Association, 2012. p. 95-105 (Electronic Notes in Theoretical Computer Science; Vol. 296).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
TY - GEN
T1 - SpinS: Extending LTSmin with Promela through SpinJa
AU - van der Berg, Freark
AU - van der Berg, Freark Iwert
AU - Laarman, Alfons
PY - 2012/9/17
Y1 - 2012/9/17
N2 - We show how PROMELA can be supported by the high-performance generic model checking tools of LTSMIN. The success of the SPIN model checker has made PROMELA an important modeling language. SPINJA was created as a Java implementation of SPIN, in an effort to make the model checker easily extendible and reusable while maintaining some of its efficiency. While these goals where certainly met, the downside of SPINJA remained its dependability on Java, degrading performance with a factor 5 and obstructing support for embedded C code in PROMELA models. LTSMIN aims at language-independence through the definition of the generic PINS interface. The toolset has shown that a generic model checker can indeed be competitive in terms of efficiency by supporting several languages from different paradigms and implementing many analysis algorithms that compete with other state-of-the-art model checkers. We extended SPINJA to emit C code that implements the PINS interface. We also improved PROMELA support in SPINJA, greatly extending the support of models beyond toy and academic examples. In this paper, we demonstrate the usage of LTSMIN’s analysis algorithms: multi-core model checking of assertion violations, deadlocks and never claims (full LTL), inspection of error trails, partial order reduction, state compression, symbolic reachability and distributed reachability. Our experiments show that the performance of these methods beats other leading model checkers.
AB - We show how PROMELA can be supported by the high-performance generic model checking tools of LTSMIN. The success of the SPIN model checker has made PROMELA an important modeling language. SPINJA was created as a Java implementation of SPIN, in an effort to make the model checker easily extendible and reusable while maintaining some of its efficiency. While these goals where certainly met, the downside of SPINJA remained its dependability on Java, degrading performance with a factor 5 and obstructing support for embedded C code in PROMELA models. LTSMIN aims at language-independence through the definition of the generic PINS interface. The toolset has shown that a generic model checker can indeed be competitive in terms of efficiency by supporting several languages from different paradigms and implementing many analysis algorithms that compete with other state-of-the-art model checkers. We extended SPINJA to emit C code that implements the PINS interface. We also improved PROMELA support in SPINJA, greatly extending the support of models beyond toy and academic examples. In this paper, we demonstrate the usage of LTSMIN’s analysis algorithms: multi-core model checking of assertion violations, deadlocks and never claims (full LTL), inspection of error trails, partial order reduction, state compression, symbolic reachability and distributed reachability. Our experiments show that the performance of these methods beats other leading model checkers.
KW - METIS-287929
KW - FMT-MC: MODEL CHECKING
KW - EWI-22042
KW - IR-80839
U2 - 10.1016/j.entcs.2013.07.007
DO - 10.1016/j.entcs.2013.07.007
M3 - Conference contribution
T3 - Electronic Notes in Theoretical Computer Science
SP - 95
EP - 105
BT - 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012
A2 - Heljanko, K.
A2 - Knottenbelt, W.J.
PB - Open Publishing Association
CY - Amsterdam
ER -