Using The Event-B Method For Critical Systems
Event-B is a formal method for system-level modeling and analysis. Key features of Event-B are the use of set theory as a modeling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. The main use for using Event-B is to obtain a formal proof for the main safety properties of the system. Several use cases running in production now are the Ariane 5 rocket, part of the NYC subway line, and part of the Paris Métro line.
Kripke structure
It’s important to first understand what Kripke structures are and how they can be transformed into transition trees. Kripke structures consist of states, transitions, and certain labeling.
Each structure has states (S), initial state (i), relations (R) and labeling (L).
- S = {s1,s2,s3}.
- I = {s1}.
- R = {(s1,s2),(s2,s1)(s2,s3),(s3,s3)}.
- L = {(s1, {p,q}), (s2, {q}), (s3, {p})}.
By traversing these structures, it is possible to construct a traversal tree with all passing states and transitions. On this computation tree, LTL and CTL can be applied and will make everything more intuitive.
B-Method
Event-B is considered an evolution of B (also known as classical B) and was made in the 1980’s. It consists of three stages, the abstract machine, refinement, and implementation.
- abstract machine specifies the goal of the design.
- refinement should be proven to be coherent and including all the properties of the abstract machine.
- implementation is achieved when a deterministic version results from the refinement steps.
Model Checking
Model-checking provides additional guarantees of correct behavior. Event-B can be evaluated by using temporal logic, such as LTL (Linear Temporal Logic). LTL and CTL (Computation Tree Logic) are subsets of CTL* and used for verifying formal methods, each with their own specialties. LTL and CTL coincide if the model has only one path. LTL has been proposed for the verification of computer programs in 1977, four years later, in 1981, CTL and CTL model checking was invented. CTL* was defined in 1986.
LTL deals with linear-time, whereas CTL deals with branching time.
CTL (Computation Tree Logic)
CTL is made of propositional temporal logic with explicit quantification over possible future states. True and False are CTL formulas, as well as propositional variables, such as φ or ψ.
EX φ: φ holds in some next state
EF φ: along some path, φ holds in a future state
E[φ U ψ]: along some path, φ holds until ψ holds
EG φ: along some path, φ holds in every stateAX φ: φ holds in all next states
AF φ: along all paths, φ holds in a future state
A[φ U ψ]: along all paths, φ holds until ψ holds
AG φ: along all paths, φ holds in every state
By looking at the above image and investigate example EGp, it is visible that p holds in every state, along some path. With example AFp, along all paths, p holds in a future state. These trees are constructed out of Kripke structures.
other examples
- AG(EF restart): from any state, it is possible to get to the restart state.
- AG ¬bad: something ‘bad’ will never happen.
- AG(AF good): something ‘good’ will always happen.
LTL (Linear Temporal Logic)
LTL allows for a statement to be made about a trace of the computation tree, whereas CTL allows for statements to be made about all traces of the tree. If φ and ψ are LTL formulas, so are φ∧ ψ, φ∨ ψ, ¬φ, φU ψ (until), X φ(next), F φ (eventually), G φ (always). LTL is simpler than CTL and is only evaluated on one path, that’s why E and A are not applicable here.
¬ X φ = X ¬φ
F φ = true U φ
G φ = ¬ F ¬ φ
G φ = φ ∧ X G φ
F φ = φ ∨ X F φ
φ W ψ = G φ ∨ (φ U ψ)Rodin Platform
Rodin (Rigorous Open Development Environment for Complex Systems) is a platform where you can execute your Event-B programs and use formal proofs on them to validate their correctness. It’s an open toolset for modeling and reasoning in Event-B. A cheat sheet can be found here.
It’s possible to write your own traffic lights program in Event-B. It is possible to define a context from which the machines will get their information. Contexts contain the static structure of the system: sets, constants, and axioms. Axioms define the main properties of sets and constants. On the other hand, machines contain the dynamic structure of the system: variables, invariants, and events.
These snippets are representations of the actual files for better readability obtained by using eventb-to-txt. Full files can be found at my Github. I use ProB for model checking, this can be installed from within the Rodin UI. ProB is a constraint solver and model checker for the B-Method.
We then define machines that can be refined later on. This is a machine M0 which defines variables such as cars_go and pedestrians_go.
After defining our base machine, this can be refined by machine M1. Which adds pedestrians_colour and cars_colours. Implementation step is reached after the final refinement from machine M0 to machine M1. Using the model checking facilities available in the Rodin platform, the consistency of our model is verified and there are no deadlocks or invariant violations.
TL;DR
Several use cases running in production now are the Ariane 5 rocket, part of the NYC subway line, and part of the Paris Métro line. The main use for using Event-B is to obtain a formal proof for the main safety properties of the system. Event-B can be evaluated by using LTL (Linear Temporal Logic) and CTL (Computation Tree Logic). Rodin is a platform where you can execute your Event-B programs and use formal proofs on them to validate their correctness. It’s an open toolset for modeling and reasoning in Event-B.
