Difference between pages "D23 Modularisation Plug-in" and "D23 UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Alexili
 
imported>Pascal
 
Line 1: Line 1:
= Overview =
+
=== Overview ===
Modularisation Plugin realises a support for structuring Event-B developments into modules. The objective is to achieve better structuring of models and proofs while also providing a facility for model reuse. It is expected that the structuring approach realised in the plugin would complement the functionality A/B-style decomposition plugin.
+
This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton.
  
The module concept is very close to the notion Event-B development (a refinement tree of Event-B machines). However, unlike a conventional development, a module is equipped with an interface. An interface defines the conditions on the way a module may be incorporated into another development (that is, another module). The plugin follows an approach where an interface is characterised by a list of operations specifying the services provided by the module. An integration of a module into a main development is accomplished by referring operations from Event-B machine actions using an intuitive procedure call notation.
+
A new plug-in feature has been developed to provide animation of UML-B state-machine diagrams. This feature was developed by University of Southampton.
  
The plugin was developed in Newcastle University in cooperation with Abo Academy and Space Systems Finland.  
+
The longer term development of UML-B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initially developed by University of Southampton, Heinrich-Heine University, Duesseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.
  
= Motivations =
+
=== Motivations ===
  
There are several conceptual approaches to decomposition. To contrast our proposal, let us consider some of them.
+
====UML-B improvements====
 +
The current version of the UML-B tool has been improved to support the refinement of  state-machines. At the last deliverable, refinement of classes was supported and state-machine refinement was beginning to be investigated. The investigation has experimented several notation and methodological alternatives. The design has now been finalised and an implementation has been achieved. State-machines can be refined by adding nested state-machines inside states. Some of the transitions in the nested state-machine do not represent new events but contribute to the refinements of existing transitions in the parent state-machine. A concept of ''transition elaboration'' has been invented to represent this relationship.
  
One approach to decomposition is to identify a general theory that, once formally formulated, would contribute to the main development. For instance, a model realising a stack-based interpreter could be simplified by considering the stack concept in isolation, constructing a general theory of stacks and then reusing the results in the main development. Thus, an imported theory of stack contributes axioms and theorems assisting in reasoning about stacks.  
+
Many other minor improvements have been made to the UML-B tool including:
 +
collapsing empty compartments on diagrams,
 +
improved navigation between diagrams,
 +
improved properties views,
 +
ability to order classes and class-types in the translation,
 +
support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems).
  
Decomposition may also be achieved by splitting a system into a number of parts and then proceeding with independent development of each part. At some point, the model parts are recomposed to construct an overall final model. This decomposition style relies on the monotonicity  of refinement in Event-B although some further constraints must be satisfied to ensure the validity of a recomposed model. A-style and B-style decompositions fit into this class.
+
====UML-B State-machine Animation====
 +
This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.
  
Finally, decomposition may be realised by hierarchical structuring where some part of an overall system functionality is encapsulated in a self-conatined modelling unit embedded into another unit. The distinctive characteristic of this style is that recomposition of model parts happens at the same point where model is decomposed.
+
====EMF Framework for Event-B====
  
Modularisation plugin realises the latter approach. The procedure call concept is used to accomplish single point composition/decomposition. There are a number of reasons to try to split a development into modules. Some of them are:
+
An EMF (Eclipse Modelling Framework) based representation of Event-B was developed and made available as a plug-in feature for Rodin. This enables Event-B machines and contexts to be loaded into EMF based tools. Serialisation (i.e. loading and saving) is performed via the Rodin API. This feature can be viewed as an ''enabling technology''. Hence motivation derives from several sources including:
 +
* A Text editor was requested by several industrial and academic partners - A fully-featured EMF based text editor ('''Camille''') has been developed by Duesseldorf and is now available.
 +
* Team-working facilities are required by all industrial partners (particularly Bosch and SSF) - EMF Compare/merge tools are now under investigation to support a '''teamworking''' repository plug-in feature.
 +
* '''UML-B integration''' - since UML-B is based on EMF, the development of an EMF representation of Event-B enables UML-B concepts to be added as extensions.
  
* Structuring large specifications: it is difficult to read and edit large model; there is also a limit to the size of model that the Platform may handle comfortably and thus decomposition is an absolute necessity for large scale developments.
+
=== Choices / Decisions ===
* Decomposing proof effort: splitting helps to split verification effort. It also helps to reuse proofs: it is not unusual to return back in refinement chain and partially redo abstract models. Normally, this would invalidate most proofs in the dependent components. Model structuring helps to localise the effect of such changes. 
 
* Team development: large models may only be developed by a (often distributed) developers team.
 
* Model reuse: modules may be exchange and reused in different projects. The notion of interface make it easier to integrate a module in a new context. 
 
* Connection to library components
 
* Code generation/legacy code
 
  
= Choices / Decisions =
+
====UML-B improvements====
  
