2.1 Outline

Background before getting started (2.2)

We give a brief description of what Event-B is, what it is being used for and what kind of background knowledge we expect.

Installation (2.3)

We guide you through downloading, installing and starting Rodin and point out platform differences. We install the provers. We list the different window views and describe what they do.

The First Machine (2.4)

We introduce our first example: a traffic light machine that uses boolean values for signals. We introduce guards, which allow the proof obligations to be automatically discharged. We explain how proof labels are read without changing to the proof perspective.

Mathematical notation (2.5)

At this point we quickly go through the most important aspects of predicate calculus and provide links to the reference chapter and to external literature. We explain everything used by the traffic light system, we introduce all data types and we provide a brief intoduction of sets and relations. We also explain the difference between predicates and expressions. For example, this is where we explain the difference between TRUE and .

Introducing Contexts (2.6)

We introduce contexts to apply the theoretical concepts that were introduced in the previous section. We use the Agatha-Puzzle as an example to step by step introduce more and more complex elements. We cover theorems and also mention well-definedness.

Event-B Concepts (2.7)

This is another theoretical section that provides more background information about the previous examples. We analyze the anatomy of a machine and introduce all the elements that a machine or context may have. We describe the sees and refines concepts which will be applied in the next section, and we briefly mention concepts like data refinement and witnesses although we do not explain them in detail.

Expanding the Traffic Light System (2.8)

We apply what we learned in the previous section by introducing a context with traffic light colors and a refinement to integrate them. We will introduce another refinement to model the push buttons.

Proving (2.9)

So far all proof obligations have been discharged automatically. Now we switch to the proving perspective and explore it for the first time. We edit the configuration for the auto prover, invalidate proofs and show that with the new configuration they will not be discharged any more. We carry out a simple proof manually and describe the provers available.

Proving Deadlock Freeness (2.10)

In this section we define what it means for a machine to be deadlock free. We use a more complex example to explore how much the Rodin provers can accomplish.

Outlook (2.11)

This concludes the tutorial. We provide many links here for further reading. In particular, we reference the documentation from the Deploy project and the Rodin Wiki.