Difference between pages "Code Generation Activity" and "Event Model Decomposition"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Pascal
 
Line 1: Line 1:
Tasking Event-B is the extension of Event-B for defining concurrent systems sharing data, for details see the [[Tasking Event-B Overview]] page. For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk
+
{{TOCright}}
=== Code Generation Feature - Version 0.2.0 For Rodin 2.3===
 
This section is undergoing maintenance. We are planning to release a new version of the code generator in the next few days.
 
===== Changes to the Tooling and Approach =====
 
The main changes are:
 
* The code generators have been completely re-written. The translators are now implemented in Java, i.e. there is no longer a dependence on the Epsilon tool set. This was undertaken for code maintenance reasons.
 
* Tasking Event-B is now integrated with the Event-B explorer.
 
* The Rose Editor is used for editing the Tasking Event-B, and
 
* a text-based editor is provided, using the Rose extension, for editing the TaskBody. This feature has been added to address some of the usability concerns. It also overcomes the 'problem' experienced with duplicate event names in a development, since the parser-builder that has been implemented automatically selects the correct event.
 
* The EMF tree editor in Rose is only used minimally; we plan enhancements to further reduce its use.
 
* Composed machines are used to store event 'synchronizations'; these are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events.
 
* The code generation approach is now extensible; new target language constructs can be added using the Eclipse extension mechanism.
 
* The translation of target's mathematical language is now specified in the theory plug-in. This improves clarity since the the translation from source to target is achieved by specifying pattern matching rules. Extensibility is also improved; the theory plug-in is used to specify new data-types, and how they are implemented.
 
* Translated code is deposited in a directory in the appropriate files. An Ada project file is generated for use with AdaCore's GPS workbench. Eventually this could be enabled/disabled in a preferences dialog box.
 
* The Tasking Event-B to Event-B translator is now properly integrated. Control variable updates to the Event-B model are made in a similar way to the equivalent updates in the state-machine plug-in. The additional elements are added to the Event-B model and marked as 'generated'. This prevents users from manually modifying them, and allows them to be removed through a menu choice.
 
  
===== Changes to the Documentation =====
+
== Introduction ==
The following Pages have been updated:
+
One of the most important feature of the Event-B approach is the possibility 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.
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Overview Tasking Event-B Overview]
 
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Tutorial Tutorial]
 
  
===== Downloads =====
+
The main idea of the decomposition is to cut a model <math>A</math> into sub-models <math>A_1, ..., A_n</math>, which can be refined separately and more comfortably than the whole.
* Rodin Update Site: ???
 
* Examples, including models used for testing: ???
 
