Difference between revisions of "ADVANCE D3.2 Model Composition and Decomposition"

From Event-B
Jump to navigationJump to search
imported>Renato
imported>Renato
Line 8: Line 8:
  
 
== Motivations / Decisions ==
 
== Motivations / Decisions ==
−
{{TODO|Fill this paragraph.}}
+
 
 +
===Composition===
  
 
While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the final result to be considered valid. Since the composition maintains the monotonicity property of the systems, the sub-systems can be refined independently on a further stage, preserving composition properties. In the latest version released (v1.5), several features were added to the shared event composition tool:
 
While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the final result to be considered valid. Since the composition maintains the monotonicity property of the systems, the sub-systems can be refined independently on a further stage, preserving composition properties. In the latest version released (v1.5), several features were added to the shared event composition tool:
Line 15: Line 16:
 
**Added stronger static checks: no shared variable is allowed; all abstract events must be refined; common parameters must have the same type; check that a composed event must have at least one combined event;  
 
**Added stronger static checks: no shared variable is allowed; all abstract events must be refined; common parameters must have the same type; check that a composed event must have at least one combined event;  
 
**Improved UI interface: using the form-based editor, if the symbol corresponding to a composed event is hovered, a preview of the composed event is displayed
 
**Improved UI interface: using the form-based editor, if the symbol corresponding to a composed event is hovered, a preview of the composed event is displayed
 +
 +
===Decomposition===
  
 
The main goal of Decomposition is to cut a model <math>M</math> into sub-models <math>M_1, ..., M_n</math>, 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 be recomposed into a whole model <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>. Note that this recomposition will never be performed in practice.  
 
The main goal of Decomposition is to cut a model <math>M</math> into sub-models <math>M_1, ..., M_n</math>, 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 be recomposed into a whole model <math>MR</math> in a way that guarantees that <math>MR</math> refines <math>M</math>. Note that this recomposition will never be performed in practice.  
Line 20: Line 23:
 
* In an shared variable 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.  
 
* In an shared variable 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.  
 
* In an shared event decomposition, the variables of a model are partitioned among the sub-models. Consequently, the events are partitioned accordingly to each sub-model.
 
* In an shared event decomposition, the variables of a model are partitioned among the sub-models. Consequently, the events are partitioned accordingly to each sub-model.
 +
 +
In the latest version released (v1.5), the user's inputs and request were taken into account. In particular in terms of better usability of the tool. We addressed this topic by:
 +
 +
* Typing guards (automatically generated) are marked as theorems
 +
* Static checks were added to the decomposition file according to the decomposition style chosen.
 +
* Improved UI interface: removed dialog requesting confirmation to delete possible existing sub-components (generated sub-components are marked as read-only)
 +
* Changed suffix of decomposition file to "_DCMP"
 +
* Fixed small bugs
  
 
== Available Documentation ==
 
== Available Documentation ==

Revision as of 14:39, 21 June 2012

Overview

Composition is the process by which it is possible to combine different sub-systems into a larger system. Known and studied in several areas, this has the advantage of reusability and combination of systems especially when it comes to distributed systems.

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. Model decomposition is a powerful technique to scale the design of large and complex systems. It enables developers to separate components development from the concerns of their integration and orchestration. And it tackles the complexity problem mentioned above, since decomposition allows the partitioning of a model into separated components, spreading the complexity of the original model. This allows a decomposed part of the model to be treated as an independent artefact so that the modeller can concentrate on this part and does not have to worry about the other parts.

Composition and decomposition can be seen as inverse operations: while composition starts with different components that can be assembled together, decomposition starts with a single components that can be partitioned into different components.

Motivations / Decisions

Composition

While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the final result to be considered valid. Since the composition maintains the monotonicity property of the systems, the sub-systems can be refined independently on a further stage, preserving composition properties. In the latest version released (v1.5), several features were added to the shared event composition tool:

    • Added proof obligations: Well-Definedness (WD) and Invariant preservation (INV) for (composition) invariants and applicable to all composed machines; Gluing Invariant Preservation (INV), Simulation (SIM) and Guard Strengthening (GRD) for refinement; other POs are expected to be proved in directly in the included machines.
    • Added stronger static checks: no shared variable is allowed; all abstract events must be refined; common parameters must have the same type; check that a composed event must have at least one combined event;
    • Improved UI interface: using the form-based editor, if the symbol corresponding to a composed event is hovered, a preview of the composed event is displayed

Decomposition

The main goal of Decomposition is to cut a model M into sub-models M_1, ..., M_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 be recomposed into a whole model MR in a way that guarantees that MR refines M. Note that this recomposition will never be performed in practice.

  • In an shared variable 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.
  • In an shared event decomposition, the variables of a model are partitioned among the sub-models. Consequently, the events are partitioned accordingly to each sub-model.

In the latest version released (v1.5), the user's inputs and request were taken into account. In particular in terms of better usability of the tool. We addressed this topic by:

  • Typing guards (automatically generated) are marked as theorems
  • Static checks were added to the decomposition file according to the decomposition style chosen.
  • Improved UI interface: removed dialog requesting confirmation to delete possible existing sub-components (generated sub-components are marked as read-only)
  • Changed suffix of decomposition file to "_DCMP"
  • Fixed small bugs

Available Documentation

Documentation for composition is available in:

Documentation for decomposition is available in:

Planning

TODO: Fill this paragraph.

References

Retrieved from ‘https://wiki.event-b.org/index.php?title=ADVANCE_D3.2_Model_Composition_and_Decomposition&oldid=319’