Abstract
With the aid of the ProB Plugin, the Rodin Platform provides an integrated environment for editing, proving, animating and model checking Event-B models. This is of considerable benefit to the modeler, as it allows him to switch between the various tools to validate, debug and improve his or her models. The crucial idea of this paper is that the integrated platform also provides benefits to the tool developer, i.e., it allows easy access to information from other tools. Indeed, there has been considerable interest in combining model checking, proving and testing. In previous work we have already shown how a model checker can be used to complement the Event-B proving environment, by acting as a disprover. In this paper we show how the prover can help improve the efficiency of the animator and model checker.
This research is being carried out as part of the DFG funded research project GEPAVAS and the EU funded FP7 research project 214158: DEPLOY (Industrial deployment of advanced system engineering methods for high productivity and dependability).
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.
Similar content being viewed by others
References
Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)
Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)
Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: Mocha: Modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.C.: Integrating model checking and theorem proving for relational reasoning. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 21–33. Springer, Heidelberg (2004)
Arons, T., Pnueli, A., Zuck, L.: Parameterized verification by probabilistic abstraction. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 87–102. Springer, Heidelberg (2003)
Bendisposto, J., Jastram, M., Leuschel, M., Lochert, C., Scheuermann, B., Weigelt, I.: Validating Wireless Congestion Control and Realiability Protocols using ProB and Rodin. FMWS 2008: Workshop on Formal Methods for Wireless Systems (August 2008)
Bendisposto, J., Leuschel, M., Ligot, O., Samia, M.: La validation de modèles event-b avec le plug-in prob pour rodin. Technique et Science Informatiques 27(8), 1065–1084 (2008)
Butler, M., Yadav, D.: An incremental development of the Mondex system in Event-B. Formal Aspects of Computing 20(1), 61–77 (2008)
Cansell, D., Hallerstede, S., Oliver, I.: UML-B specification and hardware implementation of a hamming coder/decoder. In: Mermet, J. (ed.) UML-B Specification for Proven Embedded Systems Design, ch. 16, November 2004. Kluwer Academic Publishers, Dordrecht (2004)
Clarke, E., Grumberg, O., Hiraishi, H., Jha, S.: Verification of the futurebus+ cache coherence protocol. Formal Methods in System Design (January 1995)
Dams, D., Hutter, D., Sidorova, N.: Using the inka prover to automate safety proofs in abstract interpretation - a case study. In: Bellegarde, F., Kouchnarenko, O. (eds.) Workshop on Modelling and Verification, C.I.S., Besançon, France (1999); Alternative title: Combining Theorem Proving and Model Checking - A Case Study
Dybjer, P., Haiyan, Q., Takeyama, M.: Verifying haskell programs by combining testing, model checking and interactive theorem proving. Information & Software Technology 46(15), 1011–1025 (2004)
Freitas, L.: Model Checking Circus. PhD thesis, University of York (2005)
Freitas, L., Woodcock, J., Cavalcanti, A.: State-rich model checking. Innovations Syst. Softw. Eng. 2(1), 49–64 (2006)
Gunter, E.L., Peled, D.: Model checking, testing and verification working together. Formal Asp. Comput. 17(2), 201–221 (2005)
Legeard, B., Peureux, F., Utting, M.: Automated boundary testing from Z and B. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 21–40. Springer, Heidelberg (2002)
Leuschel, M.: The high road to formal validation. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 4–23. 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)
Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)
Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale b models. In: Cavalcanti, A., Dams, D. (eds.) Proceedings FM 2009. LNCS, vol. 5850, pp. 708–723. Springer, Heidelberg (2009)
Leuschel, M., Plagge, D.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. In: Ameur, Y.A., Boniol, F., Wiels, V. (eds.) Proceedings Isola 2007, Cépaduès edn. Revue des Nouvelles Technologies de l’Information, vol. RNTI-SM-1, pp. 73–84 (2007)
Müller, O., Nipkow, T.: Combining model checking and deduction for i/o-automata. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 1–16. Springer, Heidelberg (1995)
Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)
Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82–97. Springer, Heidelberg (2001)
Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 184–195. Springer, Heidelberg (1996)
Romanovsky, A.: Rigorous Open Development Environment for Complex Systems - RODIN. ERCIM News 65, 40–41 (2006)
Scheuermann, B., Lochert, C., Mauve, M.: Implicit hop-by-hop congestion control in wireless multihop networks. In: Ad Hoc Networks (2007), doi:10.1016/j.adhoc.2007.01.001
Shankar, N.: Combining theorem proving and model checking through symbolic analysis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 1–16. Springer, Heidelberg (2000)
Sipma, H., Uribe, T., Manna, Z.: Deductive model checking. Formal Methods in System Design 15(1), 49–74 (1999)
Spermann, C., Leuschel, M.: ProB gets nauty: Effective symmetry reduction for B and Z models. In: Proceedings Symposium TASE 2008, Nanjing, China, pp. 15–22. IEEE, Los Alamitos (2008)
Steria, F.: Aix-en-Provence. In: Atelier B, User and Reference Manuals (1996), http://www.atelierb.societe.com
Uribe, T.: Combinations of model checking and theorem proving. In: Kirchner, H., Ringeissen, C. (eds.) Frocos 2000. LNCS (LNAI), vol. 1794, pp. 151–170. Springer, Heidelberg (2000)
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
Bendisposto, J., Leuschel, M. (2009). Proof Assisted Model Checking for 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_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-10373-5_26
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)