Difference between pages "User:Nicolas/Collections/ADVANCE D3.4 Model Composition and Decomposition" and "User:Pascal/Collections/Deploy Deliverable D23"

From Event-B
< User:Nicolas(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Pascal
 
Line 1: Line 1:
== Overview ==
+
== Introduction ==
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 re-usability and combination of systems especially when it comes to distributed systems.
+
The purpose of this page is to provide a template to define the common content for all sections of the DEPLOY Deliverable D23 (Model Construction and Analysis Tool II), as mentioned in the [http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d103646/D23_Writing_Plan.pdf writing plan] for this document.
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 first developers to separate components development from the concerns of their
 
integration and orchestration. Moreover, it tackles the complexity problem mentioned above,
 
since decomposition allows the partitioning the complexity of the original model into separated components. This allows a decomposed part of the model to be treated as an independent artifact 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 ==
+
== Template ==
Recent updates to the composition and decomposition features are:
+
For each item covered in this document (see the writing plan), a section shall be created to provide a description of work and describe the role of partners during the passed year.
  
1) Support for flattening: this is needed in order to compose refinement chains rather than just machines at a single abstraction level.  It was requested by Critical in order to apply composition to the smar grid case study.
+
More precisely, each section shall give an overview of the contribution, some pointers to Event-B wiki pages where to find technical details, and some justifications for the decisions.
  
2) Porting to Rodin 3
+
== Example ==
 
 
== Available Documentation ==
 
{{TODO}}
 
 
 
== Conclusion ==
 
Composition/decomposition have been applied in the interlocking case study of WP1 and the smart grid case study of WP2.
 
 
 
== References ==
 
<references/>
 

Revision as of 09:07, 2 November 2009

Introduction

The purpose of this page is to provide a template to define the common content for all sections of the DEPLOY Deliverable D23 (Model Construction and Analysis Tool II), as mentioned in the writing plan for this document.

Template

For each item covered in this document (see the writing plan), a section shall be created to provide a description of work and describe the role of partners during the passed year.

More precisely, each section shall give an overview of the contribution, some pointers to Event-B wiki pages where to find technical details, and some justifications for the decisions.

Example