Abstract
The Rodin tool for Event-B supports formal modelling and proof using a mathematical language that is based on predicate logic and set theory. Although Rodin has in-built support for a rich set of operators and proof rules, for some application areas there may be a need to extend the set of operators and proof rules supported by the tool. This paper outlines a new feature of the Rodin tool, the theory component, that allows users to extend the mathematical language supported by the tool. Using theories, Rodin users may define new data types and polymorphic operators in a systematic and practical way. Theories also allow users to extend the proof capabilities of Rodin by defining new proof rules that get incorporated into the proof mechanisms. Soundness of new definitions and rules is provided through validity proof obligations.
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.
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010)
Abrial, J.-R.: B#: Toward a synthesis between Z and B. In: Bert, D., Bowen, J.P., King, S., Waldén, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 168–177. Springer, Heidelberg (2003)
Abrial, J.-R., Cansell, D., Laffitte, G.: “Higher-Order” Mathematics in B. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 370–393. Springer, Heidelberg (2002)
Di Cultura, I.T., Armando, A., Armando, A., Cimatti, A., Cimatti, A.: Building and executing proof strategies in a formal metatheory. In: Torasso, P. (ed.) AI*IA 1993. LNCS, vol. 728, pp. 11–22. Springer, Heidelberg (1993)
Gordon, M.: HOL: A Machine Oriented Formulation of Higher Order Logic (1985)
Griffioen, D., Huisman, M.: A comparison of PVS and isabelle/HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 123–142. Springer, Heidelberg (1998)
Harrison, J.: Metatheory and Reflection in Theorem Proving: A Survey and Critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995) http://www.cl.cam.ac.uk/~jrh13/papers/reflect.dvi.gz
Mehta, F.: A Practical Approach to Partiality – A Proof Based Approach. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 238–257. Springer, Heidelberg (2008)
Mehta, F.: Proofs for the Working Engineer. PhD Thesis, ETH Zurich (2008)
Milner, R.: Logic for computable functions: description of a machine implementation. Technical report, Stanford, CA, USA (1972)
Milner, R., Tofte, M., Harper, R.: The definition of Standard ML. MIT Press, Cambridge (1990)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle Logics: HOL (2000)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference (2001)
Robinson, K.: Reconciling axiomatic and model-based specifications reprised. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 223–236. Springer, Heidelberg (2008)
Romanovsky, A., Thomas, M. (eds.): Industrial Deployment of System Engineering Methods. Springer (2013)
Schmalz, M.: The Logic of Event-B. Technical Report 698, ETH Zurich, Switzerland (2010), http://www.inf.ethz.ch/research/disstechreps/techreports
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Butler, M., Maamria, I. (2013). Practical Theory Extension in Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol 8051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39698-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-39698-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39697-7
Online ISBN: 978-3-642-39698-4
eBook Packages: Computer ScienceComputer Science (R0)