Difference between pages "D23 Rule-based Prover" and "D23 UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Im06r
 
imported>Colin
 
Line 1: Line 1:
[[Category:D23_Deliverable]]
+
=== Overview ===
==Overview==
+
This part of the deliverable describes improvements to the UML-B plug-in feature, which is the responsibility of University of Southampton.
  
The rule-based prover plug-in offers a uniform mechanism to define and validate proof rules which can then be used in proofs.
+
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 rule-based prover plug-in has two important components:
+
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, Düsseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.
*The Theory construct: where rules are defined and validated by means of proof obligations. Defining a rule includes stating whether it should be applied automatically, interactively or both.
 
*Prover Extension: which is responsible for checking what rules are applicable and applying them.
 
  
The plug-in supports the definition and validation of rewrite rules. It is expected that the plug-in will also support defining inference rules.
+
=== Motivations ===
  
The University of Southampton was responsible for the development of the rule-based prover.
+
====UML-B Support for State machine Refinement====
  
==Motivations==
+
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.
  
Extensibility is a major concern for theorem provers. The Rodin proving infrastructure offers an extensible mechanism where proof rules can be added and external provers can be plugged-in. However, it has the following limitations:
+
====UML-B General Improvements====
* In order to add a new proof rule, it is required to implement a rule schema (i.e., a reasoner) and a wrapper tactic. Therefore, a certain level of competence with the Java programming language as well as knowledge of Rodin architecture is necessary;
+
Many other minor improvements have been made to the UML-B tool including:
*After a new rule is added, soundness of the prover augmented with the new rule has to be established. It is not clear how this can be achieved at the level of Java code.
+
* collapsing empty compartments on diagrams,
 +
* improved navigation between diagrams,
 +
* improved properties views,
 +
* ability to order classes and class-types in the output translation,
 +
* support for theorems everywhere (i.e. invariants and axioms can now be designated as theorems).
  
The rule-based prover is an attempt to address the aforementioned limitations in a uniform and effective fashion. It is uniform because it offers the user (we shall call a theory developer) the possibility to develop and validate theories in a similar way to developing and validating models. It is also effective since it relieves the theory developer from writing Java code, and covers most of the rewrite rules available at:
+
====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.
  
http://wiki.event-b.org/index.php/All_Rewrite_Rules
+
The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon.
  
The advantages of the rule-based prover include:
+
[[Image:SmAnimScreenshot.png]]
  
* The rule-based prover unifies the way automatics and interactive rules are defined since this is literally specified by two toggle buttons.
+
====EMF Framework for Event-B====
* The addition and validation of new proof rules brings a degree of meta-reasoning to Rodin, and removes the need for Java code when adding rules.
 
* The theory construct provide a platform where prover extensions and (in the future) language extensions can be specified.
 
* Carefully checked library of rules can be provided.
 
  
==Choices/Decisions==
+
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:
The main decisions that had to be made regarding the rule-based prover include the following:
+
* A Text editor was requested by several industrial and academic partners - A fully-featured EMF based text editor ('''Camille''') has been developed by Düsseldorf and is now available.
*Whether to use contexts as a vehicle for defining rules;
+
* 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.
*What kind of rules should the theory cover first;
+
* '''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.
*How the meta-variables within rules are recognised (automatic type inference or not).
 
  
The following key points summarise the different decisions/choices that have been made:
+
=== Choices / Decisions ===
  
*Contexts describe the static properties of models, and they are used to parameterise machines. Adding the capability of defining proof rules within contexts would allow the co-existence of modelling elements and meta-logical elements with no clear relationship between the two. This may require significant changes to the core architecture, and will unnecessarily overload the functionality of contexts with elements not directly relevant to modelling. As such, a clear separation of modelling and meta-reasoning was adopted. This resulted in a theory construct that acts as a placeholder for prover extensions.
 
*Rodin has a collection of rewrite and inference rules. Most inference rules as found in
 
  
:http://wiki.event-b.org/index.php/Inference_Rules
+
====UML-B Support for State machine Refinement====
 +
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. Transition 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.
  
:require predicate variables to be defined. This is not the case for most rewrite rules as found in
+
====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.
  
:http://wiki.event-b.org/index.php/All_Rewrite_Rules .  
+
====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).
  
:Since predicate variables were not available when the development started, it was decided to cover rewrite rules first.
+
=== Available Documentation ===
  
==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 Language and Tool Support for Class and State Machine Refinement in UML-B]
  
==Planning ==
+
A tutorial on how to refine state-machines is available on the wiki:
 +
:[http://wiki.event-b.org/index.php/Refinement_of_Statemachines Refinement of Statemachines]
 +
 
 +
State-machine animation is described on the wiki here:
 +
:[http://wiki.event-b.org/index.php/UML-B_-_Statemachine_Animation UML-B - Statemachine Animation]
 +
It is also available as a short paper here:
 +
:[http://eprints.ecs.soton.ac.uk/18261 Animation of UML-B State-machines]
 +
 
 +
The EMF Framework for Event-B is described on the wiki here:
 +
:[http://wiki.event-b.org/index.php/EMF_framework_for_Event-B EMF framework for Event-B]
 +
It is also available as a short paper here:
 +
:[http://eprints.ecs.soton.ac.uk/18262 An EMF Framework for Event-B]
 +
 
 +
=== 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.
 +
 
 +
[[Category:D23 Deliverable]]

Revision as of 21:58, 27 January 2010

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, Düsseldorf and University of Newcastle. It is now mostly maintained and developed by University of Southampton.

Motivations

UML-B Support for State machine Refinement

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.

UML-B General Improvements

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 output 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.

The screenshot below shows a statemachine (top left) and its refinement (top right) being animated in parallel with the nested statemachines (bottom left and right) that are contained in the refined states. Two class instances are currently active; one models an ATM that is not available (e.g. in maintenace) and the other is in the process of validating a card. Transitions that are enabled for one or other of the class instances are emboldened. (The instance to be used when a transition is fired is selected when the transitions is clicked upon.

SmAnimScreenshot.png

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 Düsseldorf 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 Support for State machine Refinement

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. Transition 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:

Language and Tool Support for Class and State Machine Refinement in UML-B

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:

Animation of UML-B State-machines

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:

An EMF Framework for Event-B

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.