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

Example of a mode diagram with three modes and three transitions

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.

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.

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.

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/FT Views development process

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.

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.

Train drive mode refined

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.

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

Proof obligations

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.

• $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
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') \land A(v')] \lor [\lnot A(v') \land (A_1(v') \lor ... A_n(v'))]$	All the events of a mode must satisfy the mode guarantee and reestablish the assmumption. If the same event is used for outgoing transitions - it must satisfy the assumptions of one of the target modes and invalidate the source assumption
event_name/view_name/EVT_A	$I(v) \land H(v) \implies A_1(v) \lor \dots \lor A_k(v) \lor A_{tr1} \lor \dots \lor A_{trn}$	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, $A_{tr1} - A_{trn}$ are assumptions of the modes of which outgoing transitions are 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.

For deeper explanation of these POs please refer to the papers from the references section.

Fault Tolerance

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

The FT elements that can be added to the modal diagrams include two types of transition specialisation - error and recovery. An error always originates in a normal mode and leads to switching to a degraded or a recovery mode. A recovery transition switches back from the recovery mode to the normal one. Note that mode attribution to the specific type is relative and is not regulated by the tool. It is a design choice of which modes to be considered normal and which degraded/recovery.

Emergency stop is now a recovery mode which is triggerd by (red) error transitions

There are additional structural checks which the tool performs over the FT transitions:

• A normal transition can be refined by an error/recovery, but an FT-related transitions cannot be refined by a normal one.
• An error must be refined only by finer errors, and a recovery must be refined only by finer recoveries.
• If thers is an error leading from mode A to mode B then there must be either a recovery transition from B to A or no transitions at all.
• Cycles made of error transitions are not allowed.

In our example, we already have a second-level diagram. One of the modes (emergency_stop) clearly has relevance to extreme and dangerous situations which must be captured by the safety and FT-related requirements. Among the reasons to trigger the emergency_stop mode can be device failures and environmental hazards. The decision to trigger can be made either by a personnel or a computer, in both cases it is a rare abnormal situation. We can highlight this fact on our diagram by adding abstract errors leading to this mode and a recovery transition which eventually stops the system. Note that we have removed the switch to the manual driving mode, otherwise this would violate the error-recovery cycles rule (there would be a transition path from the recovering emergency_stop mode to the normal driving modes without a recovery transition).

How to

Editing a mode view

Install

1. Go to Help -> Install New Software -> Available Software Sites -> Add. Location of the update site is http://rodinmodeftview.sourceforge.net/
2. In the Install window select the newly added site, deselect the "Group items by category" item - the Mode/FT Views plugin should appear
3. Select the plugin and click Next until installed. Agree with any licences

Create a diagram

1. Run the usual wizard selection window. RMB on the project -> New -> Other, or New -> Other from the main menu, or simply Ctrl+N
2. Select the Mode Diagram wizard under the Event-B folder
3. Select the folder/project to contain the mode view, and type the name. Click Finish

Add diagram elements

1. Click on the required element on the right side of the editor. There are two palettes - Modes and FT
2. For modes - click or span the mode over the canvas, for transitions - drag it from the source to the destination mode

Edit elements' properties

1. Make sure you see the Properties view in your eclipse perspective. You can open it by clicking on Window -> Show View -> Properties on the main menu
2. Select the element you would like to edit - the properties will appear in the Properties view

Properties of the modes: Assumption, Guarantee, Name, Events (a list of events from the model separated with commas), Refines (the name of the abstract mode). A list of abstract modes that can be refined appears under the Refines field only if the containing mode view defined the Refines property.

Properties of the transitions: Name, Events (a list of events from the model separated with commas). Modes and transitions can also be renamed by selecting the element and pressing F2.

Click on the canvas background to select the view. Properties of the mode views: Machine (the name of the Event-B machine), Refines (the name of the abstract mode view).

Run a static check / build POs

A static check of the view will be run each time the view is saved or the abstract view is saved. Errors if any will appear under the usual Eclipse "Problems" view. Additionally, any error concerned with specific diagram element will be shown on the element as a red cross at the corner. If you point the mouse to that cross and hold a second, you will see the same error message as in the "Problems" log. The errors messages are generally comprehensible and reflect the rules for building modal views. However, currently they do not show the unproved POs.

If the static check is successful, a number of POs will be generated for the referenced machine. Even if there are SC errors, the POs which are related to the statically correct elements will still be generated.

FAQs

1. How do I get my .mode file into a particular machine? When a mode diagram is created, it appears in the project explorer at the project level, rather than within a particular machine. No amount of dragging and dropping in the project explorer will move it, but the move is very simple. Simply select the mode diagram and edit the "Machine" valid in its "Core" properties. This is a pull-down list containing all the possible machines.

Version changes

Version 1.0.1 is compatible with Rodin 2.1 and later versions

---

Version 1.0.1 for Rodin 2.0.1

---

Version 1.0.0 for Rodin 2.0

---

Dependencies between views and models resolved. Changing the model leads to SC of views.

Model keeps a single stub telling that it has at least one view.

The tool adds and removes builder configurations properly. Cleans the configurations of models when views are deleted.

Version 0.2.1

---

Changes to POs. Now a single EVT_G po is covering the link between events and associated modes and transitions. SWITCH po is removed. This allows to use non-deterministic assignments in events for both modes and transitions (which is typical for abstract models).

Version 0.1.1

---

Bug with builder configurations solved. Now mode views properly edit builder configurations of the models.

References

Papers on modal specifications:

• A.Iliasov, A.Romanovsky, F.L.Dotti. Structuring Specifications with Modes. Fourth Latin-American Symposium on Dependable Computing - LADC 09, September 1-4, 2009
• F.L.Dotti, A.Iliasov, L.Riberiro, A.Romanovsky. Modal Systems: Specification, Refinement and Realisation. In: International Conference on Formal Engineering Methods - ICFEM 09 , December 9 -12, 2009, Rio de Janeiro, Brazil

Fault tolerance:

• I.Lopatkin, A.Iliasov, A.Romanovsky. On Fault Tolerance Reuse during Refinement. In: 2nd International Workshop on Software Engineering for Resilient Systems - SERENE 2010, April 13-16, 2010, London

Examples:

• Toy train example
• AOCS case study

Complete developments:

• Sluice gate case study. Thesis version
• AOCS case study. Thesis version