2 Tutorial

The objective of this tutorial is to get you to a stage where you can use Rodin and build Event-B models. We expect you to have a basic understanding of logic and an idea why doing formal modelling is a good idea. You should be able to work through the tutorial with little or no outside help.

This tutorial covers installation and configuration for Rodin. It will teach you step by step how to build formal models. It also provides the essential theory and provides links to further information.

We attempt to alternate between theory and practical application and thereby keep you motivated. We encourage you not to download solutions to the examples but instead to actively build them up yourself as the tutorial progresses.

If something is unclear, remember to check the Reference chapter (Chapter 3) for more information.