Generating SPARK from Event-B, Providing Fundamental Safety and Security.

MEDI Workshops(2022)

引用 0|浏览15
暂无评分
摘要
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.
更多
查看译文
关键词
SPARK, Formal methods, Event-B, Security, Safety
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要