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