基于Event-B和Rodin开展形式化软件工程教学

计算机工程与科学

基于Event-B和Rodin开展形式化软件工程教学

李梦君

(国防科学技术大学计算机学院，湖南长沙 410073)

收稿日期:2015-09-15 修回日期:2015-11-10 出版日期:2016-11-26 发布日期:2016-12-26

Formal software engineering teaching

based on EventB method and Rodin

LI Mengjun

（College of Computer,National University of Defense Technology,Changsha 410073,China）

Received:2015-09-15 Revised:2015-11-10 Online:2016-11-26 Published:2016-12-26

摘要/Abstract

摘要：

形式化软件工程是软件工程的重要组成部分。EventB方法是一种软件形式化开发方法，Rodin是支持EventB方法的开放工具集。基于EventB方法和Rodin开展形式化软件工程教学，有益于学生正确理解精化等重要的软件工程概念，理解并掌握开发可信软件的方法，是软件工程教学的重要补充。

关键词: 形式化软件工程, EventB方法, Rodin

Abstract:

Formal software engineering is one important part of software engineering. EventB method is a software formal development method, and Rodin is an open toolset of EventB method. As an important supplement of software engineering teaching, teaching formal software engineering based on EventB method and Rodin helps students understand the refinement concept in software engineering, and master the technique of developing trustyworth software.

Key words: formal software engineering, EventB method, Rodin

李梦君. 基于Event-B和Rodin开展形式化软件工程教学[J]. 计算机工程与科学.

LI Mengjun .

Formal software engineering teaching

based on EventB method and Rodin

[J]. Computer Engineering & Science.