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

Philipp Körner; Michael Leuschel; Jeroen Meijer

doi:10.1007/978-3-319-98938-9_16

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 proceeding › Conference contribution › Academic › peer-review

4 Citations (Scopus)

239 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 language	English
Title of host publication	Integrated Formal Methods - 14th International Conference, IFM 2018, Proceedings
Subtitle of host publication	14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings
Editors	Carlo A. Furia, Kirsten Winter
Publisher	Springer
Pages	275-295
Number of pages	21
ISBN (Electronic)	978-3-319-98938-9
ISBN (Print)	978-3-319-98937-2
DOIs	https://doi.org/10.1007/978-3-319-98938-9_16
Publication status	Published - Sept 2018
Event	14th International Conference on Integrated Formal Methods, IFM 2018 - Maynooth University, Maynooth, Ireland Duration: 5 Sept 2018 → 7 Sept 2018 https://ifm2018.cs.nuim.ie/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11023

Conference

Conference	14th International Conference on Integrated Formal Methods, IFM 2018
Abbreviated title	IFM 2018
Country/Territory	Ireland
City	Maynooth
Period	5/09/18 → 7/09/18
Internet address	https://ifm2018.cs.nuim.ie/

Access to Document

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

paperAccepted author version, 407 KB

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, Proceedings: 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, Proceedings: 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",

note = "Funding Information: Acknowledgement. Computational support and infrastructure was provided by the “Centre for Information and Media Technology” (ZIM) at the University of D{\"u}ssel-dorf (Germany). We also thank Ivaylo Dobrikov and Alfons Laarman for their helpful explanations concerning partial order reduction algorithms. Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2018.; 14th International Conference on Integrated Formal Methods, IFM 2018, IFM 2018 ; Conference date: 05-09-2018 Through 07-09-2018",

year = "2018",

month = sep,

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 - 14th International Conference, IFM 2018, Proceedings",

address = "Germany",

url = "https://ifm2018.cs.nuim.ie/",

}

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, Proceedings: 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, Proceedings: 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 proceeding › Conference contribution › Academic › peer-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

N1 - Funding Information: Acknowledgement. Computational support and infrastructure was provided by the “Centre for Information and Media Technology” (ZIM) at the University of Düssel-dorf (Germany). We also thank Ivaylo Dobrikov and Alfons Laarman for their helpful explanations concerning partial order reduction algorithms. Publisher Copyright: © Springer Nature Switzerland AG 2018.

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 - 14th International Conference, IFM 2018, Proceedings

A2 - Furia, Carlo A.

A2 - Winter, Kirsten

PB - Springer

T2 - 14th International Conference on Integrated Formal Methods, IFM 2018

Y2 - 5 September 2018 through 7 September 2018

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, Proceedings: 14th International Conference, IFM 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings. Springer. 2018. p. 275-295. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-98938-9_16

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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this