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

  • 2 Citations

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 International Publishing
Pages275-291
Number of pages16
ISBN (Print)978-3-319-33692-3
DOIs
StatePublished - Jun 2016
Event12th International Conference on integrated Formal Methods 2016 - Reykjavik, Iceland

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

Fingerprint

Model checking
Specification languages
Glues
Experiments

Keywords

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

Cite this

Bendisposto, J., Körner, P., Leuschel, M., Meijer, J., van de Pol, J. C., Treharne, H., & Whitefield, J. (2016). Symbolic Reachability Analysis of B through ProB and LTSmin. In E. Ábrahám, & M. Huisman (Eds.), Integrated Formal Methods: 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings (pp. 275-291). (Lecture Notes in Computer Science; Vol. 9681). Cham: Springer International Publishing. DOI: 10.1007/978-3-319-33693-0_18

Bendisposto, J.; Körner, P.; Leuschel, M; Meijer, Jeroen; van de Pol, Jan Cornelis; Treharne, H.; Whitefield, J. / Symbolic Reachability Analysis of B through ProB and LTSmin.

Integrated Formal Methods: 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. ed. / E. Ábrahám; Marieke Huisman. Cham : Springer International Publishing, 2016. p. 275-291 (Lecture Notes in Computer Science; Vol. 9681).

Research output: Scientific - peer-reviewConference contribution

@inbook{55db36b3bc3c4e5bbda5ed706a307c7d,
title = "Symbolic Reachability Analysis of B through ProB and LTSmin",
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.",
keywords = "LTSMIN, Symbolic reachability, ProB, METIS-318458, B-Method, Event-B, IR-100722, EWI-27071",
author = "J. Bendisposto and P. Körner and M Leuschel and Jeroen Meijer and {van de Pol}, {Jan Cornelis} and H. Treharne and J. Whitefield",
year = "2016",
month = "6",
doi = "10.1007/978-3-319-33693-0_18",
isbn = "978-3-319-33692-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
pages = "275--291",
editor = "E. Ábrahám and Marieke Huisman",
booktitle = "Integrated Formal Methods",

}

Bendisposto, J, Körner, P, Leuschel, M, Meijer, J, van de Pol, JC, Treharne, H & Whitefield, J 2016, Symbolic Reachability Analysis of B through ProB and LTSmin. in E Ábrahám & M Huisman (eds), Integrated Formal Methods: 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9681, Springer International Publishing, Cham, pp. 275-291, 12th International Conference on integrated Formal Methods 2016, Reykjavik, Iceland, 1-5 June. DOI: 10.1007/978-3-319-33693-0_18

Symbolic Reachability Analysis of B through ProB and LTSmin. / Bendisposto, J.; Körner, P.; Leuschel, M; Meijer, Jeroen; van de Pol, Jan Cornelis; Treharne, H.; Whitefield, J.

Integrated Formal Methods: 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. ed. / E. Ábrahám; Marieke Huisman. Cham : Springer International Publishing, 2016. p. 275-291 (Lecture Notes in Computer Science; Vol. 9681).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Symbolic Reachability Analysis of B through ProB and LTSmin

AU - Bendisposto,J.

AU - Körner,P.

AU - Leuschel,M

AU - Meijer,Jeroen

AU - van de Pol,Jan Cornelis

AU - Treharne,H.

AU - Whitefield,J.

PY - 2016/6

Y1 - 2016/6

N2 - 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.

AB - 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.

KW - LTSMIN

KW - Symbolic reachability

KW - ProB

KW - METIS-318458

KW - B-Method

KW - Event-B

KW - IR-100722

KW - EWI-27071

U2 - 10.1007/978-3-319-33693-0_18

DO - 10.1007/978-3-319-33693-0_18

M3 - Conference contribution

SN - 978-3-319-33692-3

T3 - Lecture Notes in Computer Science

SP - 275

EP - 291

BT - Integrated Formal Methods

PB - Springer International Publishing

ER -

Bendisposto J, Körner P, Leuschel M, Meijer J, van de Pol JC, Treharne H et al. Symbolic Reachability Analysis of B through ProB and LTSmin. In Ábrahám E, Huisman M, editors, Integrated Formal Methods: 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. Cham: Springer International Publishing. 2016. p. 275-291. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-33693-0_18