Abstract
We consider modelling indispensable for the development of complex systems. Modelling must be carried out in a formal notation to reason and make meaningful conjectures about a model. But formal modelling of complex systems is a difficult task. Even when theorem provers improve further and get more powerful, modelling will remain difficult. The reason for this that modelling is an exploratory activity that requires ingenuity in order to arrive at a meaningful model. We are aware that automated theorem provers can discharge most of the onerous trivial proof obligations that appear when modelling systems. In this article we present a modelling tool that seamlessly integrates modelling and proving similar to what is offered today in modern integrated development environments for programming. The tool is extensible and configurable so that it can be adapted more easily to different application domains and development methods.
This research was carried out as part of the EU research project IST 511599 RODIN (Rigorous Open Development Environment for Complex Systems) http://rodin.cs.ncl.ac.uk
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: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Abrial, J.-R., Cansell, D.: Click’n’Prove: Interactive Proofs within Set Theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 1–24. Springer, Heidelberg (2003)
Abrial, J.-R., Hallerstede, S.: Refinement, decomposition and instantiation of discrete models. Fundamentae Informatica (to appear, 2006)
Back, R.J.R.: Refinement calculus, part II: Parallel and reactive programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 67–93. Springer, Heidelberg (1990)
Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334–354. Springer, Heidelberg (2005)
Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, p. 363. Springer, Heidelberg (2000)
Barnett, M., Chang, B.-Y., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Bertot, Y., Castéran, P.(P.): Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, Heidelberg (2004)
Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: A proof environment for Z-specifications. Journal of Universal Computer Science 9(2), 152–172 (2003)
Clearsy. Atelier B tool homepage, http://www.atelierb.societe.com/
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Eclipse. Eclipse platform homepage, http://www.eclipse.org/
Filliâtre, J.-C.: Verification of Non-Functional Programs using Interpretations in Type Theory. Journal of Functional Programming 13(4), 709–745 (2003)
Gamma, E., Beck, K.: Contributing to Eclipse. Addison Wesley, Reading (2003)
Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common lisp. IEEE Transactions on Software Engineering 23(4), 203–213 (1997)
King, J.C.: A new approach to program testing. In: Proceedings of the international conference on Reliable software, pp. 228–233. ACM Press, New York (1975)
Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2002)
Långbacka, T., von Wright, J.: Refining reactive systems in HOL using action systems. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 183–197. Springer, Heidelberg (1997)
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)
Morgan, C., Hoang, T.S., Abrial, J.-R.: The challenge of probabilistic event B - extended abstract. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 162–171. Springer, Heidelberg (2005)
Nipkow, T.: Structured Proofs in Isar/HOL. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 259–278. Springer, Heidelberg (2003)
Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
RODIN. RODIN project homepage, http://rodin.cs.ncl.ac.uk/
RODIN. Deliverable D16: Prototype Plug-in Tools (2006), http://rodin.cs.ncl.ac.uk/deliverables.htm
Saaltink, M.: The Z/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–85. Springer, Heidelberg (1997)
Snook, C., Butler, M.: UML-B: Formal modelling and design aided by UML. ACM Transactions on Software Engineering and Methodology (to appear, 2006), http://eprints.ecs.soton.ac.uk/10169/
Snook, C., Sandstrom, K.: Using UML-B and U2B for formal refinement of digital components. In: Proceedings of Forum on specification and design languages (FDL 2003) (2003)
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. International Series in Computer Science. Prentice-Hall, New York (1992)
Winterstein, D., Aspinall, D., Lüth, C.: Proof general / eclipse: A generic interface for interactive proof. In: IJCAI, pp. 1587–1588 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abrial, JR., Butler, M., Hallerstede, S., Voisin, L. (2006). An Open Extensible Tool Environment for Event-B. In: Liu, Z., He, J. (eds) Formal Methods and Software Engineering. ICFEM 2006. Lecture Notes in Computer Science, vol 4260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901433_32
Download citation
DOI: https://doi.org/10.1007/11901433_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47460-9
Online ISBN: 978-3-540-47462-3
eBook Packages: Computer ScienceComputer Science (R0)