Difference between pages "Current Developments" and "D32 UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
imported>Colin
 
Line 1: Line 1:
−
{{TOCright}}
+
= Overview =
−
This page sum up the known developments that are being done around or for the [[Rodin Platform]]. ''Please contributes informations about your own development to keep the community informed''
+
The main progress on UML-B has been to implement new features, improve usability and fix bugs. As in the previous years of DEPLOY, these bugs and features are reported either by mail or through dedicated SourceForge trackers.
  
−
== Deploy Tasks ==
+
The list below gives an overwiew of the noteworthy features added in UML-B during the past year:
−
The following tasks were planned at some stage of the [[Deploy]] project.
+
* Additional features added to state machines to support transitions emanating from multiple states
−
=== Core Platform ===
+
: It is often the case that a transition may occur from several (possibly all) states within a state-machine. Such models were impossible to represent in UML-B. Two pseudo-states were added to represent this. Firstly an 'ANY' pseudo-state can be used as a transition source to represent that the transition can occur from ANY state of the state-machine. Secondly a disjunctive pseudo-state can be used to combine several transitions from different source states into a single transition.
−
==== New Mathematical Language ====
 
−
==== Rodin Index Manager ====
 
−
[[Systerel]] is in charge of this task.
 
−
{{details|Rodin Index Design|Rodin index design}}
 
  
−
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.  
+
* Support (Conceptual) Singleton classes - no instances generated:
 +
:Occasionally a conceptual grouping of associated modelling elements is desired without generating the lifting mechanisms of a class.  
  
