Перевод моделей Event-B в Eiffel


https://doi.org/10.18255/1818-1015-2018-6-623-636

Полный текст:


Аннотация

Формальные языки моделирования играют важную роль в разработке программного обеспечения, так как позволяют пользователям, во-первых, определять функциональные требования, которые также служат документацией для проекта, а во-вторых, доказывать корректность свойств систем, что особенно важно для критических систем. Однако не существует четкого понимания того, как сопоставить формальную модель и определенный язык программирования. В качестве решения данной проблемы авторы статьи предлагают использовать возможность 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, и представлены ограничения плагина. Статья публикуется в авторской редакции.

Об авторах

Софья Резникова
Университет Иннополис
Россия

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

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



Виктор Ривера
Университет Иннополис
Россия

доцент

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



Джу Йонг Ли
Университет Иннополис
Россия

доцент

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



Мануэль Маццара
Университет Иннополис
Россия

профессор

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



Список литературы

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.


Дополнительные файлы

Для цитирования: Резникова С., Ривера В., Ли Д.Й., Маццара М. Перевод моделей Event-B в Eiffel. Моделирование и анализ информационных систем. 2018;25(6):623-636. https://doi.org/10.18255/1818-1015-2018-6-623-636

For citation: 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

Просмотров: 33

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)