Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book. Cambridge University Press (1996)
ClearSy. B language reference manual, http://www.tools.clearsy.com/resources/Manrefb_en.pdf (accessed: November 10, 2013)
Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + proofs. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 147–154. Springer, Heidelberg (2012)
Gafni, E., Lamport, L.: Disk Paxos. Distributed Computing 16(1), 1–20 (2003)
Hansen, D., Leuschel, M.: Translating TLA + to B for validation with ProB. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 24–38. Springer, Heidelberg (2012)
Hansen, D., Leuschel, M.: Translating B to TLA+ for validation with TLC (2013), http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport
Lamport, L.: The TLA+ hyperbook, http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html (accessed: October 30, 2013)
Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)
Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)
Mosbahi, O., Jemni, L., Jaray, J.: A formal approach for the development of automated systems. In: Filipe, J., Shishkov, B., Helfert, M. (eds.) ICSOFT (SE), pp. 304–310. INSTICC Press (2007)
Reynolds, M.: Changing nothing is sometimes doing something. Technical Report TR-98-02, Department of Computer Science, King’s College London (February 1998)
Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hansen, D., Leuschel, M. (2014). Translating B to TLA + for Validation with TLC. In: Ait Ameur, Y., Schewe, KD. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014. Lecture Notes in Computer Science, vol 8477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43652-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-662-43652-3_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43651-6
Online ISBN: 978-3-662-43652-3
eBook Packages: Computer ScienceComputer Science (R0)