Difference between revisions of "Event Model Decomposition"

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Pascal
Line 329: Line 329:
  
 
=== Configuration of the decomposition ===
 
=== Configuration of the decomposition ===
The end-user shall be asked to parametrize the decomposition.
+
The end-user shall be asked to parametrize the decomposition, and more precisely to:
 +
* identify event model (''i.e.'' an Event-B project) to be decomposed.
 +
* identify the sub-machines to be created.
 +
* partition the events.
 +
* indicate which invariants, axioms or theorems shall be ignored (because they are not required any longer).
  
* Identifying the event model to be decomposed
+
It is more suitable for the end-user to visualize the configuration, and as a consequence it shall preferably be performed through the Graphical User Interface of the Rodin platform.
* Identifying the sub-components to be created
+
 
* Specifying how to perform the decomposition (event partition)
+
The following dialog box, which fills these requirements, is given as an example. The left-hand side displays the non-decomposed model and the right-hand side the decomposed model. The second one is built by the user, by first adding machines and then copying events from left to right. The unchecked invariants are those to be ignored, the checked events are those to be copied (the initialization events are not copied).
* Asking for invariants and theorems that can be "forgotten" during the decomposition (because they are not required any longer by user)
 
  
 
<center>
 
<center>

Revision as of 16:34, 30 June 2009

Introduction

One of the most important feature of the Event-B approach is the ability to introduce new events during refinement steps, but a consequence is an increasing complexity of the refinement process when having to deal with many events and many state variables.

The main idea of the decomposition is to cut a model A into sub-models A_1, ..., A_n, which can be refined separately and more comfortably than the whole.

The constraint that shall be satisfied by the decomposition is that these refined models might - the recomposition will never be performed in practice - be recomposed into a whole model C in a way that guarantees that C refines A. An event-based decomposition of a model is detailed in Event Model Decomposition: the events of a model are partitioned to form the events of the sub-models. In parallel, the variables on which these events act are distributed among the sub-models.

The purpose is here to precisely describe what is required at the Rodin platform level to integrate this event model decomposition, and to explain why. The details of how it could be implemented are out of scope.

Other decomposition structures for Event-B are not considered here.

Terminology

A model can contain contexts, machines, or both. The notion of model decomposition covers on the one hand the machine decomposition, and on the other hand the context decomposition, both being interdependent. Models.png

  • Sub-machine: A machine built from a non-decomposed machine during the event model decomposition.
  • Sub-context: A context built from a non-decomposed context during the event model decomposition.
  • Shared variable: A variable of a given machine which is accessed by events distributed in distinct sub-machines (by opposition to private variable).
  • Private variable: A variable of a given machine which is only accessed by events of the same sub-machine (by opposition to shared variable).
  • External event: An event of a sub-machine which is built from an event of the non-decomposed machine, and which simulates the way the shared variables (between this sub-machine and another sub-machine) are handled in the non-decomposed machine (by opposition to internal event).
  • Internal event: An event copied from the non-decomposed machine to a sub-machine, according to the end-user specified distribution (by opposition to external event).

Note that a variable is said to be accessed when it is read or written. More precisely, such an access may be performed by a predicate (invariant, guard, witness) or in an assignment (action).

Low-level Specification

The low-level specification details through several steps how the event model decomposition shall be performed, and in which order. It establishes a distinction between the steps performed on the end-user's initiative, and the computed ones. It links when possible to the already implemented features of the Rodin platform which can be used at some steps.

Decomposition of a machine in sub-machines

The purpose of this paragraph is to specify how to decompose a machine in sub-machines.

What about the EXTENDS clause and the hierarchy of machines? Is it necessary to flatten this hierarchy?

About the variables

Some variables are needed by several sub-machines of the decomposition. As a consequence, these variables shall be replicated in the sub-machines. Beyond that, since it is not possible to ensure that such a variable will be refined in the same way in each sub-machine, they shall be given a special status (shared variable), with the limitation that they cannot be refined.

We will specify in this section how to introduce the notion of shared variable in the Rodin platform, and how to check the associated rules.

Defining a variable as shared

The following DTD excerpt describes the structure of a variable in the Rodin database:

<!ENTITY % NameAttDecl "name CDATA #REQUIRED">
<!ENTITY % CommentAttDecl "org.eventb.core.comment CDATA #IMPLIED">
<!ENTITY % IdentAttDecl "org.eventb.core.identifier CDATA #REQUIRED">

<!ELEMENT %variable; EMPTY>
<!ATTLIST %variable;
  %NameAttDecl;
  %CommentAttDecl;
  %IdentAttDecl;
  >