The pimary objective in the tool design was to provide a simple to use tool that could be used by a non-expert modeller. Of course, close integration with the core platform functionality was paramount.
+
The methods and modelling notations for refinement in UML-B were developed by experimentation using a case study of an ATM. The use of hierarchical nested state-machines (which were already available in UML-B) as a technique for adding detail in refinement was quickly adapted by making changes to the meta-model and translation. This technique was found to be suitable. Some further experimentation was needed in order to understand the need to link transitions of the nested state-machines with those in their parent. A concept of ''elaboration'' was introduced, whereby an elaborating  transition contributes guards and actions to the event produced from the elaborated parent transition. Transitions splitting (analogous to event splitting in Event-B refinements) is a natural consequence of refinement of states. An idea to ''bundle'' the split transitions in the parent state-machine so that the correspondence with the abstract refined state-machine is more obvious has not been pursued for now since it would add complication to the tooling.
  
* We have decided there is a need for a new type of Event-B component: interface. A decomposition based on explicit interface (rather than an implicit one such as in A-style decomposition) facilitates reuse of modules and makes it easier to provider a rich management infrastructure.  
+
====UML-B State-machine Animation====
 +
Initially, we attempted to model the animation state information as an extension to the UML-B meta-model. We discovered technological difficulties in extending EMF models in this way. Therefore,  we adopted an alternative solution using an independent meta-model of animation diagrams. These replicate parts of the structure of UML-B but add meta-properties to model the animation. When a model is to be animated, an animation model is constructed programmatically to match the UML-B model. Thereafter, the animation runs independently of UML-B. This has the additional benefit that the diagram can be simplified and tailored to better suit animation. For example, removing the editing palette.
  
* At some we had to make a decision of whether to make module integration more explicit and flexible or hide details under syntax sugar and thus achieve better model readability. We have decided that model readability should take priority over everything else. However, while model representation becomes more compact, it does not make proofs any easier.
+
====EMF Framework for Event-B====
 +
The structure of the EMF meta-model for Event-B was studied in great detail. Various options for  sub-packaging the model were tried but it has been found that it is more convenient for users to keep a simple package structure. Currently this consists of three packages; a ''core'' package containing abstract basis and project level meta-model, a ''machine'' package and a ''context'' package. A flexible abstract basis has been derived through experimentation. The abstract basis consists of an inheritance hierarchy of abstract meta-classes which provide great flexibility for writing code that deals with the meta-model in as generic a manner as possible. A driving factor in the design was to support both project level tools and component level tools. The latter should be able to manipulate a single machine or context without loading referenced components. This was achieved customising the EMF proxies (used in references) so that they are calculated lazily (when a request to resolve is received).
  
* During the initial experiments we have identified a need for multiple module instantiation. This allows a modeller to use several copies of the some module using a qualifier prefix to distinguish between objects imported from the modules.
+
=== Available Documentation ===
  
* One crucial point was realising modularisation support in such a way that structuring may be recursively applied within modules. Indeed, a module implemenation (module body) is a machine and thus it is self-similar to a caller context that is a machine.
+
UML-B Refinement is described in a paper which was presented at the FM2009 conference in Eindhoven. It is available here:
 +
:http://eprints.ecs.soton.ac.uk/18268/
  
* For the current version, we have not implemented the generation of enabledness condition logically required for module implementation. This condition, in some form, should be present in the Platform core.   
+
A tutorial on how to refine state-machines is available on the wiki:
 +
:[[Refinement_of_Statemachines]]
  
= Available Documentation =
+
State-machine animation is described on the wiki here:
 +
:[[UML-B_-_Statemachine_Animation]]
 +
It is also available as a short paper here:
 +
:http://eprints.ecs.soton.ac.uk/18261/
  
There is a dedicated wiki page covering the plugin functionality. Also, we are working on further documentation and tutorial.
+
The EMF Framework for Event-B is described on the wiki here:
 +
:[[EMF_framework_for_Event-B]]
 +
It is also available as a short paper here:
 +
:http://eprints.ecs.soton.ac.uk/18262/
  
* [[Plugin wiki|Modularisation Plug-in]]
+
=== Planning ===
* [[Plugin tutorial|Modularisation Plug-in Tutorial]]
 
* [[Installation guide|Modularisation Plug-in Installation Instructions]]
 
  
 +
UML-B integration
 +
* Develop extensibility mechanisms for EMF Event-B framework via experimentation with structured data (Records) plug-in.
 +
* Re-engineer UML-B Context diagrams as a diagrammatic view of Records
  
