maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2018-6-623-636mais-763Research ArticleОригинальные статьиArticlesПеревод моделей Event-B в EiffelTranslation from Event-B into Eiffelhttps://orcid.org/0000-0003-4616-2729РезниковаСофьяReznikovaSofia

студент-бакалавр

ул. Университетская, 1, Иннополис 420500

undergraduate student

1 Universitetskaya St., Innopolis 420500

s.reznikova@innopolis.ruhttps://orcid.org/0000-0002-1946-8979РивераВикторRiveraVictor

доцент

ул. Университетская, 1, Иннополис 420500

Assistant Professor

1 Universitetskaya St., Innopolis 420500

v.rivera@innopolis.ruhttps://orcid.org/0000-0001-5421-730XЛиДжу ЙонгLeeJoo Young

доцент

ул. Университетская, 1, Иннополис 420500

Assistant Professor

1 Universitetskaya St., Innopolis 420500

j.lee@innopolis.ruhttps://orcid.org/0000-0002-3860-4948МаццараМануэльMazzaraManuel

профессор

ул. Университетская, 1, Иннополис 420500

Associate Professor

1 Universitetskaya St., Innopolis 420500

m.mazzara@innopolis.ruУниверситет ИннополисРоссияInnopolis UniversityRussian Federation201819122018256623636Copyright © Резникова С., Ривера В., Ли Д.Й., Маццара М., 20182018Резникова С., Ривера В., Ли Д.Й., Маццара М.Reznikova S., Rivera V., Lee J.Y., Mazzara M.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/763

Формальные языки моделирования играют важную роль в разработке программного обеспечения, так как позволяют пользователям, во-первых, определять функциональные требования, которые также служат документацией для проекта, а во-вторых, доказывать корректность свойств систем, что особенно важно для критических систем. Однако не существует четкого понимания того, как сопоставить формальную модель и определенный язык программирования. В качестве решения данной проблемы авторы статьи предлагают использовать возможность source-to-source соответствия между моделями, описанными на языке Event-B (языке моделирования для реактивных приложений и систем), и программами на объектно-ориентированном языке программирования Eiffel. Предложенное решение не только автоматически генерирует соответствующий модели на Event-B код на Eiffel, но также переводит свойства модели в виде контрактов. Контракты соответствуют принципу Design-by-Contract и нативно поддерживаются в Eiffel. Реализация решения доступна как плагин EB2Eiffel в Rodin (среде разработки для Event-B). Таким образом, пользователи могут разрабатывать различные системы, начиная с моделирования функциональных требований (свойств) в Event-B, затем формально доказывая корректность этих свойств в Rodin и, наконец, используя EB2Eiffel для перевода модели на язык программирования. Используя Eiffel, пользователи могут расширять и модифицировать реализацию модели и доказывать корректность измененной модели относительно ее оригинальной, изначально переведенной версии. Также в статье описан процесс тестирования EB2Eiffel разными моделями, написанными на Event-B, и представлены ограничения плагина. Статья публикуется в авторской редакции.

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.

пошаговое улучшение системDesign-by-Contractформальное моделированиереактивные приложенияEvent-BEiffelstepwise refinementDesign-by-Contractformal modellingreactive systemsEvent-BEiffelReferencesAbrial J.-R., Modeling in Event-B: System and Software Engineering, Cambridge University Press, New York, 2010.Abrial J.-R., Modeling in Event-B: System and Software Engineering, Cambridge University Press, New York, 2010.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.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.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.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.Edmunds A., Butler M., “Tool support for Event-B code generation”, Workshop on Tool Building in Formal Methods, Wiley and Sons, Quebec, Canada, 2010.Edmunds A., Butler M., “Tool support for Event-B code generation”, Workshop on Tool Building in Formal Methods, Wiley and Sons, Quebec, Canada, 2010.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.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.Mazzara M., “Deriving specifications of dependable systems: toward a method”, 12th European Workshop on Dependable Computing (EWDC), 2009.Mazzara M., “Deriving specifications of dependable systems: toward a method”, 12th European Workshop on Dependable Computing (EWDC), 2009.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.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.Meyer B., “Applying "design by contract"”, Computer, 25:10 (1992), 40–51.Meyer B., “Applying "design by contract"”, Computer, 25:10 (1992), 40–51.Naumchev A., Meyer B., “Complete contracts through specification drivers”, CoRR, 2016, abs/1602.04007.Naumchev A., Meyer B., “Complete contracts through specification drivers”, CoRR, 2016, abs/1602.04007.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.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.Reznikova S., Innopolis thesis, 2018, https://github.com/sonyareznikova/ InnopolisThesis.Reznikova S., Innopolis thesis, 2018, https://github.com/sonyareznikova/ InnopolisThesis.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.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.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.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.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.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.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.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.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.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.Yan Z. et al., “BPMO: semantic business process modeling and WSMO extension”, IEEE International Conference on Web Services (ICWS 2007), 2007, 1185–1186.Yan Z. et al., “BPMO: semantic business process modeling and WSMO extension”, IEEE International Conference on Web Services (ICWS 2007), 2007, 1185–1186.

The authors declare that there are no conflicts of interest present.