Advances in Model and Data Engineering in the Digitalization Era - MEDI 2022 Short Papers and DETECT 2022 Workshop Papers, Cairo, Egypt, November 21-24, 2022, Proceedings
Advances in Model and Data Engineering in the Digitalization Era - MEDI 2022 Short Papers and DETECT 2022 Workshop Papers, Cairo, Egypt, November 21-24, 2022, Proceedings
复制标题
数字化时代模型和数据工程的进展 - MEDI 2022 短论文和 DETECT 2022 研讨会论文，埃及开罗，2022 年 11 月 21-24 日，论文集
DOI：
10.1007/978-3-031-23119-3_13
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Salehi Fathabadi A
中科院分区：
文献类型：
--
作者：
Salehi Fathabadi A
Event-B 是一种形式化方法，有助于对软件和硬件系统进行严格分析和构建修正开发。 SPARK 是一种用于开发高完整性软件的计算机编程语言。将设计级别的 Event-B 与实现级别的 SPARK 联系起来，使我们能够正式验证应用程序级别需求和软件实现之间的关系。 Event-B由集成开发环境Rodin和扩展插件工具支持，支持各种验证和验证技术。然而，它缺乏支持数据结构的全面代码生成功能，无法连接到实现。在本文中，我们提出了一种将经过验证的 Event-B 模型转换为 SPARK 编程语言的工具。我们描述了翻译规则以及所提出的工具如何与 Rodin 中其他基于 EMF 的插件集成。我们通过“智能投票箱”案例研究展示了拟议的翻译规则。
Event-B is a formal method that facilitates rigorous analysis and correct-by-construction development of software and hardware systems. SPARK is a computer programming language for the development of high integrity software. Linking Event-B at design level and SPARK at implementation level allows us to formally verify the relationship between application-level requirements and software implementations. Event-B is supported by an integrated development environment, Rodin, and extension plug-in tools, enabling various validation and verification techniques. However it lacks a comprehensive code generation feature with support for data structures, to connect to implementation. In this paper, we propose a tool to translate verified Event-B models into the SPARK programming language. We describe the translation rules and how the proposed tool can be integrated with other EMF-based plug-ins in Rodin. We demonstrate the proposed translation rules through a ‘smart ballot box’ case study.