Difference between pages "D45 Scalability" and "Parallel Composition using Event-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Mathieu
 
Line 1: Line 1:
−
= Overview =
+
[[User:Renato]] at [[Southampton]] is in charge of the [[Parallel Composition using Event-B]].
−
* '''Improved Performance''' According to the refocus mentioned in the [[D45_General_Platform_Maintenance#Motivations| General Platform Maintenance]] chapter, much of the reworking efforts performed on the core platform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.
 
−
* '''Design pattern management / Generic Instantiation''' {{TODO}} An overview of the contribution about the design pattern management / Generic Instantiation (Thai Son Hoang)
 
−
* '''Edition''' It appears along DEPLOY - the models defined by pilots becoming industrial sized due to the level of complexity reached - that the edition became a central concern.
 
−
:*The legacy structured editor based on a form edition specific architecture reached its limits in editing such complex models. Industrial partners found this issue significant regarding the adoption of the Rodin platform in industry and providing a new structured editor correcting this issue became a important task during this last year of the DEPLOY project.
 
−
:*Camille textual editor had to tackle challenges related to resources mapping and management for projects of industrial size mentioned above or even the design of extension capabilities, that became a major concern since the grammar could be extended with theories.
 
  
−
= Motivations =
+
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. While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the final result to be considered valid. Our goal is to add this feature to the Rodin Platform (using Event-B notation) and study the concerns, properties, conditions, proof obligations, advantages and disadvantages when create/analysing system specifications. Since the composition maintains the monotonicity property of the systems, the sub-systems can be refined independently on a further stage, preserving composition properties.
  
−
== Improved Performance ==
+
[[Image:share_event_machine.jpeg]]
−
Some of the several major performance issues faced were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Some other were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. It was necessary to solve such issues before the end of DEPLOY.
 
  
−
== Design Pattern Management / Generic Instantiation  ==
+
[[Image:share_event_mach_comp1.jpeg]]
−
{{TODO}} ''To be completed by Thai Son Hoang''
+
[[Image:share_event_machine_comp2.jpg]]
−
== Edition ==
 
−
Two major kinds of failures were faced when developing industrial sized models:
 
−
:* Failures occurring on windows platforms, the mostly used system, when reaching the operating system limit number of graphical elements in memory allowed to be displayed at once. This bug used to crash the Rodin platform, and it appeared necessary to control the number of graphical elements needed to display the model elements. Architectures sparing these graphical elements should be thus favoured.
 
−
:* Failures due to the high consumption of memory by the heavy graphical elements used by the forms of legacy editor.
 
−
:Moreover, it appeared important to visualize some elements that are not part of the current level of modelling, but are linked to it, for example, the actions in an abstract event, or its guards. Such elements are called the "inherited" elements, or "implicit children". The legacy structured editor being directly interfaced with the underlying Event-B models in database, it was difficult and tricky to modify it in order to display inherited elements. This was one more argument to go for a new editor based on a intermediary representation of the models.
 
−
:Another motivation to go for another editor was to get a more modest and ergonomic way to visualize and edit the models. The models being presented through styled text pretty printing and the edition tightly derived from a textual edition.
 
  
−
* The motivations about Camille evolution {{TODO}} Ingo Weigelt.
+
A machine '''''S''''' with events '''''e1, e2, e3''''' and '''''e4''''' and variables '''''v1, v2''''' and '''''v3''''' can be decomposed using event (de)-composition of event ''e2'' (as can be seen above). This would result in the machine '''''S1''''' and '''''S2''''' that have a partial part of the event ''e2'': machine ''S1'' has the part related to the variable ''v1'' (''e2''') and machine ''S2'' has the part related to the machine ''v2'' (''e2''<nowiki>''</nowiki>). Also some other events are separated (''e1'' and ''v1'' only exist on machine ''S1'' and events ''e3'' and ''e4'' with variable ''v3'' only exist on the machine ''S2'') as can be seen above.
  
−
= Choices / Decisions =
+
The composition is based on proposals for parallel composition in Event-B in the following paper: [http://deploy-eprints.ecs.soton.ac.uk/51/].
−
== Improved Performance ==
 
−
SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between performance loss and the various reported bugs, such as "platform hanging" bugs. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well which made the scalability improvement tasks encompass the maintenance goals.<br>
 
−
Later, a deeper investigation was performed, to identify and tackle the remaining performance issues. Profiling and code review were the two techniques used. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures.
 
−
A good example, was the Event-B built-in editor based on form editors with a high use of greedy graphical components. Such architecture appears to be weak when it was needed to display industrial size models. This affected the modelling experience with some long, and really annoying to the user, reaction lags. To solve such issue, it has been chosen to refactor the editors using a representation which was a light-weight graphical alternative to lower the number of needed components.
 
  
−
== Design Pattern Management / Generic Instantiation  ==
+
A release of the composition plugin for Rodin 0.8.2 is available (email me:ras07r@ecs.soton.ac.uk).  
−
{{TODO}} ''To be completed by Thai Son Hoang''
 
−
== Edition ==
 
−
* Rodin Editor
 
−
The legacy editor drawbacks mainly come from its greedy components and structure but a structured way to edit the models (based on a database storage) still seems particularly appropriate. This mainly explains why a new structured editor, the Rodin Editor, has been built on the basis of the improvements made to the Proving UI. In fact, the textual component used, the SWT StyledText, allowed to describe every model element as text, as would a pretty print do. The edition is made possible through the use of a unique additional graphical component that overlays the presentation of the element to edit. It lightened the presentation, but also side stepped the use of a significant amount of greedy graphical because at most two of them are needed: the model viewer and its overlay editor!<br>
 
−
The first public version (0.5.0) of the Rodin Editor as been released on the 13/07/2011 as a plug-in of the Rodin platform. This decision has been made in order to let the plug-in incubation for the time it is being tested and stated that no regression is introduced. The Rodin Editor since its version xx is part of the Rodin Core Platform.
 
−
* Camille
 
−
{{TODO}} Ingo Weigelt
 
  
−
= Available Documentation =
+
A release for Rodin 0.9.2.1 is now available from the Rodin Main Update Site.
−
* {{TODO}} Links for Improved Performance
 
−
* {{TODO}} Links for Design Pattern Management / Generic Instantiation
 
−
* Links for Edition
 
−
:Two documentation pages have been created for the Rodin Editor:
 
−
:* A general page describing the editor and how it works <ref name="RodinEditorPage">http://wiki.event-b.org/index.php/Rodin_Editor</ref>,
 
−
:* A user guide page <ref name="RodinEditorUserManual">http://wiki.event-b.org/index.php/Rodin_Editor_User_Guide</ref>,
 
−
: Moreover, a special category has been created on both SourceForge feature request<ref name="featTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651672</ref> and bug<ref name="bugTracker">https://sourceforge.net/tracker/?group_id=108850&atid=651669</ref> trackers.
 
  
−
:{{TODO}} '''Ingo''' Camille
+
1. To create a new composition file (bcp file), go to Toolbar (on top), New>>Other... Event-B>>Composition Machine. Then select the project (if not selected already) and filename (by default is cm.bcp).
  
−
= Status =
+
2. Bcp files are visible on Event-B perspective(from Rodin 0.9). For Rodin 0.8.2, go to Resource or Java perspective to edit the file.
−
== Improved Performance ==
 
−
The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI, and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.<br>
 
  
−
== Design Pattern Management / Generic Instantiation  ==
+
3. After editing the properties of the bcp file, you can generate a new bum file (machine), by using the green button on the toolbar (CM - symbol of machine) or by right clicling on the bcp file and choose the option :'Create Composed Machine'. You will have to introduce a name for the new machine and after that is just press 'OK'.
−
{{TODO}} ''To be completed by Thai Son Hoang''
 
−
== Edition ==
 
−
The Rodin Editor is part of the Rodin plateform since. As the time of writing this document, the current version is xx.
 
  
−
= References =
 
−
<references/>
 
  
−
[[Category:D45 Deliverable]]
+
'''
 +
==User Manual==
 +
'''
 +
 
 +
The Shared Event Composition Plugin is divided in 6 sections:
 +
 
 +
* '''Refines''' : allows to define an abstract machine of this composed machine. It is a valid machine that exists on the project.
 +
* '''Includes''': to compose a model, it is necessary to define which sub-systems(machines) interact. The machines must be abstract (not refinements of other machines) and have to be valid. It is also possible to choose if the included machine invariant should be visible to the composed machine or not (for proof optimization).
 +
* '''Sees''': allows to add contexts to the composed machine. The contexts seen by the ''included machines'' are visible to the composed machine. So it is only allowed to see contexts that are not already seen by the composed machine.
 +
* '''Invariants''': allows the inclusion of invariant clauses to the composed file. The inclusion of more invariants (from the included machines) depends on the user’s choice on ''Includes''. The defined invariants on the composed machine are “joint” properties between the included machines (gluing invariants), so variables and contexts from all the included machines become part of the composed machine scope.
 +
*'''Variant''': since the composed machine can be a refinement of an abstract model, there is the possibility of introducing new events. In order to avoid divergence, variants are necessary for the new events.
 +
*'''Composes Events''': the interaction between systems only happens when the composed events are synchronised and ready to be executed. The systems can interact through shared parameters. It is possible to define the following properties for composes events:
 +
** Name: name of the composes event
 +
** Extended/Not Extended: in the composes machine refines an abstract machine and if there are events with the same name, the concrete event can extend the abstract one (from Rodin 0.9).
 +
** Convergence: event can be chosen from ''Ordinary'', ''Convergence'' or ''Anticipated''.
 +
 
 +
 
 +
Still under '''Composes Events''', there are more properties that characterise a composed event:
 +
* '''Refines''' : possibility to choose if the composes event it is a refinement of an abstract event
 +
* '''Combines Event''': selection of the events that shall be composed. First the machine (out from the included machine list) is chosen and after, which event is supposed to be combined. It is possible to have only one combined event.
 +
 
 +
 
 +
The '''Combination of Events''' can be expressed as:
 +
* The parameters are listed in one single (composed) event. Parameters (from different events) with the same name will be merged (becoming only one parameter). This correspond to the shared event composition with message passing, where a parameter is passed from one event to other.
 +
* The guards from the different combined events are merged using conjuction. So this composed event will be available if all the guards are true.
 +
* the actions are also merged and executed in parallel.
 +
 
 +
Like mention above,a machine can be generated containing all the properties defined on the composed machine file. The generation of the new machine can be executed by using the green button on the toolbar (CM - symbol of machine) or by right clicling on the bcp file and choosing the option :''Create Composed Machine''. A name for the new machine have to be introduced (a name is suggested by default ) and by clicking 'OK' or 'Override', a new machine file is generated.
 +
 
 +
 
 +
 
 +
 
 +
[[Category:Parallel composition plugin]]
 +
[[Category:User documentation]]

Revision as of 08:59, 4 March 2009

User:Renato at Southampton is in charge of the Parallel Composition using Event-B.

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. While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the final result to be considered valid. Our goal is to add this feature to the Rodin Platform (using Event-B notation) and study the concerns, properties, conditions, proof obligations, advantages and disadvantages when create/analysing system specifications. Since the composition maintains the monotonicity property of the systems, the sub-systems can be refined independently on a further stage, preserving composition properties.

Share event machine.jpeg

Share event mach comp1.jpeg Share event machine comp2.jpg

A machine S with events e1, e2, e3 and e4 and variables v1, v2 and v3 can be decomposed using event (de)-composition of event e2 (as can be seen above). This would result in the machine S1 and S2 that have a partial part of the event e2: machine S1 has the part related to the variable v1 (e2') and machine S2 has the part related to the machine v2 (e2''). Also some other events are separated (e1 and v1 only exist on machine S1 and events e3 and e4 with variable v3 only exist on the machine S2) as can be seen above.

The composition is based on proposals for parallel composition in Event-B in the following paper: [1].

A release of the composition plugin for Rodin 0.8.2 is available (email me:ras07r@ecs.soton.ac.uk).

A release for Rodin 0.9.2.1 is now available from the Rodin Main Update Site.

1. To create a new composition file (bcp file), go to Toolbar (on top), New>>Other... Event-B>>Composition Machine. Then select the project (if not selected already) and filename (by default is cm.bcp).

2. Bcp files are visible on Event-B perspective(from Rodin 0.9). For Rodin 0.8.2, go to Resource or Java perspective to edit the file.

3. After editing the properties of the bcp file, you can generate a new bum file (machine), by using the green button on the toolbar (CM - symbol of machine) or by right clicling on the bcp file and choose the option :'Create Composed Machine'. You will have to introduce a name for the new machine and after that is just press 'OK'.


User Manual

The Shared Event Composition Plugin is divided in 6 sections:

  • Refines : allows to define an abstract machine of this composed machine. It is a valid machine that exists on the project.
  • Includes: to compose a model, it is necessary to define which sub-systems(machines) interact. The machines must be abstract (not refinements of other machines) and have to be valid. It is also possible to choose if the included machine invariant should be visible to the composed machine or not (for proof optimization).
  • Sees: allows to add contexts to the composed machine. The contexts seen by the included machines are visible to the composed machine. So it is only allowed to see contexts that are not already seen by the composed machine.
  • Invariants: allows the inclusion of invariant clauses to the composed file. The inclusion of more invariants (from the included machines) depends on the user’s choice on Includes. The defined invariants on the composed machine are “joint” properties between the included machines (gluing invariants), so variables and contexts from all the included machines become part of the composed machine scope.
  • Variant: since the composed machine can be a refinement of an abstract model, there is the possibility of introducing new events. In order to avoid divergence, variants are necessary for the new events.
  • Composes Events: the interaction between systems only happens when the composed events are synchronised and ready to be executed. The systems can interact through shared parameters. It is possible to define the following properties for composes events:
    • Name: name of the composes event
    • Extended/Not Extended: in the composes machine refines an abstract machine and if there are events with the same name, the concrete event can extend the abstract one (from Rodin 0.9).
    • Convergence: event can be chosen from Ordinary, Convergence or Anticipated.


Still under Composes Events, there are more properties that characterise a composed event:

  • Refines : possibility to choose if the composes event it is a refinement of an abstract event
  • Combines Event: selection of the events that shall be composed. First the machine (out from the included machine list) is chosen and after, which event is supposed to be combined. It is possible to have only one combined event.


The Combination of Events can be expressed as:

  • The parameters are listed in one single (composed) event. Parameters (from different events) with the same name will be merged (becoming only one parameter). This correspond to the shared event composition with message passing, where a parameter is passed from one event to other.
  • The guards from the different combined events are merged using conjuction. So this composed event will be available if all the guards are true.
  • the actions are also merged and executed in parallel.

Like mention above,a machine can be generated containing all the properties defined on the composed machine file. The generation of the new machine can be executed by using the green button on the toolbar (CM - symbol of machine) or by right clicling on the bcp file and choosing the option :Create Composed Machine. A name for the new machine have to be introduced (a name is suggested by default ) and by clicking 'OK' or 'Override', a new machine file is generated.

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