Mode/FT Views

The Mode/FT Views plugin is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Event-B models. Here, mode is a unit of expected system functionality under distinguished working conditions of a system. The system is a set of modes connected by transitions. Mode transitions represent the changes in working conditions due to environment or system evolution. Fault tolerance part gives two types of transition specialisation: error and recovery. Each triggers additional structural checks and reserves a place to trace FT requirements.

A Mode/FT view is a graph diagram containing modes and transitions which provide additional information necessary for establishing a formal connection with the model. The tool statically checks the views and generates a number of proof obligations.

Development process

The Mode/FT Views development process

The Mode/FT views (simply views in the rest of the page) development process is a chain of views much like Event-B models. One starts with the most abstract view and adds details on further levels. We call this process the detalisation to distinguish it from the Event-B refinement. However, we use the verb refine to talk about mode/FT elements’ references to their abstract counterparts. There shouldn’t be any confusion: a mode only refines another mode, and Event-B model can only refine another Event-B model. The detalisation process is a mirror of the Event-B refinement process on a views side.

Each view is built using a set of rules:

• simple rules applied within a single view – these are checked statically,
• detalisation rules - structural static checks plus proof obligations generated,
• Event-B linkage rules – static check against a SC-model

Disobedience to these rules leads to errors during the static check.

Each view generates a number of proof obligations to be discharged by a user. These POs formally ensure that the mode/FT view is actually a view on the model under consideration. Informally, we can say that views restrict what can be modeled in Event-B in order to meet modal and FT specifications. Note that during the development process, a model does not necessarily have to have an associated view nor it has to have only one such view. Any number of views can refer to the model – this is a design choice. On the figure, there is no view for m12 model, and the view m13.mode refines its closest abstract view (can be m11.mode for instance).

Modes and transitions

Mode is a general characterisation of a system behaviour. To match this notion in terms of Event-B models, modes are mapped into groups of events. A Mode/FT view is a set of modes providing different functionality under differing operating conditions. We use the terms assumption to denote the different operating conditions and guarantee to denote the functionality ensured by the system under the corresponding assumption. With assumption and guarantee of a mode being predicates expressed on the same variables as an Event-B machine, we are able to impose restrictions on the way modes and transitions are mapped into model events and thus cross-check design decisions in either part.

Formally, a mode is characterised by a pair $A/G$ where:

• $A$ is an assumption - a predicate over the current system state;
• $G(v,v')$ is a guarantee, a relation over the current and next states of the system; and
• vector $v$ is the set of model variables.

A system switches from one mode into another through a mode transition that non-deterministically updates the state of $v$ in such a way that the assumption of the source mode becomes false while assumption of the target mode becomes true. Let us consider two modes, $i$ and $j$. A mode transition is required to establish a new state $v'$ such that $\neg A_i(v')$ and $A_j(v')$ while it is not under obligation to respect $G_i(v,v')$.

Similar to modes, transitions are mapped into groups of events, however mode and transition events have different meanings. Mode events represent internal mode transitions which must preserve the mode assumption. Transition events represent possible switches between modes. Only one event of a group can fire a transition while all of them have to exhibit transition properties: they have to preserve a target mode assumption and negate a source mode assumption.

Detalisation conditions

The detalisation conditions force user to structure and model mode/FT features in a refinement manner. One starts with an abstract representation of the system under development and adds determinism by obeying to the detalisation rules. These rules are:

• Mode detalisation
  • Each abstract mode must be refined by at least one concrete mode.
  • Assumptions of concrete modes may be weaker than the corresponding assumption of an abstract mode, while the guarantees should be stronger (see POs explanation below). By weakening the assumptions we are widening the operating conditions of a mode, and by strengthening the guarantees we are making the system behavior in this mode more deterministic.
• New transitions can be added between concrete modes which refine the same abstract mode. It is therefore guaranteed that such transitions didn’t exist on abstract level and are a proper detalisation of an abstract mode behavior (its internal transitions).
• New transitions can be added between concrete modes which refine different abstract modes given that there are corresponding transitions between abstract modes on the abstract level.
• No transitions can be added which do not project properly into the abstract transitions. If we project all the concrete modes into their abstract counterparts, then the transitions should either project into an internal transition within a mode (that is a mode itself) or into an existing transition. For example, let us imagine two modes and a transition between them: A->B. We refine A into A1, A2, and A3, and B into B1. Now, there can be any transitions between A1, A2, A3 because we don’t see such transitions on abstract level and they are a part of internal behavior of A. There can be any transitions from A1, A2, A3 to B1 but at least one must exist to refine the A->B transition. However, no transition from B1 can exist, otherwise it would project into B->A transition which does not exist on abstract level.

Rules for building views

• All modes must have unique names with exception of the start and terminal modes which do not have names. The names are used in proof obligations.
• Every mode and transition must specify at least one event. All transitions from the start mode are implicitly mapped into INITIALISATION event.
• Each mode with exception of the start and terminal modes must specify its assumption and guarantee. Both are predicates over the model variables, guarantee is a before-after predicate (after-values are denoted with a prime). Both are checked against a statically checked Event-B model.
• Each mode must specify an abstract mode with its refines clause. An exception is when this view is the first, the most abstract one, in this case detalisation conditions are not checked and modes shouldn’t refine anything.
• Each abstract mode from the abstract view must have at least one concrete mode in the concrete view.
• Concrete modes and transitions must properly project into corresponding abstract modes and transitions.