A first possibility to tag a variable as shared would be to add a shared specific attribute, which would be set to true if and only if the variable is shared:

<ENTITY % shared "org.eventb.core.shared CDATA #REQUIRED">

<!ELEMENT %variable; EMPTY>
<!ATTLIST %variable;
  ...
  %shared; (false|true) #REQUIRED
>

Another possibility would be to define a more generic attribute, which could take different values, according to the nature of the variable:

<ENTITY % nature "org.eventb.core.nature CDATA #REQUIRED">

<!ATTLIST %variable;
  ...
  %nature; (0|1) #REQUIRED
>

<!-- The nature attribute encodes the kind of variable:
       0: private variable
       1: shared variable
-->

The second option, which has the main advantage to be more scalable, is retained here.

Ensuring that a shared variable is not data-refined

A shared variable shall always be present in the state space of any refinement of the component. The verification shall be added to those already performed by the static checker.

Partitioning the variables in the sub-machines of the decomposition

It is assumed in this section that the events have been previously partitioned among sub-machines.

The following cases have to be taken into consideration when dealing with the variable distribution:

  • If v is a variable that is only accessed by events of a given sub-machine m, then v is a private variable of m, and it shall be moved to m.
  • If v is a variable that is accessed by events of distinct sub-machines m_1, ..., m_n, then v is a shared variable, and it shall be duplicated in all sub-machines.

If all the variables are shared at the conclusion of the partition, the end user shall be notified (it certainly means that the decomposition was not judicious).

About the events

It shall be possible to simulate the way the shared variables are handled in the non-decomposed machine. This is precisely the purpose of the so-called external events.

We will examine in this section how to define such events in the Rodin platform, how to construct them, and how to enforce the rules that apply (in particular, these events cannot be refined).

Identifying an event as external

An attribute is already defined, which is introduced below, to precise the nature of an event. A first solution would be to add another masked value (eg. 4) to encode the external status.

<!ENTITY % convergence "org.eventb.core.convergence">

<!ATTLIST %event;
  ...
  %convergence; (0|1|2) #REQUIRED
  ...
  >
  <!-- 
    The convergence attribute specifies which PO should be generated
    for the combination event / variant:
      0: ordinary event, no PO
      1: convergent event, PO to show event decreases variant
      2: anticipated event, PO to show event doesn't increase variant
  -->

Another solution would be to add a distinct external attribute, which would be set to true if and only if the event is external:

<ENTITY % external "org.eventb.core.external CDATA #REQUIRED">

<!ATTLIST %event;
  ...
  %external; (false|true) #REQUIRED
>

This solution is preferred because the notion of external event is totally orthogonal to the notion of convergence.

Constructing an external event

An external event shall be built for each event of the non-decomposed machine modifying shared variables.

As explained in the modelling language, a non-deterministic action expressed as a variable identifier, followed by \bcmin, followed by a set expression, can always be translated to a non-deterministic action made of a list of distinct variable identifiers, followed by \bcmsuch, followed by a before-after predicate.

In the same manner, a deterministic action can always be translated to a non-deterministic action, as shown in the following example. Let's consider a machine with variables x, and y. Here is an action:

x \bcmeq y is the same as x \bcmsuch\ x' = y

As a consequence, we will first focus on the construction of an external event from an event of a sub-machine M whose action relies on \bcmsuch, and then derivate the construction from an event of M whose action relies on \bcmeq or \bcmin.
e is an event of M, v_i are private variables of M, s_i are shared variables between M and the destination sub-machine (i.e. the sub-machine where the external event will be dispatched), P, P_i, Q_i are before-after predicates of M, and G is a predicate of M.

Generic construction for \bcmsuch

 e
 WHERE 
   G(v_1,...,v_n,s_1,...,s_m)~      
 THEN                  
   v_1,...,v_n,s_1,...,s_m \bcmsuch P(v1,...,v_n,s_1,...,s_m, v_1',...,v_n',s_1',...,s_m')

The first step of the construction is to replace the private variables by parameters. Note that this step is purely fictive, because assigning an event parameter is not allowed!

 e
 ANY x_1,...,x_n~
 WHERE 
   G(x_1,...,x_n,s_1,...,s_m)~      
 THEN                  
   v_1,...,v_n,s_1,...,s_m \bcmsuch P(x1,...,x_n,s_1,...,s_m, x_1',...,x_n',s_1',...,s_m')

The second step consists of adding guards to define the types of the parameters, if necessary. More precisely, a theorem shall be added for each parameter for which typing is required. The .bcm file associated to the non-decomposed machine shall be parsed in order to retrieve the typing information. TODO: Some precisions and examples should be added here.

