Event-B seminar, Nov 16-17 2013, NII, Tokyo


This seminar provides introduction to the Event-B method and its supporting tool RODIN, and shows how these can be used in practice for modelling and verification of system dependability properties (safety analysis, safety cases and fault tolerance). The attendees will take part in practical sessions using the tool on their laptops.

The target audience is the engineers who would like to try the Event-B language and the RODIN tool. Previous experiences with other formal methods and mathematical logic (e.g., VDM) would increase understanding but are not mandatory.

Practical session requirements
During the practical sessions we will use a specific configuration of the Rodin Platform. To simplify installation process, we have prepared pre-configured platform version for Linux, Mac OS and Windows.

After downloading a file matching your operating system, unpack the archive in any suitable location. Following this, locate executable 'rodin' (i.e., rodin.exe) and run it. You will be presented with a workspace selection dialog. Choose any writable location on your system hard drive. The platform should start and the installation is complete.

If you would like to install and configure the platform manually or, if you are already a platform user, the following is the list of plug-ins used in the seminar:

Note that we use Platform version 2.8. However, if you are already using a slightly older version it be fine for as long as you can install the latest versions of all plug-ins.