Abstract
Formal specification languages are traditionally supported by theorem provers, but recently model checkers have proven to be useful tools. In this paper we present Eboc, an explicit state model checker for Event-B. Eboc is based on lazy techniques that allow it to fairly perform an exhaustive state space search without bounding the size of the sets used in the specification. We describe the implementation of Eboc and provide a preliminary comparison with ProB, an existing bounded model checker for classical B.
This work is partially funded by EU project Coconut FP7-ICT-217069 and by EPSRC Grant EP/E012973/1.
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
Smith, G., Wildman, L.: Model checking Z specifications using SAL. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 85–103. Springer, Heidelberg (2005)
Derrick, J., North, S., Simons, T.: Issues in implementing a model checker for Z. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 678–696. Springer, Heidelberg (2006)
Derrick, J., North, S., Simons, A.J.H.: Z2SAL - building a model checker for Z. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 280–293. Springer, Heidelberg (2008)
Hoare, C.A.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1986)
Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, Cambridge (1996)
Behm, P., Benoit, P., Faivre, A., Meynadier, J.M.: Météor: A successful application of B in a large project. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369–387. Springer, Heidelberg (1999)
Abrial, J.R.: Modeling in Event-B: Systems and Software Engineering. To be published by Cambridge University Press (2009)
Hallerstede, S.: On the purpose of Event-B proof obligations. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 125–138. Springer, Heidelberg (2008)
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)
Hallerstede, S.: Justifications for the Event-B modelling notation. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 49–63. Springer, Heidelberg (2006)
Métayer, C., Voisin, L.: The Event-B mathematical language (March 2009), http://wiki.event-b.org/index.php/Event-B_Mathematical_Language
Flatt, M., et al.: Reference: PLT Scheme. Reference Manual PLT-TR2009-reference-v4.2, PLT Scheme Inc. (June 2009)
Flatt, M., Felleisen, M.: Units: Cool modules for hot languages. In: Proc. Conf. on Programming Language Design and Implementation, SIGPLAN Notices, vol. 33(5), pp. 236–248. ACM, New York (1998)
Schneider, S.: The B-method — an introduction. Palgrave Macmillan, Basingstoke (2001)
Colley, J.: An Investigation into using Event-B for sub-system development in a SystemC TLM flow. Private Communication (July 2007)
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2006)
Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)
Leuschel, M., Plagge, D.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Technical Report STUPS/2007/02, Institut für Informatik, Heinrich-Heine-Universität Düsseldorf (2007)
Spermann, C., Leuschel, M.: ProB gets nauty: Effective symmetry reduction for B and Z models. In: Proc. 2nd Intl. Symposium on Theoretical Aspects of Software Engineering, pp. 15–22. IEEE, Los Alamitos (2008)
Plagge, D., Leuschel, M., Lopatkin, I., Iliasov, A., Romanovsky, A.: SAL, Kodkod, and BDDs for validation of B models. lessons and outlook. In: Proc. 4th Workshop on Automated Formal Methods (June 2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Matos, P.J., Fischer, B., Marques-Silva, J. (2009). A Lazy Unbounded Model Checker for Event-B . In: Breitman, K., Cavalcanti, A. (eds) Formal Methods and Software Engineering. ICFEM 2009. Lecture Notes in Computer Science, vol 5885. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10373-5_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-10373-5_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10372-8
Online ISBN: 978-3-642-10373-5
eBook Packages: Computer ScienceComputer Science (R0)