Difference between pages "Mathematical Language Evolution Design" and "Mode/FT Views"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
 
imported>Ilya.lopatkin
m (New page: 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 uni...)
 
Line 1: Line 1:
−
== Introduction ==
+
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]].
  
−
This document describes the modifications that occur to the Event-B mathematical language from the developer point of view.
 
−
The old language will still be recognized, in order to provide backward compatibility.
 
  
−
These changes are described from a user point of view in [[Changes to the Mathematical Language of Event-B]].
+
==== Development process ====
  
−
== Abstract Syntax Tree ==
+
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.
 +
As an output, 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).
  
−
Deprecated nodes (becoming atomic expressions):
+
Modes and transitions
−
* KPRJ1
+
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 \emph{assumption} to denote the different operating conditions and \emph{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.
−
* KPRJ2
 
−
* KID
 
  
−
New nodes:
+
Formally, a mode is characterised by a pair $A / G$ where:
−
* KPARTITION that represents the new partition predicate (multiple predicate)
+
\begin{itemize}
−
* KPRJ1_GEN that represents the generic atomic version of the first projection
+
\item $A(v)$ is an assumption - a predicate over the current system state;
−
* KPRJ2_GEN that represents the generic atomic version of the second projection
+
\item $G(v, v')$ is a guarantee, a relation over the current and next states of the system; and
−
* KID_GEN that represents the generic atomic version of the identity
+
\item vector $v$ is the set of model variables.
 +
\end{itemize}
  
−
=== Parser Changes ===
+
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')$.
  
−
The new parser has a version attribute. Depending on the version, formulas are parsed differently. Thus, the KPARTITION node is a regular identifier if version is V1. It is accepted as a keyword only from version V2.
+
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 falsify a source mode assumption.
−
Concerning identity and projections, they are recognized as non-generic with V1 and generic with V2.
 
−
The following table summarizes how tokens are processed depending on the language version:
 
  
 +
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
 +
o Each abstract mode must be refined by at least one concrete mode.
 +
o 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.
  
−
{| border="4"
+
Rules for building views
−
|+ Token Recognition
 
−
! scope=col |
 
−
! scope=col |Language V1
 
−
! scope=col |Language V2
 
−
|-
 
−
! scope=row |"partition"
 
−
|IDENT
 
−
|KPARTITION
 
−
|-
 
−
! scope=row |"id"
 
−
|KID
 
−
|KID_GEN
 
−
|-
 
−
! scope=row |"prj1"
 
−
|KPRJ1
 
−
|KPRJ1_GEN
 
−
|-
 
−
! scope=row |"prj2"
 
−
|KPRJ2
 
−
|KPRJ2_GEN
 
−
|}
 
  
−
==== Parsing ====
+
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.
  
−
FormulaFactory has new {{method|parse()}} methods with a language version argument. Existing methods default to the first version ({{class|LanguageVersion.V1}}), while becoming deprecated.
 
−
Thus, one now has to know, before parsing a formula, the version of the language it has been written with.
 
−
It also provides methods to [[#Upgrade|upgrade]] to the new language version.
 
  
−
==== Multiple Predicates / Partition ====
+
Proof obligations
−
 
 
−
A new predicate class is introduced: {{class|MultiplePredicate}}, in which the partition predicate is implemented.
 
−
A {{class|MultiplePredicate}} is a predicate that applies to a list of one or more expressions.
 
−
In a partition, all expressions must have the same type, that is the type of the partitioned set (first child).
 
−
 
 
−
==== Associativity ====
 
−
 
 
−
Newly non associative relational set operators now require parentheses around their operands for parsing to succeed. This is managed directly by the parser.
 
−
Unparsing also requires those parentheses, so the {{class|BinaryExpression}}{{method|.toString()}} method has been changed accordingly.
 
−
 
 
−
==== Visitors ====
 
−
 
 
−
Partition, identity and projections also entail new visitor methods, as follows:
 
−
 
 
−
{{class|IVisitor}} has 6 more methods:
 
−
* {{method|enterKPARTITION(MultiplePredicate)}}
 
−
* {{method|continueKPARTITION(MultiplePredicate)}}
 
−
* {{method|exitKPARTITION(MultiplePredicate)}}
 
−
* {{method|visitKID_GEN(AtomicExpression)}}
 
−
* {{method|visitKPRJ1_GEN(AtomicExpression)}}
 
−
* {{method|visitKPRJ2_GEN(AtomicExpression)}}
 
−
 
 
−
 
 
−
{{class|ISimpleVisitor}} has 1 more method:
 
−
* {{method|visitMultiplePredicate(MultiplePredicate)}}
 
−
 
 
−
Thus, implementors of those interfaces are required to implemented new methods, while subclassers of {{class|DefaultVisitor}} and {{class|DefaultSimpleVisitor}} should consider whether or not to override them.
 
−
 
 
−
 
 
−
== Upgrade ==
 
−
 
 
−
Formulas written with version {{class|V1}} will need upgrading to version {{class|V2}}. However, most of the V1 formulas will be exactly the same with V2.
 
−
A formula needs ugrading if:
 
−
* it contains one of {KPRJ1, KPRJ2, KID}
 
−
* it contains a non parenthesised sequence of relational set operators
 
−
 
 
−
In these cases an upgrade procedure will be applied to the formula using a {{class|IFormulaRewriter}}, to rewrite KPRJ1, KPRJ2, KID expressions into their generic equivalent (see [[Changes to the Mathematical Language of Event-B#Generic Identity and Projections]]).
 
−
 
 
−
Upgraded formulas can be obtained from a formula string by calling one of the new {{class|FormulaFactory}}{{method|.upgrade()}} methods.
 
−
 
 
−
=== File upgrade ===
 
−
 
 
−
Existing rodin files with V1 formulas inside need converting to V2 formulas. Concerned files are:
 
−
* Contexts
 
−
* Machines
 
−
* Proofs
 
−
 
 
−
This is managed through the version tools of the rodin core package: a new version number for each of these files represents the passing from V1 to V2 mathematical language.
 
−
The following table summarizes the correspondence between file version number and mathematical version number:
 
−
 
 
−
 
 
−
{| border="4"
 
−
|+ File / Math versions correspondence
 
−
! scope=col |
 
−
! scope=col |Math V1
 
−
! scope=col |Math V2
 
−
|-
 
−
! scope=row |Context
 
−
|<math>V < 2</math>
 
−
|<math>V \geqslant 2</math>
 
−
|-
 
−
! scope=row |Machine
 
−
|<math>V < 4</math>
 
−
|<math>V \geqslant 4</math>
 
−
|-
 
−
! scope=row |Proof
 
−
|<math>V < 1</math>
 
−
|<math>V \geqslant 1</math>
 
−
|}
 
−
 
 
−
 
 
−
In those XML files, the formulas are written inside various attributes. Existing version conversion tools (in {{package|org.rodinp.core}}) allowed making changes to the structure of the files (adding an element, renaming an attribute, …), through XSL transformations, targetting a single element to apply the conversion to.<br />
 
−
But upgrading formulas entails dealing with the contents of attributes in various elements dispatched all over the file. So, extending the conversion tools, a new conversion operation is implemented ({{class|ModifyAttribute}}) that changes the contents of an attribute, together with a new kind of file conversion: 'multiple' conversion, in contrast to 'simple' conversion. This new one allows targetting several elements through unrestricted XPath expressions.<br />
 
−
 
 
−
These new core tools extend the existing 'conversions' extension point. It now allows writing conversion extensions in {{package|org.eventb.core}} client package that target every assignment, expression or predicate in any context, machine or proof file and upgrade their contents to the new language version.<br />
 
−
 
 
−
The modifying code is delegated to the client that must provide, in the conversion extension, a class that implements {{class|IAttributeModifier}}. It builds the new string value of the attribute from the value read in the file. In our case, it builds a V2 formula that is the upgraded equivalent to the given V1 formula.
 
−
 
 
−
=== Formula upgrade ===
 
−
 
 
−
==== Formatting ====
 
−
 
 
−
Ideally, upgrading a formula would preserve its previous formatting (spaces, tabs, new lines). But this turns out being quite tricky.
 
−
Indeed, it prevents from simply rewriting the formula then applying a {{method|toString()}}, as this would totally forget and override any formatting.
 
−
Thus, we would have to write directly into the original string. Firstly find the source locations where changes will occur, then patching the formula with the new expression versions at those source locations.
 
−
 
 
−
But that leads to more complexity when we come to consider formulas that contain
 
−
* recursive relational set operators (that recursively shift source locations)
 
−
* binary operators with higher priorities nearby (that mindlessly absorb a member of the rewritten expression)
 
−
 
 
−
Let's look at the following formula:
 
−
 
 
−
<math>f \sube id(A \times id(B))</math>
 
−
 
 
−
A straight rewriting would proceed as follows:
 
−
 
 
−
* <math>f \sube id(A \times B \triangleleft id)</math> which already is false (requires parentheses)
 
−
Then, with the appropriate shift of the source location to replace the first <math>id</math> operator:
 
−
* <math>f \sube A \times B \triangleleft id \triangleleft id</math> which is even worse
 
−
 
 
−
This suggests putting parentheses around rewritten expressions. But they would sometimes be superfluous, which brings us to distinguish cases where they are needed and cases where they are not, depending on the priority of the operators nearby.
 
−
 
 
−
Considering this is going quite far, a simpler upgrade method is applied:
 
−
* if the formula does not use deprecated expressions, nor lacks parentheses around relational set operators, it is left unchanged, preserving the formatting
 
−
* it it does, it is rewritten and any previous formatting is overridden
 
−
 
 
−
==== Detecting missing parentheses ====
 
−
 
 
−
Missing parentheses can be quite easily detected, given a parsed formula and its string.
 
−
 
 
−
Using a visitor, we check each relational set expression.
 
−
 
 
−
Starting from its source location, we search the string for parentheses towards both left and right directions around the expression, skipping space characters.
 
−
If the first non space character is not the expected parenthesis, then one is missing and the formula needs upgrading to V2.
 
−
 
 
−
The fussy part is about the definition of space characters.
 
−
 
 
−
c is an Event-B white space character if one of the following holds:
 
−
* java.lang.Character.isSpaceChar(c)
 
−
* '\u0009' <= c && c <= '\u000d'
 
−
* '\u001c' <= c && c <= '\u001f'
 
−
 
 
−
A new {{method|isEventBWhiteSpace(char)}} method has been provided in {{class|FormulaFactory}} to prevent developers from worrying about the details of this matter.
 
−
 
 
−
==== Typing generic operators ====
 
−
 
 
−
The problem of typing generic operators arises when upgrading a fomula like <math>\operatorname{id(x)}</math>.
 
−
We know that, in the general case, the upgraded version is <math>x \domres \id</math>.
 
−
But which type should the generic <math>\id</math> bear ?
 
−
 
 
−
An answer is:
 
−
If the V1 operator is typed, then the V2 generic one should bear the same type.
 
−
 
 
−
Given the convention that <math>\operatorname{o}_T</math> means that <math>\operatorname{o}</math> has type <math>T</math>, this entails rewriting <math>\id_{T}(x)</math> into <math>x \domres \id_{T}</math>.
 
−
 
 
−
But then, what happens if <math>x</math> is a type expression,like <math>\mathbb{Z}</math> ?
 
−
 
 
−
We would come to rewriting <math>\id_{\mathbb{P}(\mathbb{Z}\times\mathbb{Z})}(\mathbb{Z})</math> into <math>\mathbb{Z} \domres \id_{\mathbb{P}(\mathbb{Z}\times\mathbb{Z})}</math>.
 
−
 
 
−
In this case, the domain restriction is clearly superfluous. This brings in a new rule:
 
−
If the V1 unary operator has a type expression for argument, then the V2 generic atomic one needs no domain restriction
 
−
 
 
−
Putting things together, the following table summarizes the upgrade of generic operators, based on the <math>\id</math> operator example. Similar rules apply to <math>\prjone</math> and <math>\prjtwo</math>.
 
−
{| cellspacing="10" cellpadding="10" style="text-align:center;"
 
−
! scope=col |
 
−
! scope=col |Math V1
 
−
! scope=col |Math V2
 
−
|-
 
−
! scope=row |Type expression
 
−
|<math>\id_{\mathbb{P}(\mathbb{Z}\times\mathbb{Z})}(\mathbb{Z})</math>
 
−
|<math>\id_{\mathbb{P}(\mathbb{Z}\times\mathbb{Z})}</math>
 
−
|-
 
−
! scope=row |Typed
 
−
|<math>\id_{T}(x)</math>
 
−
|<math>x \domres \id_{T}</math>
 
−
|-
 
−
! scope=row |Not typed
 
−
|<math>\id(x)</math>
 
−
|<math>x \domres \id</math>
 
−
|}
 
−
 
 
−
==== Not upgradable cases ====
 
−
 
 
−
{{TODO}}
 
−
 
 
−
== Sequent Prover ==
 
−
{{TODO}}
 
−
 
 
−
 
 
−
[[Category:Event-B]]
 
−
[[Category:Design]]
 

Revision as of 11:31, 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 (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. As an output, 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 \emph{assumption} to denote the different operating conditions and \emph{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: \begin{itemize} \item $A(v)$ is an assumption - a predicate over the current system state; \item $G(v, v')$ is a guarantee, a relation over the current and next states of the system; and \item vector $v$ is the set of model variables. \end{itemize}

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 falsify 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 o Each abstract mode must be refined by at least one concrete mode. o 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.


Proof obligations

Retrieved from ‘https://wiki.event-b.org/index.php?title=Mathematical_Language_Evolution_Design&oldid=6118’