Difference between revisions of "Mode/FT Views"

From Event-B
Jump to navigationJump to search
imported>Ilya.lopatkin
m
imported>Ilya.lopatkin
m
Line 1: Line 1:
 
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.
 
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]].
+
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 ====
 
==== Development process ====
Line 37: Line 37:
 
* Mode detalisation
 
* Mode detalisation
 
** Each abstract mode must be refined by at least one concrete mode.
 
** 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.
+
** 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 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.
 
* 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.
Line 44: Line 44:
 
==== Rules for building views ====
 
==== 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.
+
* 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.
 
* 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 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.
Line 52: Line 52:
  
 
==== Proof obligations ====
 
==== Proof obligations ====
 +
The tool generates a number of proof obligations for a user.
 +
* <math>I</math> - invariant
 +
* <math>J</math> - gluing invariant
 +
* <math>H, S</math> - event guard and action respectively
 +
* <math>A, G</math> - mode assumption and guarantee respectively
 +
* <math>A_i, G_i, A_j, G_j</math> - assumption/guarantees of source and target modes for transition POs
 +
* <math>v, v'</math> - model variables and after-values (in before-after predicates)
 +
* <math>u, u'</math> - model variables and after-values of a concrete model/view (where detalisation conditions involved)
 +
 +
{| class="wikitable" border="1" cellpadding="5" cellspacing="0"
 +
|-
 +
! Name
 +
! PO
 +
! Description
 +
|-
 +
| view_name/COVER
 +
| <math>I(v) \implies A_1 \lor A_2 \lor \dots \lor A_n</math>
 +
| The mode assumptions exhaust the invariant and thus cover all the system states
 +
|-
 +
| view_name/mode_name/FIS
 +
| <math>I(v) \land A(v) \implies \exists v' \cdot G(v,v')</math>
 +
| 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
 +
| <math>I(v) \land A(v) \land G(v,v') \implies I(v')</math>
 +
| Mode guarantee preserves the invariant
 +
|-
 +
| view_name/mode_name/INTERNAL
 +
| <math>I(v) \land G(v,v') \implies A(v')</math>
 +
| Internal transition condition. Mode guarantee preserves the mode assumption
 +
|-
 +
| event_name/view_name/transition_name/SWITCH
 +
| <math>I(v) \land H(v) \land S(v,v') \implies A_i(v) \land A_j(v')</math>
 +
| Switching transition. Source mode assumption held before transition, and transition enabled the target mode
 +
|-
 +
| event_name/view_name/transition_name/INITIALISATION
 +
| <math>I(v) \land S(v,v') \implies A_j(v')</math>
 +
| Initialisation transition enables the target mode.
 +
|-
 +
| event_name/view_name/mode_name/EVT_G
 +
| <math>I(v) \land A(v) \land H(v) \land S(v,v') \implies G(v,v')</math>
 +
| All the events of a mode must satisfy the mode guarantee
 +
|-
 +
| event_name/view_name/EVT_A
 +
| <math>I(v) \land H(v) \implies A_1(v) \lor \dots \lor A_k(v)</math>
 +
| The partitioning of the events into modes must be in agreement with the event guards. <math>A_1 - A_k</math> are assumptions of the modes associated with the event
 +
|-
 +
| view_name/mode_name/ENBL
 +
| <math>I(v) \land A(v) \implies H_1(v) \lor \dots \lor H_k(v)</math>
 +
| 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
 +
| <math>J(v,u) \land A(v) \implies A_1(u) \land \dots \land A_k(u)</math>
 +
| Assumption detalisation condition. Assumptions of concrete modes must be weaker than the abstract one.
 +
|-
 +
| view_name/abstract_mode_name/REF_G
 +
| <math>J(v,u) \land (G_1(u,u') \lor \dots \lor G_k(u,u')) \implies G(v,v')</math>
 +
| Guarantee detalisation condition. Guarantees of concrete modes must be stronger than the abstract one.
 +
|}

Revision as of 18:25, 19 August 2010

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