Two small-scale examples are available:
+
* Re-engineer UML-B package diagram based on EMF Event-B framework.
* [[http://iliasov.org/modplugin/ticketmachine.zip]] - a model of queue based on two ticket machine module instantiations (very basic)
 
* [[http://iliasov.org/modplugin/doors.zip]] - two doors sluice controller specification that is decomposed into a number of independent developments (few first steps only)
 
 
 
= Planning =
 
The plugin is available since Platform version 1.1. See the [[Modularisation Plug-in Release Notes|release notes]].
 
 
 
[[Category:D23 Deliverable]]
 

Revision as of 10:20, 4 December 2009

Overview

This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton.

A new plug-in feature has been developed to provide animation of UML-B state-machine diagrams. This feature was developed by University of Southampton.

The longer term development of UML-B relies on an EMF representation of Event-B. The development of a new EMF Event-B plugin-in feature is also described in this section. This feature was initially developed by University of Southampton, Heinrich-Heine University, Duesseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.

Motivations

UML-B improvements

The current version of the UML-B tool has been improved to support the refinement of state-machines. At the last deliverable, refinement of classes was supported and state-machine refinement was beginning to be investigated. The investigation has experimented several notation and methodological alternatives. The design has now been finalised and an implementation has been achieved. State-machines can be refined by adding nested state-machines inside states. Some of the transitions in the nested state-machine do not represent new events but contribute to the refinements of existing transitions in the parent state-machine. A concept of transition elaboration has been invented to represent this relationship.

Many other minor improvements have been made to the UML-B tool including: collapsing empty compartments on diagrams, improved navigation between diagrams, improved properties views, ability to order classes and class-types in the translation, support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems).

UML-B State-machine Animation

This feature was developed in response to a requirement from Siemens Transportation. Several state-machines can be selected (representing refinements and hierarchical nesting) for simultaneous animation. The animation relies on Pro-B animation of the corresponding Event-B models (that have been automatically generated by UML-B). The animated diagrams show the currently active states and the enabled transitions. Events can be 'fired' by clicking on the enabled transition. Where the state-machine belongs to a class, instances of the class can be seen moving from state to state.

EMF Framework for Event-B

An EMF (Eclipse Modelling Framework) based representation of Event-B was developed and made available as a plug-in feature for Rodin. This enables Event-B machines and contexts to be loaded into EMF based tools. Serialisation (i.e. loading and saving) is performed via the Rodin API. This feature can be viewed as an enabling technology. Hence motivation derives from several sources including:

  • A Text editor was requested by several industrial and academic partners - A fully-featured EMF based text editor (Camille) has been developed by Duesseldorf and is now available.
  • Team-working facilities are required by all industrial partners (particularly Bosch and SSF) - EMF Compare/merge tools are now under investigation to support a teamworking repository plug-in feature.
  • UML-B integration - since UML-B is based on EMF, the development of an EMF representation of Event-B enables UML-B concepts to be added as extensions.

Choices / Decisions

UML-B improvements

The methods and modelling notations for refinement in UML-B were developed by experimentation using a case study of an ATM. The use of hierarchical nested state-machines (which were already available in UML-B) as a technique for adding detail in refinement was quickly adapted by making changes to the meta-model and translation. This technique was found to be suitable. Some further experimentation was needed in order to understand the need to link transitions of the nested state-machines with those in their parent. A concept of elaboration was introduced, whereby an elaborating transition contributes guards and actions to the event produced from the elaborated parent transition. Transitions splitting (analogous to event splitting in Event-B refinements) is a natural consequence of refinement of states. An idea to bundle the split transitions in the parent state-machine so that the correspondence with the abstract refined state-machine is more obvious has not been pursued for now since it would add complication to the tooling.

UML-B State-machine Animation

Initially, we attempted to model the animation state information as an extension to the UML-B meta-model. We discovered technological difficulties in extending EMF models in this way. Therefore, we adopted an alternative solution using an independent meta-model of animation diagrams. These replicate parts of the structure of UML-B but add meta-properties to model the animation. When a model is to be animated, an animation model is constructed programmatically to match the UML-B model. Thereafter, the animation runs independently of UML-B. This has the additional benefit that the diagram can be simplified and tailored to better suit animation. For example, removing the editing palette.

EMF Framework for Event-B

The structure of the EMF meta-model for Event-B was studied in great detail. Various options for sub-packaging the model were tried but it has been found that it is more convenient for users to keep a simple package structure. Currently this consists of three packages; a core package containing abstract basis and project level meta-model, a machine package and a context package. A flexible abstract basis has been derived through experimentation. The abstract basis consists of an inheritance hierarchy of abstract meta-classes which provide great flexibility for writing code that deals with the meta-model in as generic a manner as possible. A driving factor in the design was to support both project level tools and component level tools. The latter should be able to manipulate a single machine or context without loading referenced components. This was achieved customising the EMF proxies (used in references) so that they are calculated lazily (when a request to resolve is received).

Available Documentation

UML-B Refinement is described in a paper which was presented at the FM2009 conference in Eindhoven. It is available here:

http://eprints.ecs.soton.ac.uk/18268/

A tutorial on how to refine state-machines is available on the wiki:

Refinement_of_Statemachines

State-machine animation is described on the wiki here:

UML-B_-_Statemachine_Animation

It is also available as a short paper here:

http://eprints.ecs.soton.ac.uk/18261/

The EMF Framework for Event-B is described on the wiki here:

EMF_framework_for_Event-B

It is also available as a short paper here:

http://eprints.ecs.soton.ac.uk/18262/

Planning

UML-B integration

  • Develop extensibility mechanisms for EMF Event-B framework via experimentation with structured data (Records) plug-in.
  • Re-engineer UML-B Context diagrams as a diagrammatic view of Records
  • Re-engineer UML-B package diagram based on EMF Event-B framework.