The third and last step of the construction is to introduce an existential quantifier to resolve the invalid assignment. external\_e is the newly built external event.

 external_e
 ANY x_1,...,x_n~
 WHERE 
   G(x_1,...,x_n,s_1,...,s_m)~      
 THEN                  
   s_1,...,s_m \bcmsuch \exists y_1,...y_n.P(x1,...,x_n,s_1,...,s_m, y_1,...,y_n,s_1',...,s_m')

Derived construction for \bcmsuch

 e
 WHERE 
   G(v_1,...,v_n,s_1,...,s_m)~      
 THEN                  
   v_1 \bcmsuch P_1(v_1,...,v_n,s_1,...,s_m,v_1')
   ...
   v_n \bcmsuch P_n(v_1,...,v_n,s_1,...,s_m,v_n')
   s_1 \bcmsuch P_{n+1}(v_1,...,v_n,s_1,...,s_m,s_1')
   ...
   s_m \bcmsuch P_{n+m}(v_1,...,v_n,s_1,...,s_m,s_m')

It may alternatively be represented with a single predicate, which is an intersection of the P_1,...,P_{n+m} predicates:

 e
 WHERE 
   G(v_1,...,v_n,s_1,...,s_m)~      
 THEN                  
   v_1,...,v_n,s_1,...,s_m \bcmsuch P_1(v1,...,v_n,s_1,...,s_m,v_1') \land ... \land P_n(v_1,...,v_n,s_1,...,s_m,v_n') \land P_{n+1}(v_1,...,v_n,s_1,...,s_m,s_1') \land ... \land P_{n+m}(v_1,...,v_n,s_1,...,s_m,s_m') 
  

It is then possible to build the external event, by following the same steps of construction than for the generic case:

 external_e
 ANY x_1,...,x_n~
 WHERE 
   G(x_1,...,x_n,s_1,...,s_m)~      
 THEN                  
   s_1,...,s_m \bcmsuch \exists y_1,...y_n.(P_1(x1,...,x_n,s_1,...,s_m,y_1) \land ... \land P_n(x_1,...,x_n,s_1,...,s_m,y_n) \land P_{n+1}(x_1,...,x_n,s_1,...,s_m,s_1') \land ... \land P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m'))

Or, after applying some simplification rules:

external_e

 ANY x_1,...,x_n~
 WHERE 
   G(x_1,...,x_n,s_1,...,s_m)~      
 THEN                  
   s_1 \bcmsuch \exists y_1.(P_1(x1,...,x_n,s_1,...,s_m,y_1)) \land ... \land \exists y_n.(P_n(x_1,...,x_n,s_1,...,s_m,y_n)) \land P_{n+1}(x_1,...,x_n,s_1,...,s_m,s_1')
   ...
   s_m \bcmsuch \exists y_1.(P_1(x1,...,x_n,s_1,...,s_m,y_1)) \land ... \land \exists y_n.(P_n(x_1,...,x_n,s_1,...,s_m,y_n)) \land P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m')

Construction for \bcmeq
Additional simplification rules apply: If P_i(x_1,...,x_n,s_1,...,s_m,y_i)~ is equal to y_i = Q_i(x_1,...,x_n,s_1,...,s_m)~, then \exists y_i.P_i(x1,...,x_n,s_1,...,s_m,y_i) is always true and shall be deleted.

If P_i(x_1,...,x_n,s_1,...,s_m,s_i')~ is equal to s_i' = Q_i(x_1,...,x_n,s_1,...,s_m)~, and if there is no private variable (i.e. there is no existential quantifier on the right-hand side of the assignments), then s_i \bcmsuch P_{n+i}(x_1,...,x_n,s_1,...s_m,s_i') shall be rewritten as s_i \bcmeq Q_i(x_1,...,x_n,s_1,...,s_m).
Proof obligations generated for deterministic actions are indeed more suitable than those generated for non-deterministic actions.

Construction for \bcmin
Additional simplification rules apply: If P_i(x_1,...,x_n,s_1,...,s_m,s_i')~ is equal to s_i' \in Q_i(x_1,...,x_n,s_1,...,s_m), and if there is no private variable (i.e. there is no existential quantifier on the right-hand side of the assignments), then s_i \bcmsuch P_{n+i}(x_1,...,x_n,s_1,...s_m,s_i') shall be rewritten as s_i \bcmin Q_i(x_1,...,x_n,s_1,...,s_m).
For a given set S, proving that \exists x.x \in S (proof obligation generated from x \bcmsuch x' \in S) is indeed not as "simple" as proving that S \neq \emptyset (proof obligation generated from x \bcmin S).

Partitioning the events in the sub-machines of the decomposition

Let's first assume that the variables have been previously partitioned among sub-machines. The case where e is an event that accesses a private variable v1 associated to a sub-machine M1 and a private variable v2 associated to a sub-machine M2 cannot be successfully handled. As a consequence, the following sequence shall be followed:

  • The events shall be first partitioned, as indicated by the end-user. More precisely, machines shall be created, according to this partition. At this step, the machines shall only contain the specified events. In particular, the SEES and EXTENDS clauses shall be empty.
  • The Rodin platform shall then be able to distribute the variables, according to the event partition (see Variable partition).
  • The Rodin platform shall be able to distribute the invariants, according to the variable partition (see Invariant partition).
  • If e is an event that modifies a shared variable s (i.e. s is listed among the free identifiers on the left-hand side of an assignment), then an external event that modifies s shall be built from e in each sub-machine where s is accessed.

N.B. : Note that the construction of an external event depends on the source sub-machine (i.e. the sub-machine containing the internal event e from which the external event is to be built) and on the destination sub-machine (i.e. the sub-machine where the external event is to be built).
Building an external event from a given event e modifying a shared variable s and duplicating it in each sub-machine where s is accessed does not indeed entirely fit the requirements, as illustrated below: the sub-machine M3 does not know the shared variable s2 and the sub-machine M1 does not know the shared variable s4.

External events.png

Propagating the convergence status

A sub-machine can be seen as a new abstract machine. As a consequence, the convergence status of a given event shall be propagated in the sub-machines as described below:

  • An event tagged as ordinary in the non-decomposed machine shall remain ordinary in the sub-machine.
  • An event tagged as convergent in the non-decomposed machine shall become ordinary in the sub-machine.
  • An event tagged as anticipated in the non-decomposed machine shall remain anticipated in the sub-machine.
  • An external event shall always be declared as ordinary.

See the modelling language for precisions on the convergence status.

Propagating the inheritance status

An event (external or not) of a sub-machine shall always be declared as non-extended.

Ensuring that an external event cannot be refined

The verification shall be performed by the static checker.

Decomposing the initialization event

An initialization event shall be built in each sub-machine from the initialization event of the non-decomposed machine, and according to the distribution of the variables among these sub-machines. The construction is detailed below. initialization is the initial event and e the built event, x_i are variables (private or shared) of the sub-machine containing e, y_i are variables of other sub-machines, P is a before-after predicate and G is a predicate.

 initialization
 WHERE 
   G(x_1,...,x_n,y_1,...,y_m)~      
 THEN                  
   x_1,...,x_n,y_1,...,y_m \bcmsuch P(x1,...,x_n,y_1,...,y_m,x_1',...,x_n',y_1',...,y_m')

Only the variables of the considered sub-machine shall appear in the built initialization event; other variables shall become bound:

 e
 WHERE 
   G(x_1,...,x_n)~      
 THEN                  
   x_1,...,x_n \bcmsuch \exists z_1,...,z_m.P(x1,...,x_n,y_1,...,y_m,x_1',...,x_n',y_1,...,y_m')

The derived cases and simplification rules introduced during the construction of the external events apply here as well.

About the invariants

We will see in this section how to distribute the invariants among the sub-machines, once the variables have been partitioned.

  • Case 1: If i is an invariant only involving private variables, then it shall be copied in the sub-machines containing these variables.
  • Case 2: If i is an invariant only involving shared variables, then it shall be copied in the sub-machines containing these variables.
  • Case 3: If i is an invariant involving private variables and shared variables, then it shall not be copied.

If an invariant involving a private variable and a shared variable is used for typing and is not copied, a problem will be detected by the static checker.

About the variants

As mentioned before, there is no convergent event in sub-machines. As a consequence, there is no need to take the variants into consideration when performing the decomposition.

Decomposition of a context in sub-contexts

The purpose of this paragraph is to specify how to decompose the contexts, according to the decomposition of the machines, and to establish how to link the sub-contexts to the sub-machines.

The hierarchy of contexts shall be first accumulated in a single context. More precisely, a new context shall be built (virtually or not), which contains all the carrier sets, constants and axioms of the hierarchy. This context is assumed to be the non-decomposed context from which the sub-contexts shall be built.
Note that it may be necessary to rename some axioms when flattening the hierarchy.

Flattening contexts.png

Then, an empty context shall be built for each sub-machine m, which shall be linked to m through its SEES clause. Note that, at the conclusion of the context decomposition, the sub-contexts that may be empty shall not be kept, and a SEES clause shall not be added to the associated sub-machines.

About the carrier sets

A carrier set shall be visible from any sub-machine that references it, through a predicate (invariant or guard) or an assignment (action). In other terms, a carrier set of a non-decomposed context shall be copied in a sub-context if and only if this set appears in a predicate or assignment of the associated sub-machine.

About the constants

Similarly, a constant of a non-decomposed context shall be copied in a sub-context if and only if it appears in a predicate or an assignment of the associated sub-machine.

About the axioms

We will see in this section how to distribute the axioms among the sub-contexts, once the carrier sets and constants have been copied.

TODO

High-level Specification

The high-level specification details how the event model decomposition shall be integrated into the Rodin platform as a new feature, by linking to the existing architecture.

Definition of the decomposition

It is necessary to first give a definition of the event model decomposition in the Rodin platform. Is it an Event-B project decomposition? Or, is it a decomposition performed from some well-identified machines and contexts of a given Event-B project?

Configuration of the decomposition

The end-user shall be asked to parametrize the decomposition, and more precisely to:

  • identify event model (i.e. an Event-B project) to be decomposed.
  • identify the sub-machines to be created.
  • partition the events.
  • indicate which invariants, axioms or theorems shall be ignored (because they are not required any longer).

It is more suitable for the end-user to visualize the configuration, and as a consequence it shall preferably be performed through the Graphical User Interface of the Rodin platform.

The following dialog box, which fills these requirements, is given as an example. The left-hand side displays the non-decomposed model and the right-hand side the decomposed model. The second one is built by the user, by first adding machines and then copying events from left to right. The unchecked invariants are those to be ignored, the checked events are those to be copied (the initialization events are not copied).

GUI.png

Execution of the decomposition

  • Generating the sub-machines
  • Generating the sub-contexts
  • Actions, menus, buttons
  • New project?

Generation of the proof obligations

TODO

  • Generating the useful proof obligations
  • Not "propagating" useless proof obligations

Mathematical Approach

The purpose of this section is to mathematically formalize the Event-B decomposition previously specified, and by the way to remove the possible remaining ambiguity.

Let's define \mathit{MACHINE} as the set of all machine handles, \mathit{EVENT} the set of all events, and \mathit{VAR} the set of all variables.

  • The distribution of the events of the non-decomposed machine among the different sub-machines (according to the end-user configuration) can be represented as with a partial function:

\mathit{partition}\in\mathit{EVENT}\pfun\mathit{MACHINE}
For a given sub-machine m, partition^{-1}[\{m\}]~ is then the set of internal events of m.

  • The access of a variable by a given event (according to the static-checker) can be expressed as:

\mathit{access}\in\mathit{EVENT}\rel\mathit{VAR}
For a given sub-machine m, (access;partition^{-1})[\{m\}]~ is then the set of variables accessed by the events contained in m.

  • The association of a variable with the events modifying this variable (according to the static-checker) can be specified as:

\mathit{modify}\in\mathit{VAR}\rel\mathit{EVENT}
For a given sub-machine m and a variable v \in (access;partition^{-1})[\{m\}], modify[\{v\}]~ is then the set of the events modifying v.

  • The construction of the external events for a sub-machine can be represented with a relation:

\mathit{extern}\in\mathit{MACHINE}\rel\mathit{EVENT}
It is computed as follows: extern = (modify;access;partition^{-1}) \setminus partition^{-1}
Thus, the external events of a given sub-machine m are events modifying the variables accessed by the internal events of m, but they are not internal events of m.

Example

The following example is taken from the Event Model Decomposition.

Decomposition.png

A non-decomposed machine has been decomposed in two sub-machines M1 and M2, as illustrated by the figure.
According to the terminology, in\_a and a\_2\_b are internal events of M1, and b\_2\_c and out\_c are internal events of M2. Concerning the variables, a and m are private variables of M1, c and p are private variables of M2, and b, r and s are shared variables.
The variables accessed by the internal events of M1 are a, m, b, r and s. The events modifying these variables are in\_a, a\_2\_b, which both are internal events of M1, and b\_2\_c, which is an internal event of M2. Thus, according to the definition given before, b\_2\_c is an external event for M1. In the same manner, a\_2\_b is an external event for M2.

N.B.: Note that the expression "is an external event for" is an extrapolation, and shall be literally interpreted as "should lead to the construction of an external event in".

Bibliography

  • J.R. Abrial, Mathematical Models for Refinement and Decomposition, in The Event-B Book, to be published in 2009 (lien externe).
  • J.R. Abrial, Event Model Decomposition, Version 1.3, April 2009.
  • M. Butler, Decomposition Structures for Event-B, in Integrated Formal Methods iFM2009, Springer, LNCS 5423, 2009 (lien externe).