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/

[1] Abrial J.-R., Modeling in Event-B: System and Software Engineering, Cambridge University Press, New York, 2010 | Zbl

[2] Cataño N., Rivera V., “EventB2Java: A Code Generator for Event-B”, NASA Formal Methods, NFM 2016, Lecture Notes in Computer Science, 9690, Springer, Cham, 2016, 166–171 | DOI

[3] Cataño N., Rueda C., “Teaching formal methods for the unconquered territory”, Teaching Formal Methods, TFM 2009, Lecture Notes in Computer Science, 5846, Springer, Berlin–Heidelberg, 2009, 2–19 | DOI

[4] Edmunds A., Butler M., “Tool support for Event-B code generation”, Workshop on Tool Building in Formal Methods, Wiley and Sons, Quebec, Canada, 2010

[5] Hallerstede S., “On the purpose of Event-B proof obligations”, Abstract State Machines, B and Z, Lecture Notes in Computer Science, 5238, Springer, Berlin–Heidelberg, 2008, 125–138 | DOI | Zbl

[6] Mazzara M., “Deriving specifications of dependable systems: toward a method”, 12th European Workshop on Dependable Computing (EWDC) (2009)

[7] Méry D., Singh N. K., “Automatic code generation from Event-B models”, Proceedings of the Second Symposium on Information and Communication Technology, SoICT '11, ACM, New York, 2011, 179–188

[8] Meyer B., “Applying “design by contract””, Computer, 25:10 (1992), 40–51 | DOI

[9] Naumchev A., Meyer B., Complete contracts through specification drivers, 2016, arXiv: abs/1602.04007 | Zbl

[10] Naumchev A., Meyer B., Rivera V., “Unifying requirements and code: An example”, Perspectives of System Informatics, 10th International Andrei Ershov Informatics Conference, PSI 2015, Revised Selected Papers (Kazan and Innopolis, Russia, 2015), 233–244 | Zbl

[11] Reznikova S., Innopolis thesis, , 2018 https://github.com/sonyareznikova/InnopolisThesis

[12] Rivera V., Bhattacharya S., Cataño N., “Undertaking the tokeneer challenge in Event-B”, 2016 IEEE/ACM 4th FME Workshop on Formal Methods in Software Engineering, 2016, 8–14

[13] Rivera V., Cataño N., “Translating Event-B to JML-specified Java programs”, Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC'14, ACM, New York, 2014, 1264–1271 | DOI

[14] Rivera V., Cataño N., Wahls T., Rueda C., “Code generation for Event-B”, Int. J. Softw. Tools Technol. Transf., 19:1 (2017), 31–52 | DOI

[15] Rivera V., Lee J. Y., Mazzara M., “Mapping Event-B machines into Eiffel programming language”, Proceedings of 6th International Conference in Software Engineering for Defence Applications, SEDA 2018, Rome, Italy, 2018

[16] Tschannen J. et al., “AutoProof: Autoactive functional verification of object-oriented programs”, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015, Lecture Notes in Computer Science, 9035, Springer, Berlin–Heidelberg, 2015, 566–580 | DOI

[17] Yan Z. et al., “BPMO: semantic business process modeling and WSMO extension”, IEEE International Conference on Web Services (ICWS 2007), 2007, 1185–1186