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

Formal software engineering teaching based on Event-B method and Rodin

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

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 im- portant supplement of software engineering teaching, teaching formal software engineering based on E-vent-B method and Rodin helps students understand the refinement concept in software engineering, and master the technique of developing trusty-worth software.