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

1 Citation (Scopus)
7 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

Model checking

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
Körner, Philipp ; Leuschel, Michael ; Meijer, Jeroen. / State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin. Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings. editor / Carlo A. Furia ; Kirsten Winter. Springer, 2018. pp. 275-295 (Lecture Notes in Computer Science).
@inproceedings{d0a907f1468d4555a979668deb35fdd8,
title = "State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin",
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.",
author = "Philipp K{\"o}rner and Michael Leuschel and Jeroen Meijer",
year = "2018",
month = "9",
doi = "10.1007/978-3-319-98938-9_16",
language = "English",
isbn = "978-3-319-98937-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "275--295",
editor = "Furia, {Carlo A.} and Kirsten Winter",
booktitle = "Integrated Formal Methods",

}

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

State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin. / Körner, Philipp; Leuschel, Michael; Meijer, Jeroen.

Integrated Formal Methods: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings. ed. / Carlo A. Furia; Kirsten Winter. Springer, 2018. p. 275-295 (Lecture Notes in Computer Science; Vol. 11023).

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

TY - GEN

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

AU - Körner, Philipp

AU - Leuschel, Michael

AU - Meijer, Jeroen

PY - 2018/9

Y1 - 2018/9

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

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

U2 - 10.1007/978-3-319-98938-9_16

DO - 10.1007/978-3-319-98938-9_16

M3 - Conference contribution

SN - 978-3-319-98937-2

T3 - Lecture Notes in Computer Science

SP - 275

EP - 295

BT - Integrated Formal Methods

A2 - Furia, Carlo A.

A2 - Winter, Kirsten

PB - Springer

ER -

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