Abstract
We present a semi-shallow embedding in Coq of Event-B’s notions of abstract machine and refinement. The abstract structure of Event-B developments, including machines and refinement annotations, can be represented within Coq’s type system, using inductive and dependent types. This formalization allows us to reason at the meta-level on machines and their behaviors, considered as first-class citizens. We show how this formalization of Event-B structures into Coq allows us to model Rodin’s proof obligations, and prove how these obligations entail correctness properties of a given Event-B project. Moreover, the correctness of a given refinement is now an explicit theorem, instead of being an implicit consequence of a set of 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
Notes
- 1.
Following the Coq tradition, we represent sets [resp. binary relations] as unary [resp. binary] predicates on types, with \(\lambda \) as the binding symbol for abstraction. For instance, the set of even natural numbers is described by the predicate \(\lambda \,i:\mathbb {N},\,\exists \,j:\mathbb {N},\,i=2\times j\).
References
J-R. Abrial, Modeling in Event-B - System and Software Engineering (Cambridge University Press, Cambridge, 2010)
The Rodin development team. The Rodin Tool.https://sourceforge.net/projects/rodin-b-sharp/
G. Tel, Introduction to Distributed Algorithms (Cambridge University Press, Cambridge, 2000)
The Coq development team. The Coq proof assistant. coq.inria.fr
Xavier Leroy, Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)
G. Gonthier, Formal proof – the four-color theorem. Not. Am. Math. Soc. 55(11) (2008)
Inria Marelle Team. Proof of the Feit-Thompson theorem. https://gforge.inria.fr/projects/coqfinitgroup/
B.C. Pierce et al., Software foundations. https://softwarefoundations.cis.upenn.edu/current/index.html
Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions (Springer, Berlin, 2004)
A. Chlipala, Certified Programming with Dependent Types. (MIT Press, Cambridge, 2013)
G. Babin, Y.A. Ameur, M. Pantel, Correct instantiation of a system reconfiguration pattern: A proof and refinement-based approach, in 17th IEEE International Symposium on High Assurance Systems Engineering, HASE 2016, Orlando, FL, USA, January 7-9, 2016 (2016), pp. 31–38
Acknowledgements
This work has been supported by the project Impex of the French “Agence Nationale de la Recherche”. We thank the referees for their many helpful comments on this chapter.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Singapore Pte Ltd.
About this chapter
Cite this chapter
Castéran, P. (2021). An Explicit Semantics for Event-B Refinements. In: Ait-Ameur, Y., Nakajima, S., Méry, D. (eds) Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems. Springer, Singapore. https://doi.org/10.1007/978-981-15-5054-6_8
Download citation
DOI: https://doi.org/10.1007/978-981-15-5054-6_8
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-15-5053-9
Online ISBN: 978-981-15-5054-6
eBook Packages: Computer ScienceComputer Science (R0)