Abstract
We present PROB, an animation and model checking tool for the B method. PROB’s animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the B-Toolkit, the user does not have to guess the right values for the operation arguments or choice variables. PROB contains a model checker and a constraint-based checker, both of which can be used to detect various errors in B specifications. We present our first experiences in using PROB on several case studies, highlighting that PROB enables users to uncover errors that are not easily discovered by existing tools.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Utting, M., Vacelet, N.: BZ-testing-tools: A tool-set for test generation from Z and B using constraint logic programming. In: Proceedings of FATES 2002, Formal Approaches to Testing of Software, August 2002, pp. 105–120 (2002); Technical Report, INRIA
AT&T Labs-Research. Graphviz - open source graph drawing software, Obtainable at http://www.research.att.com/sw/tools/graphviz/
B-Core (UK) Limited, Oxon, UK. B-Toolkit, On-line manual (1999), Available at http://www.b-core.com/ONLINEDOC/Contents.html
Bérard, B., Fribourg, L.: Reachability analysis of (timed) petri nets using real arithmetic. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 178–193. Springer, Heidelberg (1999)
Bouquet, F., Legeard, B., Peureux, F.: CLPS-B - a constraint solver for B. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 188–204. Springer, Heidelberg (2002)
Bowen, J.: Animating the semantics of VERILOG using Prolog. Technical Report UNU/IIST Technical Report no. 176, United Nations University, Macau (1999)
Butler, M.: csp2B: A practical approach to combining CSP and B. Formal Aspects of Computing 12, 182–198 (2000)
Butler, M.: A system-based approach to the formal development of embedded controllers for a railway. Design Automation for Embedded Systems 6(4), 355–366 (2002)
Cabeza, D., Hermenegildo, M.: The PiLLoW Web Programming Library. The CLIP Group, School of Computer Science, Technical University of Madrid (2001), Available at http://www.clip.dia.fi.upm.es/
Carlsson, M., Ottosson, G.: An open-ended finite domain constraint solver. In: Hartel, P.H., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 191–206. Springer, Heidelberg (1997)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Cui, B., Dong, Y., Du, X., Kumar, N., Ramakrishnan, C.R., Ramakrishnan, I.V., Roychoudhury, A., Smolka, S.A., Warren, D.S.: Logic programming and model checking. In: Palamidessi, C., Meinke, K., Glaser, H. (eds.) ALP 1998 and PLILP 1998. LNCS, vol. 1490, pp. 1–20. Springer, Heidelberg (1998)
Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Transactions on Programming Languages and Systems (TOPLAS) 22(5), 861–931 (2000)
Bellegarde, F., Julliand, J., Mountassir, H.: Model-Based Verification through Refinement of Finite B Event Systems. In: Formal Methods B Users Group Meeting (FM 1999 B UGM Meeting) (September 1999)
Ferreira, C., Butler, M.: A process compensation language. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 424–435. Springer, Heidelberg (2000)
Henderson, P.: Modelling architectures for dynamic systems. In: McIver, A., Morgan, C. (eds.) Programming Methodology. Springer, Heidelberg (2003)
Jackson, D.: Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology (TOSEM) 11, 256–290 (2002)
Jackson, D., Shlyakhter, I., Sridharan, M.: A micromodularity mechanism. In: ACM SIGSOFT Conference on the Foundations of Software Engineering / European Software Engineering Conference (FSE / ESEC 2001), September 2001, pp. 256–290 (2001)
Jia, X.: An approach to animating Z specifications, Available at http://venus.cs.depaul.edu/fm/zans.html
King, L., Gupta, G., Pontelli, E.: Verification of a controller for BART. In: Winter, V.L., Bhattacharya, S. (eds.) High Integrity Software, pp. 265–299. Kluwer Academic Publishers, Dordrecht (2001)
Lanet, J.-L.: The use of B for Smart Card. In: Forum on Design Languages (FDL 2002) (September 2002)
Leuschel, M.: Design and implementation of the high-level specification language CSP(LP) in Prolog. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol. 1990, pp. 14–28. Springer, Heidelberg (2001)
Leuschel, M., Adhianto, L., Butler, M., Ferreira, C., Mikhailov, L.: Animation and model checking of CSP and B using Prolog technology. In: Proceedings of VCL 2001, Florence, Italy, September 2001, pp. 97–109 (2001)
Leuschel, M., Jørgensen, J., Vanhoof, W., Bruynooghe, M.: Offline specialisation in Prolog using a hand-written compiler generator. In: Theory and Practice of Logic Programming (2004) (to appear)
Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialisation. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol. 1817, pp. 63–82. Springer, Heidelberg (2000)
Leuschel, M., Massart, T.: Logic programming and partial deduction for the verification of reactive systems: An experimental evaluation. In: Norman, G., Kwiatkowska, M., Guelev, D. (eds.) Proceedings of AVoCS 2002, Second Workshop on Automated Verification of Critical Systems, pp. 143–149 (2002); Available as Technical Report CSR-02-6, University of Birmingham
Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University (1981)
Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 143–154. Springer, Heidelberg (1997)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1999)
Sagonas, K., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Proceedings of the ACM SIGMOD International Conference on the Management of Data, Minneapolis, Minnesota, May 1994, pp. 442–453. ACM, New York (1994)
Snook, C., Butler, M.: Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit. In: UML 2000 WORKSHOP Dynamic Behaviour in UML Models: Semantic Questions (October 2000)
Steria, Aix-en-Provence, France. Atelier B, User and Reference Manuals (1996), Available at http://www.atelierb.societe.com/index_uk.html
Tatibouet, B.: The JBTools Package (2001), Available at http://lifc.univfcomte.fr/PEOPLE/tatibouet/JBTOOLS/BParseren.html
Winikoff, M., Dart, P., Kazmierczak, E.: Rapid prototyping using formal specifications. In: Proceedings of the 21st Australasian Computer Science Conference, Perth, Australia, February 1998, pp. 279–294 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leuschel, M., Butler, M. (2003). ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_46
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_46
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive