Difference between pages "Rodin Workshop 2010" and "User:Nicolas/Collections/ADVANCE D3.4 Model Composition and Decomposition"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>WikiSysop
 
imported>Andy
 
Line 1: Line 1:
= Rodin User and Developer Workshop, University of Duesseldorf, 20-22 September 2010 =
+
== 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 re-usability 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 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 ==
 +
{{TODO}}
  
 +
== Available Documentation ==
 +
{{TODO}}
  
==Monday 20th September==
+
== Conclusion ==
09h00 - 16h00 Rodin tutorial (by Systerel)
+
Composition/decomposition have been applied in the interlocking case study of WP1 and the smart grid case study of WP2.
  
==Tuesday 21st September (Workshop Day 1)==
+
== References ==
* 09h00 - 10h30 ''Atomicity Decomposition a Technique for Structuring Refinement in Event-B'', Asieh Salehi Fathabadi, Michael Butler
+
<references/>
* 09h30 - 10h00 ''Integrating astd in the Rodin platform'', Paul Amar, Marc Frappier, Cecile Lartaud, and Jeremy Milhau
 
* 10h00 - 10h30 P''otpourri of what? One year in a DA's life'', Aryldo G. Russo Jr., Thiago C. de Sousa, Haniel Barbosa, Paulo Muniz, and David Deharbe
 
* 10h30 - 11h00 Coffee break
 
* 11h00 - 11h30 ''The ProR Requirements Engineering Platform'', Michael Jastram
 
* 11h30 - 12h00 ''A Refinement Planning Sheet'', Shin Nakajima
 
* 12h00 - 12h30 ''Refinement Plans for Reasoned Modelling'', Maria Teresa Llano, Andrew Ireland, and Gudmund Grov
 
* 12h30 - 14h00 Lunch break and tool demos
 
* 14h00 - 15h00 ''Invited Talk'', Jean-Raymond Abrial
 
* 15h00 - 15h30 ''Reflections on the teaching of System Modelling and Design'', Ken Robinson
 
* 15h30 - 16h00 Coffee break
 
* 16h00 - 16h30 ''Verification of a Byzantine Agreement Protocol using Event-B'', Roman Krenicky and Mattias Ulbrich
 
* 16h30 - 17h00 ''Code Generation with the Event-B Tasking Extension (Tool Development)'', Andy Edmunds
 
* 17h00 - 17h30 ''Modelling Recursion in Event-B'', Stefan Hallerstede
 
 
 
==Wednesday 22nd September (Workshop Day 2)==
 
* 09h00 - 09h30 Using automated theory formation to discover invariants of Event-B models, Maria Teresa Llano, Andrew Ireland, Alison Pease, Simon Colton, John Charnley
 
* 09h30 - 10h00 ''Specifying and Solving Constraint Satisfaction Problems in B'', Michael Leuschel and Daniel Plagge
 
* 10h00 - 10h30 F''ault Tolerance View in Event-B Development'', Ilya Lopatkin, Alexei Iliasov, Alexander Romanovsky
 
* 10h30 - 11h00 Coffee break
 
* 11h00 - 11h30 ''Event-B models of P systems'', Florentin Ipate, Turcanu Adrian
 
* 11h30 - 11h45 ''Records'', Vitaly Savicks, Colin Snook, Michael Butler
 
* 11h45 - 12h00 ''Decomposition Tool: Development and Usage'', Renato Silva, Carine Pascal, T.S. Hoang, and Michael Butler
 
* 12h00 - 12h15 ''Sequence Refinement'', ''Modularisation Plugin'', Alexei Iliasov
 
* 12h15 - 12h30 ''Modelling Views Paradigm Support for Rodin'', Alexei Iliasov
 
* 12h30 - 14h00 Lunch break and tool demos
 
* 14h00 - 15h00 ''Invited Talk'', Joe Kiniry
 
* 15h00 - 15h30 ''A small experiment in Event-B rippling'', Gudmund Grov, Alan Bundy & Lucas Dixon
 
* 15h30 - 16h00 Coffee break
 
* 16h00 - 16h30 ''Animation of UML-B State-machines'', Vitaly Savicks, Colin Snook, Michael Butler
 
* 16h30 - 17h00 ''Addressing Extensibility Issues in Rodin and Event-B'', Issam Maamria and Michael Butler
 
 
 
=Registration=
 
[http://www.formal-methods.de/avocs10/registration.html Registration page]
 

Revision as of 12:26, 7 November 2014

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 re-usability 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 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

TODO

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