Event-B Models

This page serves as a repository for various Event-B models, usually associated with published papers.

Theories

Disclaimer: these theories are still in development, and are relatively empirical.

They have not been proven in their entirety and may contain various bugs and imprecisions.

Also, please note they have been developed using Rodin 3.4 and have not been tested with more recent of Rodin/the Theory plug-in.

Description: theories used throughout the Event-B developments on this page. They define multiple continuous domain aspects such as reals, continuity, differential equations, etc.

  • Monoid: A theory of monoids.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Group: A theory of groups.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Ring: A theory of rings.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Relation: A theory of relations (orders and such).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Reals: A theory of reals. The formalization taken here is purely axiomatic (no Dedekind cuts nor Cauchy sequences). The theory defines the RReal datatype, as well as the usual operators on reals (plus, multiply, minus, etc.). The theory also features an extensive amount of proof rules aimed at improving Rodin's proving capabilities.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Intervals: A theory of (real) intervals. This theory maily allows to define open and closed intervals (as well as unbound intervals). It also provides we theorems and proof rules for doing a bit of interval arithmetics.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Functions: A theory of functions. This theory adds to Event-B's functions a few specific capabilities, among which concepts such as continuity and derivability as well as multiple theorems to go along with this.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Piecewise: A theory of piecewise defined functions and properties. This extends the Functions theory with piecewise version of concepts (piecewise continuity/derivability, etc.).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • DiffEq: A theory of differential equations. The theory defines a special datatype (DE for Differential Equation) that represent any differential equation. Elements of this type can be created using special constructors, for instance ode to create an ODE. The theory also defines relevent concepts for differential equation (e.g. solvability) as well as operators for using them in Event-B (continuous before-after predicate, etc.)
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • ApproximationBase: Basic components for defining approximations. This theory mainly defines the DeltaApproximation axiomatic operator, corresponding to the relation approximately equals to.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Approximation: Extension of the ApproximationBase theory with useful operators (lifted version of approximation over functions, sets and so on).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)

Stopping Car Case Study

Description: stopping car case study, adapted from the work of <a href'https://link.springer.com/article/10.1007%2Fs10009-015-0367-0'>Quesel et al.</a> and studied in the paper ABZ'18 paper ("Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B").

  • SystemCtx: Context for the System machine. Mainly defines the system's state space (S).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • System: Machine representing an uncontrolled continuous system.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • StateSystemCtx: Context for the StateSystem machine. Mainly defines the system's discrete states (STATES).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • StateSystem: Machine representing an uncontrolled continuous system with a discrete controller.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • ControlledSystemCtx: Context for the ControlledSystem machine.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • ControlledSystem: Machine representing a controlled hybrid system.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • Car_C1: Context for the Car_M1 machine. This context contains every constants and functions needed by the model.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Car_M1: Machine representing the stopping car as presented in the paper.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)

Alternative Version

Description: stopping car case study as presented in the section before, but using the new version of the generic model (that is, with integrated progress and updated continuous assignment operators).

  • GenericCtx: Context for the generic machine. Mainly defines the system's state spaces.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • Generic: Machine representing the generic hybrid system.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • AutobrakeCtx: Context for the Autobrake machine.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Autobrake: Machine representing the automatic brake case study as presented in the paper.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)

Signalized Left Turn Assist Case Study

Description: signalized left turn assist (SLTA) case study, adapted from the work of Aréchiga et al. and studied in the paper ICWFS'18 ("Hybrid Systems and Event-B: A Formal Approach to Signalised Left-Turn Assist").

  • SystemCtx: Context for the System machine. Mainly defines the system's state space (S).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • System: Machine representing an uncontrolled continuous system.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • StateSystemCtx: Context for the StateSystem machine. Mainly defines the system's discrete states (STATES).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • StateSystem: Machine representing an uncontrolled continuous system with a discrete controller.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • ControlledSystemCtx: Context for the ControlledSystem machine.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • ControlledSystem: Machine representing a controlled hybrid system.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • LeftTurnAssistCtx: Context for the LeftTurnAssist machine. This context defines every needed constants and functions
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • LeftTurnAssist: Machine representing a car turning left as presented in the paper.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)

Alternative Version

Description: SLTA case study as presented in the previous section, but using the new version of the generic model (that is, with integrated progress and upgraded continuous assignment operators).

  • GenericCtx: Context for the generic machine. Mainly defines the system's state spaces.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • Generic: Machine representing the generic hybrid system.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • LeftTurnAssistCtx: Context for the LeftTurnAssist machine.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • LeftTurnAssist: Machine representing a car turning left as presented in the paper.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)

Liquid Tank Case Study

This case study is borrowed from control theory literature. The models rely on additional theories, that define a few domain-specific concepts (such as valves, flows, etc.).

