Translation from Event-B into Eiffel
https://doi.org/10.18255/1818-1015-2018-6-623-636
Abstract
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.
About the Authors
Sofia Reznikova
Innopolis University
Russian Federation
Russian Federation
undergraduate student
1 Universitetskaya St., Innopolis 420500
Victor Rivera
Innopolis University
Russian Federation
Russian Federation
Assistant Professor
1 Universitetskaya St., Innopolis 420500
Joo Young Lee
Innopolis University
Russian Federation
Russian Federation
Assistant Professor
1 Universitetskaya St., Innopolis 420500
Manuel Mazzara
Innopolis University
Russian Federation
Russian Federation
Associate Professor
1 Universitetskaya St., Innopolis 420500
References
1. Abrial J.-R., Modeling in Event-B: System and Software Engineering, Cambridge University Press, New York, 2010.
2. Catan ̃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.
3. Catan ̃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.
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.
6. Mazzara M., “Deriving specifications of dependable systems: toward a method”, 12th European Workshop on Dependable Computing (EWDC), 2009.
7. M ́ery 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.
9. Naumchev A., Meyer B., “Complete contracts through specification drivers”, CoRR, 2016, abs/1602.04007.
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.
11. Reznikova S., Innopolis thesis, 2018, https://github.com/sonyareznikova/ InnopolisThesis.
12. Rivera V., Bhattacharya S., Catan ̃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., Catan ̃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.
14. Rivera V., Catan ̃o N., Wahls T., Rueda C., “Code generation for Event-B”, Int. J. Softw. Tools Technol. Transf., 19:1 (2017), 31–52.
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.
17. Yan Z. et al., “BPMO: semantic business process modeling and WSMO extension”, IEEE International Conference on Web Services (ICWS 2007), 2007, 1185–1186.
Review
For citations:
Reznikova S., Rivera V., Lee J.Y., Mazzara M. Translation from Event-B into Eiffel. Modeling and Analysis of Information Systems. 2018;25(6):623-636. https://doi.org/10.18255/1818-1015-2018-6-623-636
Views:
1233
Email this article 