The state-based formal methods B and TLA + share the common base of predicate logic, arithmetic and set theory. However, there are still considerable differences, such as the way to specify state transitions, the different approaches to typing, and the available tool support. In this paper, we present a translation from B to TLA + to validate B specifications using the model checker TLC. We provide translation rules for almost all constructs of B, in particular for those which are not built-in in TLA + . The translation also includes many adaptations and optimizations to allow efficient checking by TLC. Moreover, we present a way to validate liveness properties for B specifications under fairness conditions. Our implemented translator, Tlc4B, automatically translates a B specification to TLA + , invokes the model checker TLC, and translates the results back to B. We use ProB to double check the counter examples produced by TLC and replay them in the ProB animator. We also present a series of case studies and benchmark tests comparing Tlc4B and ProB.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{HansenL14,
author = {Dominik Hansen and
Michael Leuschel},
editor = {Yamine A{\"{\i}}t Ameur and
Klaus{-}Dieter Schewe},
title = {Translating {B} to {TLA} + for Validation with {TLC}},
booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8477},
pages = {40--55},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-662-43652-3\_4},
doi = {10.1007/978-3-662-43652-3\_4},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/HansenL14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}