Skip to main content
SpringerLink
Log in

Proof Assisted Model Checking for B

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2009)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5885))

Included in the following conference series:

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)

    MATH  Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. 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)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Article  Google Scholar 

  8. Butler, M., Yadav, D.: An incremental development of the Mondex system in Event-B. Formal Aspects of Computing 20(1), 61–77 (2008)

    Article  Google Scholar 

  9. 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)

    Google Scholar 

  10. Clarke, E., Grumberg, O., Hiraishi, H., Jha, S.: Verification of the futurebus+ cache coherence protocol. Formal Methods in System Design (January 1995)

    Google Scholar 

  11. 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

    Google Scholar 

  12. 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)

    Article  Google Scholar 

  13. Freitas, L.: Model Checking Circus. PhD thesis, University of York (2005)

    Google Scholar 

  14. Freitas, L., Woodcock, J., Cavalcanti, A.: State-rich model checking. Innovations Syst. Softw. Eng. 2(1), 49–64 (2006)

    Article  Google Scholar 

  15. Gunter, E.L., Peled, D.: Model checking, testing and verification working together. Formal Asp. Comput. 17(2), 201–221 (2005)

    Article  MATH  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. 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)

    Google Scholar 

  19. Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT 10(2), 185–203 (2008)

    Article  Google Scholar 

  20. 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)

    Google Scholar 

  21. 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)

    Google Scholar 

  22. 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)

    Google Scholar 

  23. 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)

    Google Scholar 

  24. 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)

    Chapter  Google Scholar 

  25. 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)

    Google Scholar 

  26. Romanovsky, A.: Rigorous Open Development Environment for Complex Systems - RODIN. ERCIM News 65, 40–41 (2006)

    Google Scholar 

  27. 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

    Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. Sipma, H., Uribe, T., Manna, Z.: Deductive model checking. Formal Methods in System Design 15(1), 49–74 (1999)

    Article  Google Scholar 

  30. 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)

    Google Scholar 

  31. Steria, F.: Aix-en-Provence. In: Atelier B, User and Reference Manuals (1996), http://www.atelierb.societe.com

  32. 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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Heinrich-Heine Universität Düsseldorf, Universitätsstr. 1, D-40225, Düsseldorf

    Jens Bendisposto & Michael Leuschel

Authors
  1. Jens Bendisposto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Leuschel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Coordenadora da Engenharia de Computação, Diretora de Publicações da SBC, Depto. Informática, ontifícia Universidade Católica do Rio de Janeiro, ,, R. Marques de Sao Vicente 225 - Prédio do RDC - Sala 416, Rio de Jan,  

    Karin Breitman

  2. Department of Computer Science, University of York, ,, Heslington, YO10 5DD, York, UK,

    Ana Cavalcanti

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation