Abstract
We present ProB, a validation toolset for the B method. ProB’s automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a refinement checker, both of which can be used to detect various errors in B specifications. We describe the underlying methodology of ProB, and present the important aspects of the implementation. We also present empirical evaluations as well as several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B’98: Recent Advances in the Development and Use of the B Method, Second International B Conference, Montpellier, France, April 22–24, 1998, Proceedings. LNCS, vol. 1393. Springer, Heidelberg (1998)
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Abrial, J.-R.: Case study of a complete reactive system in Event-B: a mechanical press controller. In: Tutorial at ZB’2005, http://www.zb2005.org/ (2005)
Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: ICFEM06. LNCS, vol. 4260. Springer, Heidelberg (2006)
Abrial, J.-R., Cansell, D.: Click’n prove: interactive proofs within set theory. In: Basin, D.A., Wolff, B. (eds) TPHOLs. LNCS, vol. 2758, pp. 1–24. Springer, Heidelberg (2003)
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’02, Formal Approaches to Testing of Software, August 2002. Technical Report, INRIA, pp. 105–120 (2002)
AT&T Labs-Research. Graphviz—open source graph drawing software. http://www.research.att.com/sw/tools/graphviz/
UK B-Core (UK) Limited, Oxon: B-Toolkit, On-line manual, 1999. http://www.b-core.com/ONLINEDOC/Contents.html
Basu, S., Mukund, M., Ramakrishnan, C.R., Ramakrishnan, I.V., Verma, R.M.: Local and symbolic bisimulation using tabled constraint logic programming. In: International Conference on Logic Programming (ICLP), Paphos, Cyprus, November 2001. LNCS, vol. 2237, pp. 166–180. Springer, Heidelberg (2001)
Bellegarde, F., Julliand, J., Mountassir, H.: Model-based verification through refinement of finite B event systems. In: Robinson, K., Bert, D. (eds), Formal Methods’99 B User Group Meeting, Toulouse, France, September 1999. Springer, Heidelberg (1999)
Bendisposto, J., Leuschel, M.: A Generic Flash-Based Animation Engine for ProB. In: Julliand and Kouchnarenko [36], pp. 266–269 (1999)
Bérard, B., Fribourg, L.: Reachability analysis of (timed) petri nets using real arithmetic. In: Proceedings of Concur’99, 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), Tools and Algorithms for the Construction and Analysis of Systems, 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)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Informat. Computat. 98(2), 142–170 (1992)
Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Proceedings of Formal Methods 2005, Newcastle upon Tyne, LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005)
Butler, M.J.: An approach to the design of distributed systems with B AMN. In: Bowen, J.P., Hinchey, M.G., Till, D.,(eds), ZUM ’97: The Z Formal Specification Notation, 10th International Conference of Z Users, Reading, UK, April, 1997, Proceedings, LNCS, vol. 1212, pp. 223–241. Springer, Heidelberg (1997)
Butler, M.J.: csp2B: a practical approach to combining CSP and B. Formal Asp. Comput. 12(3), 182–198 (2000)
Carlsson, M., Ottosson, G.: An open-ended finite domain constraint solver. In: Glaser, H.G., Hartel, P.H., Kuchen, H. (eds), Proc. Programming Languages: Implementations, Logics, and Programs, LNCS, vol. 1292 pp. 191–206. Springer, Heidelberg (1997)
Clarke, E.M.: Orna Grumberg, and Doron Peled. Model Checking. MIT Press, (1999)
ClearSy. Atelier B, User and Reference Manuals, Available at http://www.atelierb.societe.com/index_uk.html
Cui, B., Dong, Y., Du, X., Narayan Kumar, C.R., Ramakrishnan, I.V., Ramakrishnan, Roychoudhury, A., Smolka, S.A., Warren, D.S.: Logic programming and model checking. In: Palamidessi, C., Glaser, H., Meinke, K., (eds) Proceedings of ALP/PLILP’98, 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)
Dunne, S., Conroy, S.: Process refinement in B. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds), ZB 2005: Formal Specification and Development in Z and B, 4th International Conference of B and Z Users, Guildford, UK, LNCS, vol. 3455, pp. 45–64. Springer, Heidelberg (2005)
Farwer, B., Leuschel, M.: Model checking object Petri nets in Prolog. In PPDP ’04: Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, pages 20–31, New York, NY, USA, 2004. ACM Press (2004)
Ferreira, C., Butler, M.: A process compensation language. In Santen, T., Stoddart, B. (eds), Proceedings Integrated Formal Methods (IFM 2000), LNCS, vol. 1945 pp. 424–435. Springer, November 2000 (2000)
Formal Systems (Europe) Ltd. Failures-Divergence Refinement—FDR2 User Manual. Available at http://www.fsel.com/
Gardiner, P.H.B., Morgan, C.: A single complete rule for data refinement. Formal Asp. Comput. 5(4), 367–382 (1993)
Hazel, D., Strooper, P., Traynor, O.: Possum: An animator for the SUM specification language. In Proceedings Asia-Pacific Software Engineering Conference and International Computer Science Conference, pages 42–51. IEEE Computer Society, (1997)
He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds), ESOP 86, European Symposium on Programming, Saarbrücken, Federal Republic of Germany, March, 1986, Proceedings, LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Henderson, P.: Modelling architectures for dynamic systems. In: McIver, A., Morgan, C. (eds) Programming Methodology. Springer, Heidelberg (2003)
Hoare, C.A.R: Communicating Sequential Processes. Prentice–Hall, Englewood Cliffs (1985)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2001
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, (2006)
Jia, X.: An approach to animating Z specifications. Available at http://venus.cs.depaul.edu/fm/zans.html
Julliand, J., Kouchnarenko, O. (eds.): B 2007: Formal Specification and Development in B, 7th International Conference of B Users, Besançon, France, January 17–19, 2007, Proceedings, volume 4355 of Lecture Notes in Computer Science. Springer
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, New York (2001)
Knuth, D.: All questions answered. Notices of the ACM 49(3), 318–324 (2003)
Lanet, J.-L.: The use of B for Smart Card. In Forum on Design Languages (FDL02) (2002)
Leuschel, M.: Design and implementation of the high-level specification language CSP(LP) in Prolog. In: Ramakrishnan, I.V. (ed), Proceedings of PADL 01, 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, pp. 97–109, Florence, Italy, September (2001)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds), Proceedings FME 2003, Pisa, Italy, LNCS vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Leuschel, M., Butlerm, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds), Proceedings ICFEM’05, LNCS, vol. 3785, pp. 345–359. Springer, Heidelberg (2005)
Leuschel, M., Butler, M., Spermann, C., Turner, E.: Symmetry reduction for B by permutation flooding. In: Julliand J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B, 7th International Conference of B Users, Besançon, France, January 17–19, 2007, Lecture Notes in Computer Science, Proceedings, vol. 4355 pp. 79–93. Springer, Heidelberg (2006)
Leuschel, M., Cansell, D., Butler, M.: Validating and animating higher-order recursive functions in B. In: Abrial, J.-R., Glässer, U. (eds), Festschrift for Egon Börger, May (2006)
Leuschel, M., Massart, T.: Infinite state model checking by abstract interpretation and program specialisation. In: Bossi, A. (ed.) Logic-Based Program Synthesis and Transformation. Proceedings of LOPSTR’99, Venice, Italy, 2000. LNCS, vol. 1817, pp. 63–82. Springer, Heidelberg (2000)
Leuschel, M., Turner, E.: Visualizing larger states spaces in ProB. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds), Proceedings ZB’2005, LNCS, vol. 3455, pp. 6–23. Springer, Heidelberg (2005)
Malik, P., Utting, M.: CZT: A framework for Z tools. In: Treharne, H., King, S., Henson, M.C., Schneider, S.A. (eds), ZB, LNCS, vol. 3455, pp. 65–84. Springer, Heidelberg (2005)
McMillan, K.L.: Symbolic model checking. PhD thesis, CMU (1993)
Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In Jim Davies and Jeremy Gibbons, editors, IFM, Lecture Notes in Computer Science, vol. 4591, pp. 480–500. Springer, Heidelberg (2007)
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), Proceedings of the International Conference on Computer-Aided Verification (CAV’97), LNCS, vol. 1254, pp. 143–154. Springer, Heidelberg (1997)
Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Dong, Y., Du, X., Roychoudhury, A., Venkatakrishnan, V.N.: XMC: A logic-programming-based verification toolset. In Proceedings of CAV 2000, pp. 576–580 (2000)
Robinson, N.J., Fidge, C.J.: Animation of data refinements. In Asia-Pacific Software Engineering Conference, APSEC 2002, pp. 137–146. IEEE Computer Society (2002)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice–Hall, Englewood Cliffs (1998)
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 (1994)
Schneider, S., Treharne, H.: Communicating B machines. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds), ZB 2002: Formal Specification and Development in Z and B, 2nd International Conference of B and Z Users, Grenoble, LNCS, vol. 2272, pp. 416–435. Springer, Heidelberg (2002)
Servat T BRAMA: a new graphic animation tool for B models. In: Julliand and Kouchnarenko [36], pp. 274–276
Sweden SICS, Kista: SICStus Prolog User’s Manual. http://www.sics.se/sicstus
Bruno Tatibouet: The jbtools package. http://lifc.univ-fcomte.fr/PEOPLE/tatibouet/JBTOOLS/BParser_en.html, 2001
Turner, E., Leuschel, M., Spermann, C., Butler, M.: Symmetry reduced model checking for B. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007, June 5–8, 2007, Shanghai, China. IEEE Computer Society (2007)
Utting, M.: Data structures for Z testing tools. In FM-TOOLS 2000 Conference, July 2000, TR 2000-07, Information Faculty, University of Ulm (2000)
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
Corresponding author
Additional information
This research was carried out as part of the EU research project IST 511599 RODIN (Rigorous Open Development Environment for Complex Systems).
Rights and permissions
About this article
Cite this article
Leuschel, M., Butler, M. ProB: an automated analysis toolset for the B method. Int J Softw Tools Technol Transf 10, 185–203 (2008). https://doi.org/10.1007/s10009-007-0063-9
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-007-0063-9