SpinS: Extending LTSmin with Promela through SpinJa

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    8 Citations (Scopus)
    151 Downloads (Pure)

    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
    Publication statusPublished - 17 Sep 2012
    Event11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012 - London, United Kingdom
    Duration: 17 Sep 201217 Sep 2012
    Conference number: 11
    http://anna.fi.muni.cz/PDMC/PDMC12/

    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

    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. https://doi.org/10.1016/j.entcs.2013.07.007