Abstract
TLA + and B share the common base of predicate logic, arithmetic and set theory. However, there are still considerable differences, such as very different approaches to typing and modularization. There is also considerable difference in the available tool support. In this paper, we present a translation of the non-temporal part of TLA + to B, which makes it possible to feed TLA + specifications into existing tools for B. Part of this translation must include a type inference algorithm, in order to produce typed B specifications. There are many other tricky aspects, such as translating modules as well as let/in and if/then/else expressions. We also present an integration of our translation into ProB. ProB thus provides a complementary tool to the explicit state model checker TLC, with convenient animation and constraint solving for TLA + . We also present a series of case studies, highlighting the complementarity to TLC. In particular, we highlight the sometimes dramatic difference in performance when it comes to solving complicated constraints in TLA + .
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Abrial, J.-R.: The B-Book. Cambridge University Press (1996)
Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA + Proof System: Building a Heterogeneous Verification Platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, p. 44. Springer, Heidelberg (2010)
ClearSy. Atelier B, User and Reference Manuals. Aix-en-Provence, France (2009), http://www.atelierb.eu/
Hallerstede, S., Leuschel, M.: Constraint-based deadlock checking of high-level specifications. TPLP 11(4-5), 767–782 (2011)
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., Massart, T.: Efficient approximate verification of B via symmetry markers. Annals of Mathematics and Artificial Intelligence 59(1), 81–106 (2010)
Merz, S.: TLA+ Case Study: A Resource Allocator. Technical Report A04-R-101, INRIA Lorraine - LORIA (2004), http://hal.inria.fr/inria-00107809
Merz, S., Vanzetto, H.: Automatic Verification of TLA + Proof Obligations with SMT Solvers. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 289–303. Springer, Heidelberg (2012)
Mokhtari, Y., Merz, S.: Animating TLA Specifications. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705, pp. 92–110. Springer, Heidelberg (1999)
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)
Plagge, D., Leuschel, M.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT 11, 9–21 (2010)
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
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hansen, D., Leuschel, M. (2012). Translating TLA + to B for Validation with ProB . In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds) Integrated Formal Methods. IFM 2012. Lecture Notes in Computer Science, vol 7321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30729-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-30729-4_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30728-7
Online ISBN: 978-3-642-30729-4
eBook Packages: Computer ScienceComputer Science (R0)