There is an increasing demand for automation in system engineering, particularly for the development of complex systems, to speed up the development process and minimise the risk of coding errors. In current setting, Python has increasingly become a preferred choice for developers and industries for prototype development, particularly due to its robust ecosystem of open-source libraries and frameworks. However, it lacks safe coding features for critical systems. Formal methods are important for designing safe systems by verifying essential safety properties. Event-B and B methods are already in the core industrial practices for the verification and validation of system requirements. These verified models can be further used for code generation. However, manual code generation can be prone to errors and is often time-consuming, which may result in serious system failures. To produce safe Python code from formal models, we advocate for automating the code generation process. This paper introduces a code generation methodology, along with tool support, for generating Python code from Event-B models. Additionally, we have implemented and tested a plugin, called EB2Py, on several Event-B examples to demonstrate scalability and reliability of our approach.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Correct-by-Construction Code Generation from Event-B to Python

  • Neeraj Kumar Singh

摘要

There is an increasing demand for automation in system engineering, particularly for the development of complex systems, to speed up the development process and minimise the risk of coding errors. In current setting, Python has increasingly become a preferred choice for developers and industries for prototype development, particularly due to its robust ecosystem of open-source libraries and frameworks. However, it lacks safe coding features for critical systems. Formal methods are important for designing safe systems by verifying essential safety properties. Event-B and B methods are already in the core industrial practices for the verification and validation of system requirements. These verified models can be further used for code generation. However, manual code generation can be prone to errors and is often time-consuming, which may result in serious system failures. To produce safe Python code from formal models, we advocate for automating the code generation process. This paper introduces a code generation methodology, along with tool support, for generating Python code from Event-B models. Additionally, we have implemented and tested a plugin, called EB2Py, on several Event-B examples to demonstrate scalability and reliability of our approach.