State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin

Philipp Körner, Michael Leuschel, Jeroen Meijer

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

    2 Citations (Scopus)
    41 Downloads (Pure)

    Abstract

    In previous work, we presented symbolic reachability analysis by linking ProB, an animator and model checker for B and Event-B, and LTSmin, a language-independent model checker offering state-of-the-art model checking algorithms. Although the results seemed very promising, it was a very basic integration of these tools and much potential of LTSmin was not covered by the implementation.

    In this paper, we present a much more mature version of this tool integration. In particular, explicit-state model checking, efficient verification of state invariants, model checking of LTL properties, as well as partial order reduction and proper multi-core model checking are now available. The (improved) performance of this advanced tool link is benchmarked on a series of models with various sizes and compared to ProB.
    Original languageEnglish
    Title of host publicationIntegrated Formal Methods
    Subtitle of host publication14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings
    EditorsCarlo A. Furia, Kirsten Winter
    PublisherSpringer
    Pages275-295
    Number of pages21
    ISBN (Electronic)978-3-319-98938-9
    ISBN (Print)978-3-319-98937-2
    DOIs
    Publication statusPublished - Sep 2018
    Event14th International Conference on Integrated Formal Methods, IFM 2018 - Maynooth University, Maynooth, Ireland
    Duration: 5 Sep 20187 Sep 2018
    https://ifm2018.cs.nuim.ie/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume11023

    Conference

    Conference14th International Conference on Integrated Formal Methods, IFM 2018
    Abbreviated titleIFM 2018
    CountryIreland
    CityMaynooth
    Period5/09/187/09/18
    Internet address

    Fingerprint Dive into the research topics of 'State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin'. Together they form a unique fingerprint.

  • Cite this

    Körner, P., Leuschel, M., & Meijer, J. (2018). State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin. In C. A. Furia, & K. Winter (Eds.), Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings (pp. 275-295). (Lecture Notes in Computer Science; Vol. 11023). Springer. https://doi.org/10.1007/978-3-319-98938-9_16