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. Fault tolerance part adds 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.

Overview

There exist a number of systems, many of them being safety-critical, which are modal, i.e. they are described using the notion of operation modes. Operation mode here is used to denote the expected system functionality under distinguished working conditions of the system. A modal system is a set of modes related by mode transitions. The mode transitions represent the possible changes in the working conditions of a system - environmental changes or system evolution.

Example of a mode diagram with three modes and three transitions

For example, let us consider a very abstract modal representation of a train. In our case, it has three modes and three transitions. Intuitively simple, the mode drive represents an activity when the driver performs acceleration/deceleration control. Eventually, when the train comes to stop at the station, the system switches to another mode of operation - stopped. The actual event that has led to this mode is represented by a transition train_stopped and could be triggered by a number of sensors for instance. This mode has environmental conditions and available system operations different from when the train was moving. For example, the doors now can be opened for the passengers (which wasn't allowed while moving) and maintenance carried by the staff. Likewise, when the train is ready to depart, the driver requests to close the doors (transition close_request) and the train switches to the mode doors_closing which eventually closes all the doors (doors_closed). Then, the control over the train is given back to the driver. It can be easily seen from the diagram that the train is allowed to move only after the doors are closed, and is therefore safe to passengers. This is of course a simplification, and the real modal views are much more elaborate.

As you can see, such diagrams represent possible modes and transitions of the systems in a very concise form. It focuses the modeller attention on modal specifics and thus decreases the chance of a design fault. It generally fits into the framework of architectural descriptions using separate viewpoints and stakeholder concerns (see IEEE Std 1471–2000).

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.
  • The 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 and transitions 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.

Proof obligations

The tool generates a number of proof obligations for a user.

• $I$ - invariant
• $J$ - gluing invariant
• $H, S$ - event guard and action respectively
• $A, G$ - mode assumption and guarantee respectively
• $A_i, G_i, A_j, G_j$ - assumption/guarantees of source and target modes for transition POs
• $v, v'$ - model variables and after-values (in before-after predicates)
• $u, u'$ - model variables and after-values of a concrete model/view (where detalisation conditions involved)

Name	PO	Description
view_name/COVER	$I(v) \implies A_1 \lor A_2 \lor \dots \lor A_n$	The mode assumptions exhaust the invariant and thus cover all the system states
view_name/mode_name/FIS	$I(v) \land A(v) \implies \exists v' \cdot G(v,v')$	Feasibility of a mode guarantee. There exist at least one internal transition that can take place within the mode
view_name/mode_name/inv_name/INV	$I(v) \land A(v) \land G(v,v') \implies I(v')$	Mode guarantee preserves the invariant
view_name/mode_name/INTERNAL	$I(v) \land G(v,v') \implies A(v')$	Internal transition condition. Mode guarantee preserves the mode assumption
event_name/view_name/transition_name/SWITCH	$I(v) \land H(v) \land S(v,v') \implies A_i(v) \land A_j(v')$	Switching transition. Source mode assumption held before transition, and transition enabled the target mode
event_name/view_name/transition_name/INITIALISATION	$I(v) \land S(v,v') \implies A_j(v')$	Initialisation transition enables the target mode.
event_name/view_name/mode_name/EVT_G	$I(v) \land A(v) \land H(v) \land S(v,v') \implies G(v,v')$	All the events of a mode must satisfy the mode guarantee
event_name/view_name/EVT_A	$I(v) \land H(v) \implies A_1(v) \lor \dots \lor A_k(v)$	The partitioning of the events into modes must be in agreement with the event guards. $A_1 - A_k$ are assumptions of the modes associated with the event
view_name/mode_name/ENBL	$I(v) \land A(v) \implies H_1(v) \lor \dots \lor H_k(v)$	Mode enabledness. At least one of the events of the mode must be enabled when the mode assumption holds
view_name/abstract_mode_name/REF_A	$J(v,u) \land A(v) \implies A_1(u) \land \dots \land A_k(u)$	Assumption detalisation condition. Assumptions of concrete modes must be weaker than the abstract one.
view_name/abstract_mode_name/REF_G	$J(v,u) \land (G_1(u,u') \lor \dots \lor G_k(u,u')) \implies G(v,v')$	Guarantee detalisation condition. Guarantees of concrete modes must be stronger than the abstract one.