Introduction to Event-B

Contents

What is Event-B?

System specifications are derived from requirements.
System specification is an important precursor to design, implementation and testing.
Event-B is a formal language for writing high-level specifications of computer systems.
Event-B language includes logic and set theory.
Formal specification is more precise and consistent than an informal (natural language) specification.
Event-B typically used in safety-critical applications.

A set is a collection of elements.
Elements of a set are not ordered.
Elements of a set may be numbers, names, identifiers, etc.
Sets may be finite or infinite.
Relationship between an element and a set: the element is a member of the set.

For element x and set S, we express the membership relation as follows: x ∈ S

Finite sets can be expressed by enumerating the elements within braces.
- for example: { 3, 5, 8 }, { a, b, c, d }
The cardinality of a finite set is the number of elements in that set:
- For example: card( { 3, 5, 8 } ) = 3, card( { a, b, c, d } ) = 4, card( {} ) = 0

A set S is said to be subset of set T when every element of S is also an element of T. This is written as follows: S ⊆ T
- { 5, 8 } ⊆ { 4, 5, 6, 7, 8 }
A set S is said to be equal to set T when S ⊆ T and T ⊆ S(no matter if they have the same number of elements): S = T
- { 5, 8, 3 } = { 3, 5, 5, 8 }

Union of S and T: set of elements in either S or T. S ∪ T
Intersection of S and T: set of elements in both S and T. S ∩ T
Difference of S and T: set of elements in S but not in T. S \ T

Example: {a, b, c} ∪ {b, d} = {a, b, c, d}

{a, b, c} ∩ {b, d} = {b}

{a, b, c} \ {b, d} = {a, c}

{a, b, c} ∩ {d, e, f } = {}

{a, b, c} \ {d, e, f } = {a, b, c}

Event-B context contains:
- Sets: abstract types used in specification
- Constants: logical variables whose value remain constant
- Axioms: constraints on the constants. An axiom is a logical predicate.
Event-B machine contains:
- Variables: state variables whose values can change
- Invariants: constraints on the variables that should always hold true. An invariant is a logical predicate.
- Initialisation: initial values for the abstract variables
- Events: guarded actions specifying ways in which the variables can change. Events may have parameters.

All variables and expressions in B must have a type.
- Types are represented by sets.
Let T be a set and x a constant or variable.
- x ∈ T specifies that x is of type T.
All the elements of a set must have the same type.

Basic types are introduced to represent the entities of the problem being modelled.
Types help to structure specifications by differentiating objects.
Types help to prevent errors by not allowing us to write meaningless things.
Types can be checked by computer.

The powerset of a set S is the set whose elements are all subsets of S.

This event has a parameter w representing the word that is added to the set of known words.

In both cases, result represents a the output parameter.

Specify a system that monitors users entering and leaving a building.
A person can only enter the building if they are recognised by the monitor.
The system should be aware of whether a recognised user is currently inside or outside the building.