The case study is presented in several architecture:

  • one controller and one tank (single-to-single)
  • one controller and several tanks (single-to-many)
  • several controllers and several tanks (many-to-many)

Theories

Description: two theories of liquid tanks, with basic concepts and differential equations to model controlled pumps.

  • Valves: A simple theory of valves. This theory defines simple facilities for dealing with valves and pumps in the water tank models.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Flow: A theory of flows. This theory defines the good properties of an ODE describing a flow (typically, an emptying flow should make the volume decrease). This is the theory defining the isFlow and isFlowODE predicates used in the models and referenced in the papers. It also defines simple differential equation templates for some particular cases.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)

Models

Description: the various models for the liquid tank cases study.

  • GenericCtx: Context of the Generic machine. It holds the system's state space (S) as well as the controller's possible discrete states (STATES).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_base_Ctx: Context for the WaterTank_base machine. This context mainly olds the basic data of the case study: Vmax, Vlow, etc.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_ode_Ctx: Context for the WaterTank_ode machine. This context does not contain anything more than WaterTank_base_Ctx.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_1Tank_Ctx: Context for the WaterTank_1Ctrl_1Tank. This context does not contian anything more than WaterTank_base_Ctx.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_2Tanks_Ctx: Context that serves as base for the WaterTank_2Tanks_Cylinder_Ctx and WaterTank_2Ctrl_2Tanks_Ctx. This context defines anything required to model the case study with 2 tanks.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_1Tank_Cylinder_Ctx: Context for the WaterTank_1Ctrl_1Tank_Cylinder. This context contains the definition required to model a tank as a cylinder (volume calculus, update constants such as Hmax, Hlow, ...).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_2Tanks_Cylinder_Ctx: Context for the WaterTank_1Ctrl_2Tanks_Cylinder machine. This context contains constants and definitions for modeling the case study of two cylinder tanks with one controller (H1,low, H2,low, etc.).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_2Ctrl_2Tanks_Ctx: Context for the WaterTank_2Ctrl_2Tanks machine. This context makes available everything needed for the many-to-many case study, and in particular boundaries for the imprecision due to state estimation.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Generic: Machinge modelling a generic hybrid system, entry point of the method.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_base: Model of an abstract tank with abstract pumps. Only the layout of the machine is given and ought to be refined.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_ode: An abstract version of the tank but forcing the use of ODEs.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_1Ctrl_1Tank: The single-to-single case: one tank controlled by one controller, refining WaterTank_base.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_1Ctrl_1Tank_Cylinder: A refinement of the WaterTank_1Ctrl_1Tank where the considered tank is a cylinder. The height of liquid is controlled (instead of the direct volume).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_1Ctrl_2Tanks_Cylinder: A refinement of WaterTank_ode consisting of one controller attached to two cylinder tanks, as presented in the TASE paper.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • WaterTank_2Ctrl_2Tanks: A refinement of WaterTank_ode featuring two tanks independently controlled by two controllers communicating in some way.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)

Planar Robot Case Study

This case study is adapted from the work of Fainekos, also studied by Girard and Pappas.

In this case study, a robot moves on a 2D plane and must visit multiple targets, while remaining in a designated area.

Similarly to the liquid tank case study, we gather domain-specific knowledge in a theory.

Theory

Description: a domain theory for planar (2D) robot movements, including controlled differential equations and adequate controls, as proposed by Feinekos.

  • PlannarControlTheory: A basic theory for defining plannar robots. This theory mainly defines structures for the plannar robot models (in particular: differential equations and controls). This is an Event-B transcription of what has been defined by Girard (see).
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)

Models

Description: models for the planar control case study.

  • GenericCtx: Context for Generic.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • Generic: Generic model.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • Robot_0_Ctx: Context for Robot_0.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Robot_0: Basic robot description. The different events are introduced with no concrete ODE.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Robot_1_Ctx: Context for Robot_0.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Robot_1: First (exact) refinement of the robot, introducing the concrete 'simple' ODE.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Robot_2_Ctx: Context for Robot_0.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Robot_2: Second (approximate) refinement of the robot, introducing the 'complex' ODE.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)

Inverted Pendulum Case Study

This case study is borrowed from control theory literature. The goal of the system is to maintain a rod with a mass at its end in a vertical position, by applying some torque at its basis.

  • InvertedPendulum: A basic theory for handling inverted pendulums, including algebraic definitions of differential equations and approximation relationship.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • GenericCtx: Context for Generic.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • Generic: Generic model.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100) (Last update: 2023-03-02 09:34:55 +0100)
  • PendulumCtx: Context for Pendulum.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • Pendulum: Model for the non-linear ("direct") version of the inverted pendulum.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • PendulumLinCtx: Context for PendulumLin.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)
  • PendulumLin: Model of the linearized version of the inverted pendulum.
    [PDF  | Text ] (Last update: 2023-03-02 09:34:55 +0100)