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.

Modes 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).

Modes and transitions

Example of a mode diagram with one of the modes selected and assumption/guarantee and an event mapping specified

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 modal 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 the 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. While mode events represent internal mode transitions which must preserve the mode assumption, the transition events represent possible switches between modes. All of these events must represent the transition between the modes: they must preserve the target mode assumption and negate the source mode assumption. Transition is an instant action. If two or more events are enabled at the time of transition, the usual Event-B demonic choice is applied to choose which event fires.

Coming back to our train example, now we can annotate our modes with appropriate assumptions and guarantees, and link them to the model events. Let us denote the train modes with a set of distinct constants $\{DRIVE, STOPPED, DOORS\_CLOSING\}$ and create a variable called $mode$ which represents the current mode. Then, the assumption of our drive mode can be the predicate $mode = DRIVE$, and the guarantee $mode' = DRIVE$, and likewise for the other two modes. Now, we can map our mode drive into a group of events, e.g. $\{accelerate, decelerate, brakes\_engaged, and\_many\_others\}$, all guards and actions of which must comply with the assumption/guarantee of the mode (see a list of POs to be generated below). The same way, we can link the transition to the next mode train_stopped with some events $\{normal\_stop, emergent\_stop\}$ that should have an action $mode := STOPPED$ among others, and thus can establish the assumption of the stopped mode (again, a PO will be generated for this).

Detalisation

The mode views (simply views in the rest of the page) development process is a chain of documents 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 modal 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.

Train drive mode refined

Here are the essential points of our detalisation process:

• A view must refine no more than one abstract view (similar to Event-B models).
• Mode detalisation
  • Each mode of the view must refine a mode from the abstract view (no new modes may appear unlike Event-B events)
  • Each abstract mode must be refined by at least one concrete mode - this can be essentially the same mode but expressed on the refined model variables.
  • 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.
  • A mode specifies what it refines with its Refines property clause.
• Transition detalisation
  • 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 onto the abstract transitions. If we project all the concrete modes onto their abstract counterparts, the transitions must either project onto internal transitions within modes or onto mode-to-mode transitions.

To show how this is applied to the train example, let us refine one of the modes (drive) into three new modes auto_drive, manual_drive, and emergency_stop and add appropriate transitions. There can be any transitions between these three modes since they all represent internal behaviour in the mode drive. However, now we see two transitions which both lead to the stopped mode (emrg_stop and stop) - these initiate from different concrete modes but both refine the same abstract transition and are therefore valid. Note that we are not allowed to add transitions initiating from the stopped mode and leading to one of the new drive modes (and thus bypassing the doors_closing mode) - this would violate the abstract mode diagram since such transition didn't exist on the previous level.

The modes on a concrete level must refer to the events from the refined Event-B model now. Likewise, the assumption/guarantee pairs must be expressed on the variables of the refined model.

This way, we essentially split the modes and transitions into a number of finer ones, just like one 'splits' model events.

Fault Tolerance

Fault tolerance is a crucial property of any critical system that we need to ensure during the development process. Based on our research within the Deploy project [cite], we proposed to extend the modal views [cite] with additional FT-related elements and structural checks, to explicitly target dynamic dependability issues, and improve traceability of FT requirements.

How to use the tool

The Mode/FT Views development process

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).

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.