SpinS: Extending LTSmin with Promela through SpinJa

Freark van der Berg, Freark Iwert van der Berg, Alfons Laarman

  • 7 Citations

Abstract

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.
Original languageUndefined
Title of host publication11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012
EditorsK. Heljanko, W.J. Knottenbelt
Place of PublicationAmsterdam
PublisherOpen Publishing Association
Pages95-105
Number of pages8
DOIs
StatePublished - 17 Sep 2012
Event11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 - London, United Kingdom

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
Volume296
ISSN (Print)1571-0661
ISSN (Electronic)2075-2180

Workshop

Workshop11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012
Abbreviated titlePDMC
CountryUnited Kingdom
CityLondon
Period17/09/1217/09/12
Internet address

Fingerprint

Model checking
Inspection
Experiments
Modeling languages

Keywords

  • METIS-287929
  • FMT-MC: MODEL CHECKING
  • EWI-22042
  • IR-80839

Cite this

van der Berg, F., van der Berg, F. I., & Laarman, A. (2012). SpinS: Extending LTSmin with Promela through SpinJa. In K. Heljanko, & W. J. Knottenbelt (Eds.), 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 (pp. 95-105). (Electronic Notes in Theoretical Computer Science; Vol. 296). Amsterdam: Open Publishing Association. DOI: 10.1016/j.entcs.2013.07.007

van der Berg, Freark; van der Berg, Freark Iwert; Laarman, Alfons / SpinS: Extending LTSmin with Promela through SpinJa.

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: Scientific - peer-reviewConference contribution

@inbook{caf7e661c54b415e8592980071351ec5,
title = "SpinS: Extending LTSmin with Promela through SpinJa",
abstract = "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.",
keywords = "METIS-287929, FMT-MC: MODEL CHECKING, EWI-22042, IR-80839",
author = "{van der Berg}, Freark and {van der Berg}, {Freark Iwert} and Alfons Laarman",
year = "2012",
month = "9",
doi = "10.1016/j.entcs.2013.07.007",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Open Publishing Association",
pages = "95--105",
editor = "K. Heljanko and W.J. Knottenbelt",
booktitle = "11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012",

}

van der Berg, F, van der Berg, FI & Laarman, A 2012, SpinS: Extending LTSmin with Promela through SpinJa. in K Heljanko & WJ Knottenbelt (eds), 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012. Electronic Notes in Theoretical Computer Science, vol. 296, Open Publishing Association, Amsterdam, pp. 95-105, 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012, London, United Kingdom, 17-17 September. DOI: 10.1016/j.entcs.2013.07.007

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: Scientific - peer-reviewConference contribution

TY - CHAP

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

PB - Open Publishing Association

ER -

van der Berg F, van der Berg FI, Laarman A. SpinS: Extending LTSmin with Promela through SpinJa. In Heljanko K, Knottenbelt WJ, editors, 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012. Amsterdam: Open Publishing Association. 2012. p. 95-105. (Electronic Notes in Theoretical Computer Science). Available from, DOI: 10.1016/j.entcs.2013.07.007