−
==== Text Editor ====
+
* enable super-type arrows to target ExtendedClassTypes and RefinedClasses
−
The efforts in [[Düsseldorf]] ([[User:Fabian|Fabian]]) and [[Newcastle]] ([[User:Alexei|Alexei]]) have been joined to create a single text editor which will be part of the [[#EMF framework for Rodin|EMF framework for Rodin]] (see that [[#EMF framework for Rodin|section]] for details).
 
  
−
==== EMF framework for Event-B ====
+
* provide convergence property on state transitions
−
Newcastle, Southampton and Düsseldorf have begun to develop an EMF framework to support Rodin modelling tools based on EMF. The framework includes an EMF representation of Event-B, a synchronising persistence interface for loading and saving models via the Rodin API and facilities to support text editing and parsing. Examples of tools that will be based on the EMF framework for Rodin are, a Text editor, a compare/merge editor (which can be used for team based development), pattern/composition tools, Diagram Editors. 
 
  
−
More details can be found here: [[EMF framework for Event-B]]
+
* report to user if translation didn't proceed due to model validator
  
−
=== Plug-ins ===
+
* improve refresh of diagrams for error marking and for properties changes
−
==== Requirement Management Plug-in ====
 
−
[[User:Jastram|Michael]] at [[Düsseldorf]] is in charge of the [[:Category:Requirement Plugin|Requirements Management Plug-in]].
 
  
−
{{See also|ReqsManagement|Requirements Tutorial|l1=Requirements Management Plug-in}}
+
* improvements and additions to model validations
  
−
This plug-in allows:
+
* correct and improve missing default labelling in diagrams
−
* Requirements to be edited in a set of documents (independently from Rodin)
 
−
* Requirements to be viewed within Rodin
 
−
* Individual Requirements to be linked to individual Event-B-Entities
 
−
* A basic completion test to be performed
 
  
−
==== UML-B Improvements ====
+
* corrections and improvements to automatic diagram deletion.
−
[[Southampton]] is in charge of [[UML-B]] plug-in.
 
  
−
A new version of UML-B is being developed that will have improved integration with Event-B. The new version will be built as an extension to the EMF framework for Event-B. While this new version is being developed improvements are also being made to the existing version of UML-B. Both topics are covered in more detail on the following page:
+
* Requires Rodin 2.0 (Eclipse 3.6 and JVM 1.6)
−
[[UML-B Integration and Improvements]]
+
 +
* Improved management of diagram files when model changes
  
−
==== ProB Plug-in ====
+
* Add preference for line routing style (default rectilinear) for each diagram type
−
[[Düsseldorf]] is in charge of [[ProB]].
 
−
<!-- {{details|ProB current developments|ProB current developments}} -->
 
  
−
===== Work already performed =====
+
* Add missing comment fields in properties view
  
−
We have now ported ProB to work directly on the Rodin AST. Animation is working and the user can now set a limited number of preferences.
 
−
The model checking feature is now also accessible.
 
−
It is also possible to create CSP and classical B specification files. These files can be edited with BE4 and animated/model checked with ProB.
 
−
On the classical B side we have moved to a new, more robust parser (which is now capable of parsing some of the more complicated AtelierB
 
−
specifications from Siemens).
 
  
−
On the developer side, we have moved to a continuous integration infrastructure using CruiseControl. Rodin is also building from CVS in that infrastructure.
+
UML-B State-machine Animation Plug-in is a new feature developed by University of Southampton as a response to a request from industrial partners to support the animation of UML-B state-machine diagrams. The essence of request was to provide a means of visualising the animation and model-checking process of Event-B machines modelled in UML-B tool, in particular state-machines, thus to simplify this process. The tool integrates the capabilities of ProB animation and UML-B tool's notation.
  
−
===== Ongoing and future developments=====
+
= Motivations =
  
−
We are currently developing a new, better user interface.
+
Enhancements to state diagram drawing. Several case studies were involving state machine diagrams which were problematic because particular transitions could be enabled from any sub-state. there was no way to represent these cases in UML-B.  
−
We also plan to support multi-level animation with checking of the gluing invariant.
 
  
−
We have prototypes for several extensions working, but they need to be fully tested and integrated into the plugin:
+
The motivation for the Animation Plug-in was to extend already beneficial graphical notation of UML-B with animation capabilities similar to those that ProB tool provides for Event-B models. With the aid of such a plug-in animation and model checking would be possible on UML-B diagrams instead of translated and less obvious Event-B code. The resulting plug-in uses ProB tool to run the standard animation on translated models and animates UML-B state-machines at the same time.
−
* an inspector that allows the user to inspect complex predicates (such as invariants or guards) as well as expressions in a tree-like manner
 
−
* a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
 
−
* a 2D viewer to inspect the state space of the specification
 
  
−
==== B2Latex Plug-in ====
+
= Choices / Decisions =
−
[[Southampton]] is in charge of [[B2Latex]].
+
* Integrated UML-B
 +
: It was planned to develop a new version (iUML-B) of UML-B which is more integrated with Event-B. A precursor stage to this was to develop an EMF representation of Event-B. This was completed last year and is now used successfully by several plug-ins. A Records plug-in was developed in response to user requests. The Records plug-in was implemented as an extension to the Event-B EMF framework. This was seen as a 'practice run' before attempting a similar extension to support UML-B. However, the Records plug-in took longer than expected and this has delayed work on iUML-B. Some progress on iUML-B has recently been made with the release of a project level diagram tool for Event-B and some progress on representing State-Machine diagram models as an extension to the Event-B EMF models.
  
−
Kriangsak Damchoom will update the plug-in to add [[Event Extension|extensions of events]].
+
* State-machine Animation Plug-in
 +
: The initial design decision was to extend the UML-B metamodel with the animation components. Due to difficulties with UML-B diagram extensibility an alternative option was determined - to create a separate model, derived from UML-B state-machine subset, with incorporated animation support. This design was successfully implemented together with ProB and Rodin UI extensions into Animation plug-in, which supports such UML-B concepts as classes and different state-machine translation kinds, as well as Event-B refinement.
  
−
==== Parallel Composition Plug-in ====
+
= Available Documentation =
−
[[Southampton]] is in charge of the [[Parallel Composition using Event-B]] .
+
The following pages give useful information about UML-B:
 +
* Lectures<ref>http://wiki.event-b.org/index.php/UML-B</ref>.
 +
* Tutorials<ref>http://wiki.event-b.org/index.php/UML-B</ref>.
 +
* Worked Examples<ref>http://wiki.event-b.org/index.php/UML-B</ref>.
  
−
The intention of the plug-in is to allow the parallel composition of events using Event-B syntax. The composition uses a value-passing style (shared event composition), where parameters can be shared/merged.
+
UML-B State-machine Animation Plug-in:
 +
* General information<ref>http://wiki.event-b.org/index.php/UML-B_-_Statemachine_Animation</ref>
 +
* Tutorial<ref>http://wiki.event-b.org/index.php/Statemachine_Animation_Tutorial</ref>
  
−
This plug-in allows:
+
= Planning =
−
* Selection of machines that will be part of the composition (''Includes'' Section)
+
During the coming year, special efforts will be made on the following topics,
−
* Possible selection of an abstract machine (''Refines'' Section)
+
* Development of the Project Diagram Plugin for Event-B to make it extensible and/or to automatically cater for future component types.
−
* Possible inclusion of invariants that relate the included machines (''Invariant'' Section and use of the monotonicity )
+
: <explain!>
−
* Invariants of included machines are conjoined.
+
* Development of a State-machine diagram plug-in as an integrated part of Event-B modelling
−
* Selection of events that will be merged. The event(s) must come from different machines. At the moment, events with parameters with same name are merged. If it is a refinement composition, it is possible to choose the abstract event that is being refined.
+
: <explain!>
−
* Initialisation event is the parallel composition of all the included machines' initialisations.
 
−
* For a composed event, the guards are conjoined and the all the actions are composed in parallel.
 
  
−
Currently, after the conclusion of the composition machine, a new machine can be generated, resulting from the properties defined on the composition file. This allows proofs to be generated as well as a visualisation of the composition machine file. In the future, the intention is to make the validation directly on the composition machine file directly where proofs would be generated ( and discharged) - the new machine generation would be optional. An event-b model for the validation/generation of proofs in currently being developed. Another functionality which should be quite useful for the composition (but not restricted to that) is '''renaming''':
 
  
−
* while composing, two machines may have variables with the same name for instance (which is not allowed for this type of composition). In order to solve this problem, one would have to rename one of the variables in order to avoid the clash, which would mean change the original machine. A possible solution for that would be to rename the variable but just on composition machine file, keeping the original machine intact. A renaming framework designed and developed by Stefan Hallerstede and Sonja Holl exists currently although still on a testing phase. The framework was developed to be used in a general fashion (not constrained to event-b syntax). The idea is to extend the development of this framework and apply to Event-B syntax (current development).
+
=References=
 +
<references/>
  
−
There is a prototype for the composition plug-in available that works for Rodin 0.8.2. A release for the Rodin 0.9 is concluded and will be available from the Rodin Main Update Site soon, under 'Shared Event Composition' update.
+
[[Category:D32 Deliverable]]
−
 
 
−
==== Measurement Plug-In ====
 
−
 
 
−
The [[Measurement Plug-In]] to the RODIN platform will provide information both about the model itself and about the process of building the model.
 
−
It has a double purpose:
 
−
 
 
−
* provide feedback to the user about the quality of the Event-B model he is building and about potential problems in it or in the way he is building it.
 
−
* automate the data collection process for the measurement and assessment WP. This data collected will be analyzed to identify global transfer (increase in model quality, size, complexity,...), tool shortcomings (usability, prover), modelling issues (to be addressed by training, language, tool evolution,...), etc.
 
−
 
 
−
== Exploratory Tasks ==
 
−
=== One Single View ===
 
−
[[Maria]] is in charge of this exploratory work during is internship.
 
−
{{details|Single View Design|Single View Design}}
 
−
The goal of this project is to present everything in a single view in Rodin. So the user won't have to switch perspectives.
 
−
 
 
−
 
 
−
 
 
−
== Others ==
 
−
 
 
−
=== AnimB ===
 
−
[[Christophe]] devotes some of its spare time for this plug-in.
 
−
{{details|AnimB Current Developments|AnimB Current Developments}}
 
−
The current developments around the [[AnimB]] plug-in encompass the following topics:
 
−
;Live animation update
 
−
:where the modification of the animated event-B model is instantaneously taken into account by the animator, without the need to restart the animation.
 
−
;Collecting history
 
−
:The history of the animation will be collected.
 
−
 
 
−
=== Team-Based Development ===
 
−
 
 
−
; Usage Scenarios
 
−
: In order to understand the problem properly, [http://www.stups.uni-duesseldorf.de/ Düsseldorf] created a number of usage [[Scenarios for Team-based Development]].
 
−
: A page as also been opened for [[Scenarios for Merging Proofs|merging proofs scenarios]].
 
−
[[Category:Work in progress]]
 
−
 
 
−
=== B2C ===
 
−
This plug-in translates Event-B models to C source code, which may then be compiled using external C development tools. [[Steve]] wrote B2C with the specific purpose of translating the  [http://dx.doi.org/10.1007/978-3-540-87603-8_21 MIDAS] model, an Event-B implementation of a Virtual Machine instruction set.
 
−
 
 
−
B2C supports a sub-set of Event-B that can be easily translated to C form. The user provides a final refinement step that does nothing except restate the model in this translatable form: symbolic constants must be replaced by their literal values, range membership guards are replaced by greater-than and less-than guards, and actions are restated not to use global statments on their left-sides (this because the variable may have been modified by an earlier action, and may not be valid). The manipulations are done within EventB where they can be checked by the Proof Obligation system, and B2C made as simple as possible to maximise reliability. This re-write process is currently a manual step, but could in principle be done by another plug-in
 
−
 
 
−
B2C source code is not currently available for download: contact [[Steve]] directly if it is required.
 
−
 
 
−
 
 
−
 
 
−
=== New Proof Rules ===
 
−
 
 
−
[[New Proof Rules|This document]] describes the set of newly added reasoners for improving the usability of the prover within Rodin Platform.
 

Revision as of 20:44, 25 November 2010

Overview

The main progress on UML-B has been to implement new features, improve usability and fix bugs. As in the previous years of DEPLOY, these bugs and features are reported either by mail or through dedicated SourceForge trackers.

The list below gives an overwiew of the noteworthy features added in UML-B during the past year:

  • Additional features added to state machines to support transitions emanating from multiple states
It is often the case that a transition may occur from several (possibly all) states within a state-machine. Such models were impossible to represent in UML-B. Two pseudo-states were added to represent this. Firstly an 'ANY' pseudo-state can be used as a transition source to represent that the transition can occur from ANY state of the state-machine. Secondly a disjunctive pseudo-state can be used to combine several transitions from different source states into a single transition.
  • Support (Conceptual) Singleton classes - no instances generated:
Occasionally a conceptual grouping of associated modelling elements is desired without generating the lifting mechanisms of a class.
  • enable super-type arrows to target ExtendedClassTypes and RefinedClasses
  • provide convergence property on state transitions
  • report to user if translation didn't proceed due to model validator
  • improve refresh of diagrams for error marking and for properties changes
  • improvements and additions to model validations
  • correct and improve missing default labelling in diagrams
  • corrections and improvements to automatic diagram deletion.
  • Requires Rodin 2.0 (Eclipse 3.6 and JVM 1.6)
  • Improved management of diagram files when model changes
  • Add preference for line routing style (default rectilinear) for each diagram type
  • Add missing comment fields in properties view


UML-B State-machine Animation Plug-in is a new feature developed by University of Southampton as a response to a request from industrial partners to support the animation of UML-B state-machine diagrams. The essence of request was to provide a means of visualising the animation and model-checking process of Event-B machines modelled in UML-B tool, in particular state-machines, thus to simplify this process. The tool integrates the capabilities of ProB animation and UML-B tool's notation.

Motivations

Enhancements to state diagram drawing. Several case studies were involving state machine diagrams which were problematic because particular transitions could be enabled from any sub-state. there was no way to represent these cases in UML-B.

The motivation for the Animation Plug-in was to extend already beneficial graphical notation of UML-B with animation capabilities similar to those that ProB tool provides for Event-B models. With the aid of such a plug-in animation and model checking would be possible on UML-B diagrams instead of translated and less obvious Event-B code. The resulting plug-in uses ProB tool to run the standard animation on translated models and animates UML-B state-machines at the same time.

Choices / Decisions

  • Integrated UML-B
It was planned to develop a new version (iUML-B) of UML-B which is more integrated with Event-B. A precursor stage to this was to develop an EMF representation of Event-B. This was completed last year and is now used successfully by several plug-ins. A Records plug-in was developed in response to user requests. The Records plug-in was implemented as an extension to the Event-B EMF framework. This was seen as a 'practice run' before attempting a similar extension to support UML-B. However, the Records plug-in took longer than expected and this has delayed work on iUML-B. Some progress on iUML-B has recently been made with the release of a project level diagram tool for Event-B and some progress on representing State-Machine diagram models as an extension to the Event-B EMF models.
  • State-machine Animation Plug-in
The initial design decision was to extend the UML-B metamodel with the animation components. Due to difficulties with UML-B diagram extensibility an alternative option was determined - to create a separate model, derived from UML-B state-machine subset, with incorporated animation support. This design was successfully implemented together with ProB and Rodin UI extensions into Animation plug-in, which supports such UML-B concepts as classes and different state-machine translation kinds, as well as Event-B refinement.

Available Documentation

The following pages give useful information about UML-B:

  • Lectures[1].
  • Tutorials[2].
  • Worked Examples[3].

UML-B State-machine Animation Plug-in:

  • General information[4]
  • Tutorial[5]

Planning

During the coming year, special efforts will be made on the following topics,

  • Development of the Project Diagram Plugin for Event-B to make it extensible and/or to automatically cater for future component types.
<explain!>
  • Development of a State-machine diagram plug-in as an integrated part of Event-B modelling
<explain!>


References

  1. ↑ http://wiki.event-b.org/index.php/UML-B
  2. ↑ http://wiki.event-b.org/index.php/UML-B
  3. ↑ http://wiki.event-b.org/index.php/UML-B
  4. ↑ http://wiki.event-b.org/index.php/UML-B_-_Statemachine_Animation
  5. ↑ http://wiki.event-b.org/index.php/Statemachine_Animation_Tutorial
Retrieved from ‘https://wiki.event-b.org/index.php?title=Current_Developments&oldid=2658’