Event-B seminar, Nov 16-17 2013, NII, TokyoOverview
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.
- Linux, 32 bit: download
- Linux, 64 bit: download
- Mac OS (64 bit only): download
- Windows (same version for 32 and 64 bit): download
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:
- AtelierB provers
- Theory plug-in
- Flow plug-in (install from update site iliasov.org/usecase)
- ProB animator and model checker plug-in
- Camille text editor
- Modularisation plug-in
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.