Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
The Rodin tool supports the application of the Event-B formal method. It provides core functionality for syntactic analysis and proof-based verification of Event-B models. Rodin also provides extension points for a range of additional plug-ins that enrich the core functionality through support for features such as model checking, model animation, graphical front ends, additional proof capabilities and code generation.While the B Method, developed by Jean-Raymond Abrial in the early 1990s, is focused on supporting formal development of software, Event-B broadens the perspective to cover systems; instead of just modelling software components, Event-B is intended for modelling and reasoning about systems that may consist of physical components, electronics and software. An essential difference between Event-B and the B Method is that Event-B admits a richer notion of refinement in which new observables may be introduced in refinement steps; this means that complex interactions between subcomponents may be abstracted from in early stage modelling and then introduced through refinement in incremental stages.
Schedule and organisation
The class takes place in
University of social science and humanities
10-12 Dinh Tien Hoang Street, Ben Nghe ward, District 1, Ho Chi Minh city.
Every night of the week days at 6pm plus Saturday at 1pm.
Instructions to install Rodin can be found there .Material
Some brief lecture notes. Still, the best reference is The Rodin Handbook.