* Sources at: ???
 
  
 +
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 <math>C</math> in a way that guarantees that <math>C</math> refines <math>A</math>. An event-based decomposition of a model is detailed in the [[#ancre_1|Event Model Decomposition]] article: 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.
  
TODO
+
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.
* Add array types.
 
* Add addressed variables (for direct read/write access to memory)
 
* Flattening of composed machines/implementation machines.
 
* Interrupts
 
  
=== Sensing and Actuating for Tasking Event-B ===
+
== Terminology ==
Version 0.1.5. Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.
+
* Event model decomposition: The decomposition of a model, as defined in [[Machines_and_Contexts_(Modelling_Language)|the modelling language]], in sub-models. Other [[#ancre_2|decomposition structures for Event-B]] are not considered here.
 +
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.
 +
* 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).
  
* The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
+
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).
  
* As in previous releases, the code generation plug-in relies on the Epsilon tool suite. Add the following Epsilon interim update site to the list of available update sites in the Eclipse menu ''help/install new software'': http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
[[Image:Models.png]]
  
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
== 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.
  
A new [http://wiki.event-b.org/index.php?title=Tasking_Event-B_Tutorial Code Generation Tutorial] has been produced, that makes use of these new features. There is an explanation of the heating controller, upon which it is based, [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
+
=== <font id="machine_decomposition">Decomposition of a machine in sub-machines</font> ===
 +
The purpose of this paragraph is to specify how to decompose a machine in sub-machines.  
  
The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ Deploy E-Prints archive] or [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
+
The hierarchy of machines (see the <math>REFINES</math> clauses) shall be first flatten (virtually or not), as illustrated below. The resulting machine is considered as being the non-decomposed machine from which the sub-machines shall be built.  
 +
<br>Note that it may be necessary to rename some variables or invariants.
  
=== The Code Generation Demonstrator for Rodin 2.1.x ===
+
<center>
 +
[[Image:Flattening_machines.png]]
 +
</center>
  
Released 24 January 2011.
+
==== 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.  
  
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
+
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.
  
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
+
===== Defining a variable as shared =====
 +
The following DTD excerpt describes the structure of a variable in the Rodin database:
  
The update-site is available through the Rodin update site in the ''Utilities'' category.
+
<!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;
 +
  >
  
The code generation tutorial examples are available for download at:
+
A first possibility to tag a variable as ''shared'' would be to add a <tt>shared</tt> specific attribute, which would be set to <tt>true</tt> if and only if the variable is ''shared'':
  
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
+
<ENTITY % shared "org.eventb.core.shared CDATA #REQUIRED">
 +
 +
<!ELEMENT %variable; EMPTY>
 +
<!ATTLIST %variable;
 +
  ...
 +
  %shared; (false|true) #REQUIRED
 +
  >
  
The code generation plug-in relies on the Epsilon tool suite. Install Epsilon manually, since the automatic install utility does not seem to work for this feature. We currently use the Epsilon interim update site available at:
+
Another possibility would be to define a more generic attribute, which could take different values, according to the nature of the variable:
  
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
+
<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
 +
-->
  
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
+
The second option, which has the main advantage to be more scalable, is retained here.
  
== Code Generation Status ==
+
===== Ensuring that a shared variable is not data-refined =====
=== Latest Developments ===
+
A shared variable shall always be present in the state space of any refinement of the component.  
* Demonstrator plug-in feature version 0.1.0
+
The verification shall be added to those already performed by the static checker. The static checker shall have a way to determine if a given variable is ''shared'' or not.
** for Rodin 2.1.x version is available.
 
  
* The Code Generation feature consists of,
+
===== <font id="var_partition">Partitioning the variables in the sub-machines of the decomposition</font> =====
** a tasking Development Generator.
+
The first question raised by the partition of the variables is whether it shall be the first stage of the decomposition, or not. Let's first suppose that the answer is "yes". The case where <math>e</math> is an event that accesses a variable <math>v1</math> associated to a sub-machine <math>M1</math> and a variable <math>v2</math> associated to a sub-machine <math>M2</math> cannot be successfully handled: should <math>e</math> be associated to <math>M1</math> or to <math>M2</math>? Moreover, contrary to the events, the variables are not essentially bearers of meanings, and they cannot by themselves guide the decomposition.
** a tasking Development Editor (Based on an EMF Tree Editor).
 
** a translator, from Tasking Development to Common Language Model (IL1).
 
** a translator, from the Tasking Development to Event-B model of the implementation.
 
** a pretty-printer for the Tasking Development.
 
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 
  
* A tutorial is available [[Code Generation Tutorial]]
+
As a consequence, it is pertinent to assume that the events have been first partitioned. The following cases have then to be taken into consideration when dealing with the variable distribution:
** Step 1 - Create the tasking development.
+
* If <math>v</math> is a variable that is only accessed by events of a given sub-machine <math>m</math>, then <math>v</math> is a ''private'' variable of <math>m</math>. It shall be moved to <math>m</math>.
** Step 2 - Add annotations.
+
* If <math>v</math> is a variable that is accessed by events of distinct sub-machines <math>m_1, ..., m_n</math>, then <math>v</math> is a ''shared'' variable. It shall be tagged as such and duplicated in all sub-machines.
** Step 3 - Invoke translators.
 
  
=== Ongoing Work ===
+
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!).
  
* Full Rodin Integration
+
==== About the events ====
* Sensed Variables
+
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.
* Branching in Shared Machines
 
  
=== Future Work ===
+
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).
* Support for Interrupts.
 
* Richer DataTypes.
 
* Accommodation of duplicate event names in tasking developments.
 
  
== Metamodels ==
+
===== Identifying an event as external =====
* In the plug-in we define several meta-models:
+
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.  
** CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either  sequential or concurrent systems.
 
** Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.  
 
** Common Language (IL1) Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.
 
  
== Translation Rules ==
+
<!ENTITY % convergence "org.eventb.core.convergence">
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
+
 +
<!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
 +
  -->
  
== Release History ==
+
Another solution would be to add a distinct <tt>external</tt> attribute, which would be set to <tt>true</tt> if and only if the event is ''external'':
=== The Code Generation Demonstrator for Rodin 1.3.x ===
 
  
 +
<ENTITY % external "org.eventb.core.external CDATA #REQUIRED">
 +
 +
<!ATTLIST %event;
 +
  ...
 +
  %external; (false|true) #REQUIRED
 +
  >
  
First release: 30 November 2010.
+
This solution is preferred because the notion of ''external'' event is totally orthogonal to the notion of convergence.
  
available from:
+
===== <font id="build_external">Constructing an external event</font> =====
 +
The construction of an ''external'' event highly relies on some [[Rewriting_rules_for_event_model_decomposition|rewriting / simplification rules]]. It is recommended to peruse them before reading further.
  
https://sourceforge.net/projects/codegenerationd/files/
+
<math>e</math> is an event of <math>M</math>, <math>v_i</math> are ''private'' variables of <math>M</math>, <math>s_i</math> are ''shared'' variables between <math>M</math> and the destination sub-machine (''i.e.'' the sub-machine where the ''external'' event will be dispatched), <math>P, P_i, Q_i</math> are before-after predicates of <math>M</math>, and <math>G</math> is a predicate of <math>M</math>.
  
The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.
+
<u>Generic construction</u>
 +
<br>We first focus on the generic construction of an ''external'' event from an event of a sub-machine <math>M</math> whose action is expressed as follows:
  
A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed - the only configuration necessary may be to switch workspace to ''<installPath>\rodin1.3bWin7\workspace''. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.
+
  e
 +
  '''WHERE'''
 +
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
 +
  '''THEN'''                 
 +
    <math>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')</math>
  
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.  
+
<ol>
 +
<li>The first step of the construction consists in replacing the ''private'' variables by parameters. Note that this step is purely fictive, because assigning an event parameter is not allowed!</li>
  
'''A step-by-step [[Code Generation Tutorial]] is available'''  
+
  e
 +
  '''ANY''' <math>x_1,...,x_n~</math>
 +
  '''WHERE'''
 +
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 +
  '''THEN'''                 
 +
    <math>x_1,...,x_n,s_1,...,s_m \bcmsuch P(x1,...,x_n,s_1,...,s_m, x_1',...,x_n',s_1',...,s_m')</math>
  
==== About the Initial Release ====
+
<li>The second step consists in 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 <tt>.bcm</tt> file associated to the non-decomposed machine shall be parsed in order to retrieve the typing information.
The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.
 
  
==== Source Code ====
+
<li>The third and last step of the construction consists in introducing an existential quantifier to resolve the invalid assignment. <math>external\_e</math> is the newly built external event.</li>
  
The sources are available from,
+
  external_e
 +
  '''ANY''' <math>x_1,...,x_n~</math>
 +
  '''WHERE'''
 +
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 +
  '''THEN'''                 
 +
    <math>s_1,...,s_m \bcmsuch \exists y_1,...y_n \qdot P(x1,...,x_n,s_1,...,s_m, y_1,...,y_n,s_1',...,s_m')</math>
 +
</ol>
  
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
+
<u>Derived constructions</u>
 +
<br>Then, it is possible to derivate the construction for other actions:
 +
# [[Rewriting_rules_for_event_model_decomposition|Rewriting rules 1 to 5]] shall be first applied as many times as possible, from left to right, to get the action into the generic form introduced before.
 +
# Then, the steps detailed for the generic construction shall be followed.
 +
# Then, the [[Rewriting_rules_for_event_model_decomposition|simplification rules 6 to 8]] shall be enforced.
 +
# Finally, the [[Rewriting_rules_for_event_model_decomposition|rewriting rules 1 to 4]] shall be applied, from right to left.  
  
Note - I used Eclipse 3.5 Galileo, and you will need to install (or have sources from) Epsilon's interim update site. There is also dependency on Camille v2.0.0
+
Thus, if <math>P_i(x_1,...,x_n,s_1,...,s_m,s_i')~</math> is equal to <math>s_i' = Q_i(x_1,...,x_n,s_1,...,s_m)~</math>, and if there is no ''private'' variable (''i.e.'' there is no existential quantifier on the right-hand side of the assignments), then <math>s_i \bcmsuch P_{n+i}(x_1,...,x_n,s_1,...s_m,s_i')</math> shall be rewritten as <math>s_i \bcmeq Q_i(x_1,...,x_n,s_1,...,s_m)</math>.
 +
<br>
 +
The proof obligations generated for deterministic actions are indeed more suitable than those generated for non-deterministic actions.
  
 +
In the same manner, if <math>P_i(x_1,...,x_n,s_1,...,s_m,s_i')~</math> is equal to <math>s_i' \in Q_i(x_1,...,x_n,s_1,...,s_m)</math>, and if there is no private variable (''i.e.'' there is no existential quantifier on the right-hand side of the assignments), then <math>s_i \bcmsuch P_{n+i}(x_1,...,x_n,s_1,...s_m,s_i')</math> shall be rewritten as <math>s_i \bcmin Q_i(x_1,...,x_n,s_1,...,s_m)</math>.
 +
<br>
 +
For a given set <math>S</math>, proving that <math>\exists x \qdot x \in S</math> (FIS proof obligation generated from <math>x \bcmsuch x' \in S</math>) is indeed not as "simple" as proving that <math>S \neq \emptyset</math> (proof obligation generated from <math>x \bcmin S</math>).
  
 +
<u>Example</u>
  
 +
  e
 +
  '''WHERE'''
 +
    <math>G(v_1,...,v_n,s_1,...,s_m)~</math>     
 +
  '''THEN'''                 
 +
    <math>\begin{array}{ll}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') \end{array}</math>
 +
 +
  external_e
 +
  '''ANY''' <math>x_1,...,x_n~</math>
 +
  '''WHERE'''
 +
    <math>G(x_1,...,x_n,s_1,...,s_m)~</math>     
 +
  '''THEN'''                 
 +
    <math>\begin{array}{ll}s_1\!\!\! &\bcmsuch P_{n+1}(x_1,...,x_n,s_1,...,s_m,s_1')\\
 +
    ...\\
 +
    s_m\!\!\! &\bcmsuch P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m') \end{array}</math>
 +
 +
In this example, the rules [[Rewriting_rules_for_event_model_decomposition#rule_4|4]], [[Rewriting_rules_for_event_model_decomposition#rule_7|7]] and [[Rewriting_rules_for_event_model_decomposition#rule_8|8]] shall be applied.
 +
 +
===== Partitioning the events in the sub-machines of the decomposition =====
 +
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 <math>SEES</math> and <math>REFINES</math> clauses shall be empty. Moreover, note that it may be necessary to rename some events when performing the partition.
 +
* The Rodin platform shall then be able to distribute the variables, according to the event partition (see [[#var_partition|Variable partition]]).
 +
* The Rodin platform shall be able to distribute the invariants, according to the variable partition (see [[#inv_partition|Invariant partition]]).
 +
* If <math>e</math> is an event that modifies a ''shared'' variable <math>s</math> (''i.e.'' <math>s</math> is listed among the free identifiers on the left-hand side of an assignment), then an ''external'' event that modifies <math>s</math> shall be built from <math>e</math> in each sub-machine where <math>s</math> 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 <math>e</math> 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).
 +
<br>
 +
Building an ''external'' event from a given event <math>e</math> modifying a ''shared'' variable <math>s</math> and duplicating it in each sub-machine where <math>s</math> is accessed does not indeed entirely fit the requirements, as illustrated below: the sub-machine <math>M3</math> does not know the ''shared'' variable <math>s2</math> and the sub-machine <math>M1</math> does not know the ''shared'' variable <math>s4</math>.
 +
 +
<center>
 +
[[Image:External_events.png]]
 +
</center>
 +
 +
===== <font id="convergence">Propagating the convergence status</font> =====
 +
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 [[Events_(Modelling_Language)|the modelling language]] for precisions on the convergence status.
 +
 +
===== Propagating the extended 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. The static checker shall have a way to determine if a given event is ''external'' or not.
 +
 +
===== 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. <math>initialization</math> is the initial event and <math>e</math> the built event, <math>x_i</math> are variables (''private'' or ''shared'') of the sub-machine containing <math>e</math>, <math>y_i</math> are variables of other sub-machines, <math>P</math> is a before-after predicate and <math>G</math> is a predicate.
 +
 +
  initialization   
 +
  '''THEN'''                 
 +
    <math>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')</math>
 +
 +
Only the variables of the considered sub-machine shall appear in the built initialization event; other variables shall become bound:
 +
 +
  e 
 +
  '''THEN'''                 
 +
    <math>x_1,...,x_n \bcmsuch \exists z_1,...,z_m \qdot P(x1,...,x_n,y_1,...,y_m,x_1',...,x_n',y_1,...,y_m')</math>
 +
 +
The derived cases and simplification rules introduced during [[#build_external|the construction of the external events]] apply here as well.
 +
 +
==== <font id="inv_partition">About the invariants</font> ====
 +
We will see in this section how to distribute the invariants among the sub-machines, once the variables have been partitioned.
 +
 +
* Case 1: If <math>i</math> is an invariant only involving ''private'' variables of a given sub-machine, then it shall be copied in this sub-machine.
 +
* Case 2: If <math>i</math> is an invariant involving ''private'' variables of distinct sub-machines, then it shall not be copied.
 +
* Case 3: If <math>i</math> is an invariant only involving ''shared'' variables, then it shall only be copied in the sub-machines containing all these variables.
 +
* Case 4: If <math>i</math> is an invariant involving ''private'' variables and ''shared'' variables, then it shall only be copied in the sub-machines containing all these variables.
 +
 +
These different cases are illustrated in the figure below, where <math>P1</math>, <math>P2</math>, <math>P3</math> and <math>P4</math> are predicates. <math>A</math> is an abstract machine, <math>C</math> is a concrete machine extending <math>A</math>, <math>M</math> is the flattened machine for <math>C</math> and <math>A</math> (see [[#machine_decomposition|how flattening a hierarchy of machines]]), and <math>M1</math>, <math>M2</math>, and <math>M3</math> are the sub-machines resulting from the decomposition of <math>M</math>. <math>v1</math> is a ''private'' variable of <math>M1</math>, <math>v2</math> is a variable ''shared'' between <math>M1</math> and <math>M2</math>, <math>v3</math> is a variable ''shared'' between <math>M2</math> and <math>M3></math>, and <math>v4</math> is a ''private'' variable of <math>M3</math>.
 +
 +
<center>
 +
[[Image:Invariants.png]]
 +
</center>
 +
 +
'''To summarize, an invariant based on a <math>P(v_m,...,v_n)~</math> predicate is copied in a sub-machine <math>M_x</math> if and only if <math>M_x</math>  contains the <math>\{v_m,...,v_n\}~</math> variables.'''
 +
 +
If an invariant is used for typing but it has not been copied, a theorem shall be added in the sub-machines for each variable for which typing is required (otherwise a problem will be detected by the static checker). Note that there is no contradiction with the requirements on [[#po|proof obligations]]; no proof obligation (PO) is indeed generated for predicates <math>v \in T</math>, where <math>v</math> is a variable and <math>T</math> is a type.
 +
 +
Beyond that, a workaround exists if an invariant <math>inv</math>, based on a <math>P(v_m,...,v_n)~</math> predicate, seems useful (for example an invariant between a concrete variable and some abstract variable) but it has disappeared in a sub-machine <math>M_x</math> containing variables <math>\{v_p,...,v_q\}~</math> (''eg.'' <math>inv2</math> and <math>inv3</math> have both been excluded from <math>M3</math> machine by application of the stated rules). It is indeed possible to add in the non-decomposed machine a theorem based on <math>P~</math>, but where the variables <math>\{v_m,...,v_n\} \setminus \{v_p,...,v_q\}</math> become bound, and then to perform again the decomposition. It will lead to a new proof obligation in the non-decomposed machine, which does not pose any difficulty.
 +
<br>For example, if a theorem <math>inv5: P5(v4)~</math>, with <math>P5 \defi \exists v1 \qdot P2(v1,v4)</math>, is added to the <math>C</math> concrete machine, then it will be copied in the sub-machine <math>M3</math> during the decomposition (see case 1). In order to prove the <math>P5~</math> statement, the bound variable <math>v1</math> shall obviously be instantiated with <math>v1</math>.
 +
 +
==== About the variants ====
 +
As mentioned [[#convergence|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.
 +
 +
=== <font id="context_decomposition">Decomposition of a context in sub-contexts</font> ===
 +
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 (see the <math>EXTENDS</math> clauses) 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.
 +
<br>Note that it may be necessary to rename some axioms when flattening the hierarchy.
 +
 +
<center>
 +
[[Image:Flattening_contexts.png]]
 +
</center>
 +
 +
Then, an empty context shall be built for each sub-machine <math>m</math>, by respecting the following sequence: the constants shall be first included, then the carrier sets shall be added, and finally the axioms shall be considered.
 +
<br>This context shall be linked to <math>m</math> through its <math>SEES</math> clause. Note that, at the conclusion of the context decomposition, the sub-contexts that may be empty shall not be kept, and a <math>SEES</math> clause shall not be added to the associated sub-machines.
 +
 +
==== About the constants ====
 +
A constant of a non-decomposed context shall be copied in a sub-context if and only if it appears in a predicate (invariant or guard) or an assignment (action) of the associated sub-machine.
 +
 +
==== About the carrier sets ====
 +
A carrier set shall be visible from any sub-machine that references it, explicitly or implicitly, through a predicate or an assignment. 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, or types a constant previously copied to this sub-context.
 +
 +
==== About the axioms ====
 +
We will see in this section how to distribute the axioms among the sub-contexts, once the constants and carrier sets have been copied.
 +
 +
As for the [[#inv_partition|invariants]], an axiom is copied in a sub-machine <math>M_x</math> if and only if <math>M_x</math> contains the referenced constants and sets. If an axiom is used for typing but it has not been copied, a theorem shall be added in the sub-contexts for each constant for which typing is required (otherwise a problem will be detected by the static checker).
 +
 +
== 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?
 +
 +
The entry point for the decomposition is a machine <math>M1</math>, its visible contexts, and its whole parent hierarchy of machines.
 +
 +
<center>
 +
[[Image:Machine.png]]
 +
</center>
 +
 +
The machine <math>M1</math> to be taken as input for the decomposition shall be pointed by the end-user. The <math>EXTENDS</math> clauses of contexts and the <math>SEES</math> clauses of machines are used to build the associated hierarchy of contexts. In the same manner, the <math>REFINES</math> clauses allow to build the associated hierarchy of machines.
 +
 +
=== Configuration of the decomposition ===
 +
The end-user shall be asked to parametrize the decomposition, and more precisely to:
 +
* identify the machine to be taken as input for the decomposition.
 +
* 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).
 +
 +
<center>
 +
[[Image:GUI.png]]
 +
</center>
 +
 +
=== Execution of the decomposition ===
 +
A <tt>Decompose</tt> action shall be added. It shall be enabled if and only if a machine is selected. It shall be available from the <tt>Project</tt> menu, from the toolbar, and in the contextual menu displayed when right-clicking on the selected project.
 +
 +
[[Image:Action.png]]
 +
 +
A new Event-B project shall be created for each sub-machine built during the configuration. The [[#machine_decomposition|decomposition of the sub-machine]] shall first be completed, and then the non-decomposed [[#context_decomposition|context shall be partitioned]], as specified before.
 +
 +
As far as possible, the developments shall not be performed in the Event-B core; the dedicated extension points shall be used instead (''eg.'' those provided for the static checker. See the <tt>plugin.xml</tt> file of the <tt>org.eventb.core</tt> package).
 +
 +
=== <font id="po">Generation of the proof obligations</font> ===
 +
A model to be decomposed is assumed to be proved, ''i.e.'' the proof obligations (PO) have all been handled successfully. The following conditions on PO shall be fulfilled during the decomposition:
 +
* The decomposition shall not generate any new proof obligation.
 +
* The proof obligations related to the non-decomposed model shall not be "propagated" to the decomposed models to be proved again. As a consequence, the Proof Obligation Generator (POG) shall be temporary disconnected until the decomposition is performed.
 +
 +
== 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 <math>\mathit{MACHINE}</math> as the set of all machine handles, <math>\mathit{EVENT}</math> the set of all events, and <math>\mathit{VAR}</math> 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:
 +
<math>\mathit{partition}\in\mathit{EVENT}\pfun\mathit{MACHINE}</math>
 +
<br>For a given sub-machine <math>m</math>, <math>partition^{-1}[\{m\}]~</math> is then the set of ''internal'' events of <math>m</math>.
 +
* The access of a variable by a given event (according to the static-checker) can be expressed as:
 +
<math>\mathit{access}\in\mathit{EVENT}\rel\mathit{VAR}</math>
 +
<br>For a given variable <math>v</math>, <math>(partition;access^{-1})[\{v\}]~</math> is then the set of the sub-machines accessing <math>v</math>, and <math>v</math> is a ''private'' variable of a sub-machine <math>m</math> if and only if this set contains a single component (''i.e.'' <math>card((partition;access^{-1})[\{v\}]) = 1~</math>); otherwise, and if and only if this set is not empty, <math>v</math> is ''shared''.
 +
<br>In parallel, for a given sub-machine <math>m</math>, <math>(access;partition^{-1})[\{m\}]~</math> is the set of variables accessed by the events contained in <math>m</math>.
 +
* The association of a variable with the events modifying this variable (according to the static-checker) can be specified as:
 +
<math>\mathit{modify}\in\mathit{VAR}\rel\mathit{EVENT}</math>
 +
<br>For a given sub-machine <math>m</math> and a variable <math>v \in (access;partition^{-1})[\{m\}]</math>, <math>modify[\{v\}]~</math> is then the set of the events modifying <math>v</math>.
 +
* The construction of the ''external'' events for a sub-machine can be represented with a relation:
 +
<math>\mathit{extern}\in\mathit{MACHINE}\rel\mathit{EVENT}</math>
 +
<br>It is computed as follows: <math>extern = (modify;access;partition^{-1}) \setminus partition^{-1}</math>
 +
<br>Thus, the ''external'' events of a given sub-machine <math>m</math> are events modifying the variables accessed by the ''internal'' events of <math>m</math>, but they are not ''internal'' events of <math>m</math>.
 +
 +
=== Example ===
 +
The following example is taken from the [[#ancre_1|Event Model Decomposition]].
 +
 +
<center>
 +
[[Image:Decomposition.png]]
 +
</center>
 +
 +
A non-decomposed machine has been decomposed in two sub-machines <math>M1</math> and <math>M2</math>, as illustrated by the figure.
 +
<br>According to the terminology, <math>in\_a</math> and <math>a\_2\_b</math> are ''internal'' events of <math>M1</math>, and <math>b\_2\_c</math> and <math>out\_c</math> are ''internal'' events of <math>M2</math>. Concerning the variables, <math>a</math> and <math>m</math> are ''private'' variables of <math>M1</math>, <math>c</math> and <math>p</math> are ''private'' variables of <math>M2</math>, and <math>b</math>, <math>r</math> and <math>s</math> are ''shared'' variables.
 +
<br>The variables accessed by the ''internal'' events of <math>M1</math> are <math>a</math>, <math>m</math>, <math>b</math>, <math>r</math> and <math>s</math>. The events modifying these variables are <math>in\_a</math>, <math>a\_2\_b</math>, which both are ''internal'' events of <math>M1</math>, and <math>b\_2\_c</math>, which is an ''internal'' event of <math>M2</math>. Thus, according to the definition given above, <math>b\_2\_c</math> is an ''external'' event for <math>M1</math>. In the same manner, <math>a\_2\_b</math> is an ''external'' event for <math>M2</math>.
 +
 +
''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, <font id="ancre_3">''The B-book: assigning programs to meanings''</font>, Cambridge University Press, 1996 (ISBN 0-521-49619-5).
 +
* J.R. Abrial, Mathematical Models for Refinement and Decomposition, in ''The Event-B Book'', to be published in 2009 ([http://www.event-b.org/abook.html lien externe]).
 +
* J.R. Abrial, <font id="ancre_1">''Event Model Decomposition''</font>, Version 1.3, April 2009.
 +
* M. Butler, <font id="ancre_2">Decomposition Structures for Event-B</font>, in ''Integrated Formal Methods iFM2009'', Springer, LNCS 5423, 2009 ([http://eprints.ecs.soton.ac.uk/16965/1/butler.pdf lien externe]).
 +
 +
[[Category:Design]]
 
[[Category:Work in progress]]
 
[[Category:Work in progress]]

Revision as of 16:28, 6 July 2009

Introduction

One of the most important feature of the Event-B approach is the possibility 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 the Event Model Decomposition article: 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.

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.

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

Models.png

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.

The hierarchy of machines (see the REFINES clauses) shall be first flatten (virtually or not), as illustrated below. The resulting machine is considered as being the non-decomposed machine from which the sub-machines shall be built.
Note that it may be necessary to rename some variables or invariants.

Flattening machines.png

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 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. The static checker shall have a way to determine if a given variable is shared or not.

Partitioning the variables in the sub-machines of the decomposition

The first question raised by the partition of the variables is whether it shall be the first stage of the decomposition, or not. Let's first suppose that the answer is "yes". The case where e is an event that accesses a variable v1 associated to a sub-machine M1 and a variable v2 associated to a sub-machine M2 cannot be successfully handled: should e be associated to M1 or to M2? Moreover, contrary to the events, the variables are not essentially bearers of meanings, and they cannot by themselves guide the decomposition.

As a consequence, it is pertinent to assume that the events have been first partitioned. The following cases have then 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. 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. It shall be tagged as such and 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
 ...
 >

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

The construction of an external event highly relies on some rewriting / simplification rules. It is recommended to peruse them before reading further.

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
We first focus on the generic construction of an external event from an event of a sub-machine M whose action is expressed as follows:

 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')
  1. The first step of the construction consists in replacing the private variables by parameters. Note that this step is purely fictive, because assigning an event parameter is not allowed!
  2. e ANY x_1,...,x_n~ WHERE G(x_1,...,x_n,s_1,...,s_m)~ THEN x_1,...,x_n,s_1,...,s_m \bcmsuch P(x1,...,x_n,s_1,...,s_m, x_1',...,x_n',s_1',...,s_m')
  3. The second step consists in 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.
  4. The third and last step of the construction consists in introducing an existential quantifier to resolve the invalid assignment. external\_e is the newly built external event.
  5. 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 \qdot P(x1,...,x_n,s_1,...,s_m, y_1,...,y_n,s_1',...,s_m')

Derived constructions
Then, it is possible to derivate the construction for other actions:

  1. Rewriting rules 1 to 5 shall be first applied as many times as possible, from left to right, to get the action into the generic form introduced before.
  2. Then, the steps detailed for the generic construction shall be followed.
  3. Then, the simplification rules 6 to 8 shall be enforced.
  4. Finally, the rewriting rules 1 to 4 shall be applied, from right to left.

Thus, 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).
The proof obligations generated for deterministic actions are indeed more suitable than those generated for non-deterministic actions.

In the same manner, 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 \qdot x \in S (FIS 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).

Example

 e
 WHERE 
   G(v_1,...,v_n,s_1,...,s_m)~      
 THEN                  
   \begin{array}{ll}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') \end{array}
 external_e
 ANY x_1,...,x_n~
 WHERE 
   G(x_1,...,x_n,s_1,...,s_m)~      
 THEN                  
   \begin{array}{ll}s_1\!\!\! &\bcmsuch P_{n+1}(x_1,...,x_n,s_1,...,s_m,s_1')\\
    ...\\
    s_m\!\!\! &\bcmsuch P_{n+m}(x_1,...,x_n,s_1,...s_m,s_m') \end{array}

In this example, the rules 4, 7 and 8 shall be applied.

Partitioning the events in the sub-machines of the decomposition

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 REFINES clauses shall be empty. Moreover, note that it may be necessary to rename some events when performing the partition.
  • 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 extended 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. The static checker shall have a way to determine if a given event is external or not.

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    
 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   
 THEN                  
   x_1,...,x_n \bcmsuch \exists z_1,...,z_m \qdot 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 of a given sub-machine, then it shall be copied in this sub-machine.
  • Case 2: If i is an invariant involving private variables of distinct sub-machines, then it shall not be copied.
  • Case 3: If i is an invariant only involving shared variables, then it shall only be copied in the sub-machines containing all these variables.
  • Case 4: If i is an invariant involving private variables and shared variables, then it shall only be copied in the sub-machines containing all these variables.

These different cases are illustrated in the figure below, where P1, P2, P3 and P4 are predicates. A is an abstract machine, C is a concrete machine extending A, M is the flattened machine for C and A (see how flattening a hierarchy of machines), and M1, M2, and M3 are the sub-machines resulting from the decomposition of M. v1 is a private variable of M1, v2 is a variable shared between M1 and M2, v3 is a variable shared between M2 and M3>, and v4 is a private variable of M3.

Invariants.png

To summarize, an invariant based on a P(v_m,...,v_n)~ predicate is copied in a sub-machine M_x if and only if M_x contains the \{v_m,...,v_n\}~ variables.

If an invariant is used for typing but it has not been copied, a theorem shall be added in the sub-machines for each variable for which typing is required (otherwise a problem will be detected by the static checker). Note that there is no contradiction with the requirements on proof obligations; no proof obligation (PO) is indeed generated for predicates v \in T, where v is a variable and T is a type.

Beyond that, a workaround exists if an invariant inv, based on a P(v_m,...,v_n)~ predicate, seems useful (for example an invariant between a concrete variable and some abstract variable) but it has disappeared in a sub-machine M_x containing variables \{v_p,...,v_q\}~ (eg. inv2 and inv3 have both been excluded from M3 machine by application of the stated rules). It is indeed possible to add in the non-decomposed machine a theorem based on P~, but where the variables \{v_m,...,v_n\} \setminus \{v_p,...,v_q\} become bound, and then to perform again the decomposition. It will lead to a new proof obligation in the non-decomposed machine, which does not pose any difficulty.
For example, if a theorem inv5: P5(v4)~, with P5 \defi \exists v1 \qdot P2(v1,v4), is added to the C concrete machine, then it will be copied in the sub-machine M3 during the decomposition (see case 1). In order to prove the P5~ statement, the bound variable v1 shall obviously be instantiated with v1.

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 (see the EXTENDS clauses) 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, by respecting the following sequence: the constants shall be first included, then the carrier sets shall be added, and finally the axioms shall be considered.
This context 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 constants

A constant of a non-decomposed context shall be copied in a sub-context if and only if it appears in a predicate (invariant or guard) or an assignment (action) of the associated sub-machine.

About the carrier sets

A carrier set shall be visible from any sub-machine that references it, explicitly or implicitly, through a predicate or an assignment. 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, or types a constant previously copied to this sub-context.

About the axioms

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

As for the invariants, an axiom is copied in a sub-machine M_x if and only if M_x contains the referenced constants and sets. If an axiom is used for typing but it has not been copied, a theorem shall be added in the sub-contexts for each constant for which typing is required (otherwise a problem will be detected by the static checker).

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?

The entry point for the decomposition is a machine M1, its visible contexts, and its whole parent hierarchy of machines.

Machine.png

The machine M1 to be taken as input for the decomposition shall be pointed by the end-user. The EXTENDS clauses of contexts and the SEES clauses of machines are used to build the associated hierarchy of contexts. In the same manner, the REFINES clauses allow to build the associated hierarchy of machines.

Configuration of the decomposition

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

  • identify the machine to be taken as input for the decomposition.
  • 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

A Decompose action shall be added. It shall be enabled if and only if a machine is selected. It shall be available from the Project menu, from the toolbar, and in the contextual menu displayed when right-clicking on the selected project.

Action.png

A new Event-B project shall be created for each sub-machine built during the configuration. The decomposition of the sub-machine shall first be completed, and then the non-decomposed context shall be partitioned, as specified before.

As far as possible, the developments shall not be performed in the Event-B core; the dedicated extension points shall be used instead (eg. those provided for the static checker. See the plugin.xml file of the org.eventb.core package).

Generation of the proof obligations

A model to be decomposed is assumed to be proved, i.e. the proof obligations (PO) have all been handled successfully. The following conditions on PO shall be fulfilled during the decomposition:

  • The decomposition shall not generate any new proof obligation.
  • The proof obligations related to the non-decomposed model shall not be "propagated" to the decomposed models to be proved again. As a consequence, the Proof Obligation Generator (POG) shall be temporary disconnected until the decomposition is performed.

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 variable v, (partition;access^{-1})[\{v\}]~ is then the set of the sub-machines accessing v, and v is a private variable of a sub-machine m if and only if this set contains a single component (i.e. card((partition;access^{-1})[\{v\}]) = 1~); otherwise, and if and only if this set is not empty, v is shared.
In parallel, for a given sub-machine m, (access;partition^{-1})[\{m\}]~ is 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 above, 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, The B-book: assigning programs to meanings, Cambridge University Press, 1996 (ISBN 0-521-49619-5).
  • 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).