Generating Event-B Executable Model in Python
https://doi.org/10.15514/ISPRAS-2025-37(6)-54
Abstract
The context of the research is a process of runtime verification of information security tools based on a formal model. The verification process can be divided into two stages: formal verification of a model and testing the implementation with use of the verified model. Since many models are created with formal verification in mind, there are many solutions for the first stage. At the same time, to test the implementation, it is necessary to reproduce the model behavior. This is a complex task, especially when considering the industrial application of this approach. The article proposes a possible technique for reproducing the model behavior using program code generated based on the model. The proposed technique is aimed, on the one hand, at obtaining a time-efficient process of reproducing the model behavior, and on the other hand, at increasing the readability of the program code and the visual correspondence between the code and the text of the original model. Transparency of the process is an important quality when working with critical systems, and simplicity allows for the wide application of the technology in practice.
About the Authors
Aleksei Aleksandrovich KARNOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences,
National Research University, Higher School of Economics
Russian Federation
Russian Federation
Researcher at ISP RAS. Research interests: formal specifications, verification and testing, static and dynamic analysis.
Eugeny Valerievich KORNYKHIN
Ivannikov Institute for System Programming of the Russian Academy of Sciences,
National Research University, Higher School of Economics
Russian Federation
Russian Federation
Cand. Sci. (Phys.-Math.), Associate Professor of system programming departments at Moscow State University and Senior Researcher at ISP RAS. Fields of Interest: formal deductive verification, model-based testing.
References
1. ГОСТ Р 59453.1. Защита информации. Формальная модель управления доступом. Часть 1. Общие положения: описание стандарта и тендеры. – Введен 2021-06-01 – Москва: Стандартинформ, 2021. / State Std. GOST R 59453.1. Information protection. Formal access control model. Part 1. General principles. Moscow, 2021 (in Russian).
2. ГОСТ Р 59453.2. Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификации формальной модели управления доступом. – Введен 2021-06-01 – Москва: Стандартинформ, 2021. / State Std. GOST R 59453.1. Information protection. Recommendations on verification of formal access control model. Part 2. General principles. Moscow, 2021 (in Russian).
3. ГОСТ Р 59453.3. Защита информации. Формальная модель управления доступом. Часть 3. Рекомендации по разработке. – Введен 2025-03-31 – Москва: Стандартинформ, 2025. / State Std. GOST R 59453.3. Information protection. Recommendations on verification of formal access control model. Part 3. Recommendations on development. Moscow, 2025 (in Russian).
4. ГОСТ Р 59453.4. Защита информации. Формальная модель управления доступом. Часть 4. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом. – Введен 2025-03-31 – Москва: Стандартинформ, 2025. / State Std. GOST R 59453.4. Information protection. Recommendations on verification of formal access control model. Part 4. Recommendations for verification of information security features that implement access control policies based on formal descriptions of the access control model. Moscow, 2025 (in Russian).
5. Abrial J.-R., Butler M., Hallerstede S., Hoang T., Mehta F., Voisin L. Rodin: an open toolset for modelling and reasoning in Event-B. The International Journal on Software Tools for Technology Transfer, vol. 12. Springer, 2010, pp. 447–466. DOI: 10.1007/s10009-010-0145-y.
6. Девянин П.Н., Ефремов Д.В., Кулямин В.В., Петренко А.К., Хорошилов А.В.,
7. Щепетков И.В. Моделирование и верификация политик безопасности управления доступом в операционных системах. Горячая линия – Телеком, Москва, Россия, 2019. / Devyanin P.N., Efremov D.V., Kulyamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Modeling and verification of access control security policies in operating systems. Moscow, Russia: Hotline-Telecom, 2019 (in Russian).
8. Ефремов Д.В., Копач В.В., Корныхин Е.В., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы. Труды ИСП РАН, 2021, том 33, вып. 6, стр. 15–26. DOI: 10.15514/ISPRAS-2021-33(6)-2. / Efremov D.V., Kopach V.V., Kornykhin E.V.,
9. Kulyamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Runtime verification of operating systems based on abstract models. Proceedings of ISP RAS, 2021, vol. 33, no. 6, pp. 15–26 (in Russian). DOI: 10.15514/ISPRAS-2021-33(6)-2.
10. Девянин П.Н., Леонова М.А. Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB. ПДМ, 2021, № 52, стр. 83–96. DOI: 10.17223/20710410/52/5. / Devyanin P.N., Leonova M.A. The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB. Prikladnaya Diskretnaya Matematica, 2021, no. 52, pp. 83–96, (in Russian). DOI: 10.17223/20710410/52/5.
11. Карнов А.А. Проблема неопределенности в анализе трасс на основе высокоуровневых моделей в контексте динамической верификации. Труды ИСП РАН, 2024, том 36, вып. 4, стр. 169–182. DOI: 10.15514/ISPRAS-2024-36(4)-13 / Karnov A.A. Uncertainty Problem in High-Level Model-Based Trace Analysis as Part of Runtime Verification. Proceedings of the ISP RAS, 2024, vol. 36, no. 4, pp. 169–182. (In Russian). DOI: 10.15514/ISPRAS-2024-36(4)-13
12. J.-R. Abrial, The Event-B Modelling Notation, Available at: https://wiki.event-b.org/index.php/Event-B_Modelling_Language
13. Metayer C., Voisin L., The Event-B Mathematical Language, Available at: https://wiki.event-b.org/index.php/Event-B_Mathematical_Language
14. Abrial J.-R., Hallerstede S., Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. In Fundamenta Informaticae, 2007, vol. 77, pp. 1–28. DOI: 10.5555/2366448.2366450.
15. Börger E., ASM Refinement Method. In Formal Aspects of Computing, vol. 15, pp. 237–257, Springer-Verlag, 2003. DOI: 10.1007/s00165-003-0012-7
16. Efremov D., Shchepetkov I., Runtime verification of Linux kernel security module. In International Symposium on Formal Methods, 2019, pp. 185–199. Available at: https://arxiv.org/pdf/2001.01442
17. Bartocci E., Falcone Y., Fracalanza A., Reger G. Introduction to runtime verification. In Bartocci E., Falcone Y. (editors) Lectures on Runtime Verification. Lecture Notes in Computer Science, vol. 10457, Springer, 2018. pp. 1–33. DOI: 10.1007/978-3-319-75632-5_1.
18. Leuschel M., Butler M. ProB: an automated analysis toolset for the B method. The International Journal on Software Tools for Technology Transfer, vol. 10, Springer, 2008, pp. 185–203.
19. DOI: 10.1007/s10009-007-0063-9.
20. Servat, T., BRAMA: A New Graphic Animation Tool for B Models. In Julliand, J., Kouchnarenko, O. (edsitors) Formal Specification and Development in B. Lecture Notes in Computer Science, vol. 4355. Springer, 2007. DOI: 10.1007/11955757_28
21. AnimB. Available at: https://wiki.event-b.org/index.php/AnimB
22. Code generation activity. Available at: https://wiki.event-b.org/index.php/Code_Generation_Activity
23. Wright S., Automatic generation of C from Event-B. Presented at the Workshop on Integration of Model-based Formal Methods and Tools, Bangkok, Thailand, 02 2009.
24. Cataño N., Rivera V., EventB2Java: A code generator for Event-B. In Rayadurgam, S., Tkachuk, O. (editors) NASA Formal Methods. Lecture Notes in Computer Science, vol. 9690, Springer, 2016.
25. DOI: 10.1007/978-3-319-40648-0_13.
26. A Concise Summary of the Event-B mathematical toolkit. Available at: https://wiki.event-b.org/images/EventB-Summary.pdf
27. Петренко А.К., Девянин П.Н., Ефремов Д.В., Карнов А.А., Корныхин Е.В., Кулямин В.В., Хорошилов А.В., Динамическая верификация промышленных средств защиты информации на основе формальных моделей управления доступом. Труды ИСП РАН, 2025, том 37, вып. 3, стр. 275–288. DOI: 10.15514/ISPRAS-2025-37(3)-19 / Petrenko A.K., Devyanin P.N., Efremov D.V., Karnov A.A., Kornykhin E.V., Kulyamin V.V., Khoroshilov A.V., Dynamic verification of industrial information security tools based on formal access control models. Proceedings of the ISP RAS, 2025, vol. 37, issue 3, pp. 275–288. DOI: 10.15514/ISPRAS-2025-37(3)-19
Review
For citations:
KARNOV A.A., KORNYKHIN E.V. Generating Event-B Executable Model in Python. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(6):119-138. (In Russ.) https://doi.org/10.15514/ISPRAS-2025-37(6)-54
Email this article 