Code generation for Event-B

详细信息    查看全文

• 作者：Víctor Rivera ; Néstor Cataño ; Tim Wahls…
• 关键词：Android ; Code generation ; Event ; B ; Formal methods ; Java ; JML ; EventB2Java ; Rodin ; Tokeneer
• 刊名：International Journal on Software Tools for Technology Transfer
• 出版年：2017
• 出版时间：February 2017
• 年：2017
• 卷：19
• 期：1
• 页码：31-52
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Software Engineering; Software Engineering/Programming and Operating Systems; Theory of Computation;
• 出版者：Springer Berlin Heidelberg
• ISSN：1433-2787
• 卷排序：19

文摘

Event-B is a modelling language and a formal methods approach for correct construction of software. This paper presents our work on code generation for Event-B, including the definition of a syntactic translation from Event-B to JML-annotated Java programs, the implementation of the translation as the EventB2Java tool, and two case studies on the use of EventB2Java. The first case study is on implementing an Android application with the aid of the EventB2Java tool, and the second on testing an Event-B specification of the Tokeneer security-critical system. Additionally, we have benchmarked our EventB2Java tool against two other Java code generators for Event-B.