Geodesic
Translation from Event-B into Eiffel
Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 623-636

Voir la notice de l'article provenant de la source Math-Net.Ru

Formal modelling languages play a key role in the development of software: they enable users to specify functional requirements that serve as documentation as well; they enable users to prove the correctness of system properties, especially for critical systems. However, there is still an open question on how to map formal models to a specific programming language. In order to propose a solution, this paper presents a source-to-source mapping between Event-B models, a formal modelling language for reactive systems, and Eiffel programs, an Object Oriented (O-O) programming language. The mapping not only generates an actual Eiffel code of the Event-B model, but also translates model properties as contracts. The contracts follow the Design by Contract principle and are natively supported by the programming language. The mapping is implemented in the freely available Rodin plug-in EB2Eiffel. Thus, users can develop systems (i) starting with the modelling of functional requirements (properties) in Event-B, then (ii) formally proving the correctness of such properties in Rodin and finally (iii) by using EB2Eiffel to translate the model into Eiffel. In Eiffel, users can extend/customise the implementation of the model and formally prove it against the initial model. This paper also presents different Event-B models from the literature to test EB2Eiffel and its limitations. The article is published in the authors’ wording.
Keywords: stepwise refinement, Design-by-Contract, formal modelling, reactive systems, Event-B, Eiffel. 
@article{MAIS_2018_25_6_a2,
     author = {S. Reznikova and V. Rivera and J. Y. Lee and M. Mazzara},
     title = {Translation from {Event-B} into {Eiffel}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {623--636},
     publisher = {mathdoc},
     volume = {25},
     number = {6},
     year = {2018},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a2/}
}
TY  - JOUR
AU  - S. Reznikova
AU  - V. Rivera
AU  - J. Y. Lee
AU  - M. Mazzara
TI  - Translation from Event-B into Eiffel
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2018
SP  - 623
EP  - 636
VL  - 25
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a2/
LA  - en
ID  - MAIS_2018_25_6_a2
ER  - 
%0 Journal Article
%A S. Reznikova
%A V. Rivera
%A J. Y. Lee
%A M. Mazzara
%T Translation from Event-B into Eiffel
%J Modelirovanie i analiz informacionnyh sistem
%D 2018
%P 623-636
%V 25
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a2/
%G en
%F MAIS_2018_25_6_a2
S. Reznikova; V. Rivera; J. Y. Lee; M. Mazzara. Translation from Event-B into Eiffel. Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 6, pp. 623-636. http://geodesic.mathdoc.fr/item/MAIS_2018_25_6_a2/