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

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

作　　者：李梦君[1] 

机构地区：[1]国防科学技术大学计算机学院,湖南长沙410073

出　　处：《计算机工程与科学》2016年第A01期143-145,共3页Computer Engineering & Science

摘　　要：形式化软件工程是软件工程的重要组成部分。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.

关 键 词：形式化软件工程 Event—B方法 Rodin 

分 类 号：G642[文化科学—高等教育学]