Symbolic Reachability Analysis of B through ProB and LTSmin

J. Bendisposto, P. Körner, M Leuschel, Jeroen Meijer, Jan Cornelis van de Pol, H. Treharne, J. Whitefield

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

    6 Citations (Scopus)
    99 Downloads (Pure)

    Abstract

    We present a symbolic reachability analysis approach for B that can provide a significant speedup over traditional explicit state model checking. The symbolic analysis is implemented by linking ProB to LTSmin, a high-performance language independent model checker. The link is achieved via LTSmin ’s Pins interface, allowing ProB to benefit from LTSmin ’s analysis algorithms, while only writing a few hundred lines of glue-code, along with a bridge between ProB and C using ØMQ. ProB supports model checking of several formal specification languages such as B, Event-B, Z and TLA+TLA+. Our experiments are based on a wide variety of B-Method and Event-B models to demonstrate the efficiency of the new link. Among the tested categories are state space generation and deadlock detection; but action detection and invariant checking are also feasible in principle. In many cases we observe speedups of several orders of magnitude. We also compare the results with other approaches for improving model checking, such as partial order reduction or symmetry reduction. We thus provide a new scalable, symbolic analysis algorithm for the B-Method and Event-B, along with a platform to integrate other model checking improvements via LTSmin in the future.
    Original languageEnglish
    Title of host publicationIntegrated Formal Methods
    Subtitle of host publication12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings
    EditorsE. Ábrahám, Marieke Huisman
    Place of PublicationCham
    PublisherSpringer
    Pages275-291
    Number of pages16
    ISBN (Print)978-3-319-33692-3
    DOIs
    Publication statusPublished - Jun 2016
    Event12th International Conference on integrated Formal Methods 2016 - Reykjavik Iceland, Reykjavik, Iceland
    Duration: 1 Jun 20165 Jun 2016
    Conference number: 12

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer International Publishing
    Volume9681
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference12th International Conference on integrated Formal Methods 2016
    Abbreviated titleiFM 2016
    CountryIceland
    CityReykjavik
    Period1/06/165/06/16

    Keywords

    • LTSMIN
    • Symbolic reachability
    • ProB
    • METIS-318458
    • B-Method
    • Event-B
    • IR-100722
    • EWI-27071

    Fingerprint Dive into the research topics of 'Symbolic Reachability Analysis of B through ProB and LTSmin'. Together they form a unique fingerprint.

    Cite this