Difference between pages "D32 Model Animation" and "D32 UML-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Daniel
 
imported>Tommy
m
 
Line 1: Line 1:
−
= Model Animation =  
+
= 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.
  
−
== Overview ==
+
The list below gives an overwiew of the noteworthy features added in UML-B during the past year:
−
=== Siemens Application===
+
* Additional features added to state machines to support transitions emanating from multiple states
−
The most important additions of the last 12 months are:
+
: 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.
−
* Application of ProB in three active deployments, namely the upgrading of the Paris Metro Line 1 for driverless trains, line 4 of the S\~{a}o Paulo metro and line 9 of the Barcelona metro. We also briefly report on experiments on the models of the CDGVAL shuttle. The paper <ref name="fm2009">Leuschel et al. FM'2009</ref> only contained the initial San Juan case study, which was used to evaluate the potential of our approach.
 
−
* In this article we describe the previous method adopted by Siemens in much more detail,  as well as explaining the performance issues with Atelier B.
 
−
* Comparisons and empirical evaluations with other potential approaches and alternate tools (Brama, AnimB, BZ-TT and TLC) have been conducted.
 
−
* We provide more details about the ongoing validation process of ProB, which is required by Siemens for it to use ProB to replace the existing method.
 
  
−
The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
+
* 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.  
−
Also, since  <ref name="fm2009"/>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).
+
 
 +
* enable super-type arrows to target ExtendedClassTypes and RefinedClasses
  
−
More details:
+
* provide convergence property on state transitions
−
* <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
 
−
* <ref>Leuschel et al. Draft of Validation Report</ref>
 
  
−
=== Multi-level Animation ===
+
* report to user if translation didn't proceed due to model validator
−
(ABZ'2010 & SCP journal paper)
 
  
−
=== Evaluation of the ProB Constraint Solver ===
+
* improve refresh of diagrams for error marking and for properties changes
−
Various industrial applications have shown the need for improved constraint-solving capabilities (see CBC Deadlock, Test-Case Generation). In order to evaluate ProB, and detect areas for improvement, we have studied to what extent classical constraint satisfaction problems can be  conveniently expressed as B predicates, and then solved by ProB. In particular, we have studied problems such as the n-Queens problem, graph colouring, graph isomorphism detection, time tabling, Sudoku, Hanoi, magic squares, Alphametic puzzles, and several more. We have then compared the performance with respect to other tools, such as the model checker TLC  for TLA+, AnimB for Event-B,  and Alloy.
 
−
 
 
−
The experiments show that some constraint satisfaction problems can be expressed very conveniently in B and solved very effectively with ProB. For example, TLC takes 8747 seconds (2 hours 25 minuts) to solve the 9-queens problem expressed as a logical predicate; Alloy 4.1.10 with minisat takes 0.406 seconds, ProB 1.3.3 takes 0.01 seconds. For 32 queens, ProB 1.3.3 takes 0.28 seconds, while Alloy 4.1.10 with minisat takes over 4 minutes (TLC was only able to solve the n-queens problem up until n=9, or n=14 when reformulating the problem as a model checking problem rather than a constraint-solving problem). In another small experiment, we checked whether two graphs with 9 nodes of out-degree exactly one are isomorphic by checking for the existence of a permutation which preserved the graph structure. TLC finds a permutation after 2 hours 6 minutes and 28 seconds; ProB 1.3.3 takes 0.01 seconds to find the same solution, while Alloy takes 0.11 seconds with SAT4J and 0.05 seconds with minisat.
 
−
For some other examples (in particular time-tabling) involving operators such as the relational image, the performance of ProB is still sub-optimal with respect to, e.g., Alloy; we plan to overcome this shortcoming in the future. Our long term goal is that B can not only be used to as a formal method for developing safety critical software, but also as a high-level constraint  programming language.
 
  
−
=== Constraint-Based Deadlock Checking ===
+
* improvements and additions to model validations
−
Ensuring the absence of deadlocks is important for certain applications, in particular for Bosch's Adaptive Cruise Control. We are tackling the problem of finding deadlocks via constraint solving rather than by model checking. Indeed, model checking is problematic when the out-degree is very large. In particular, quite often there can be a practically infinite number of ways to instantiate the constants of a B model. In this case, model checking will only find deadlocks for the given constants
 
−
chosen.
 
  
−
Idea: solve constraints of axioms, invariant together with a constraint specifying a deadlock.
+
* correct and improve missing default labelling in diagrams
  
−
Required Developments:
+
* corrections and improvements to automatic diagram deletion.
−
* implementation of the algorithm, with semantic relevance filtering (to be able to restrict the deadlock search to certain scenarios: in Bosch's case due to the flow plugin, one wants to restrict deadlock checking e.g. to states with the variable Counter set to 10).
 
−
* Improvements to ProB's constraint solving engine: (reification of constraints, more precise information propagation for membership constraints, performance improvments in the typchecker and other parts of the kernel)
 
  
−
Success: Model 1 and Model 2: CrCtrl_Comb2Final;
+
* Requires Rodin 2.0 (Eclipse 3.6 and JVM 1.6)
−
relevance of Counter=10 due to flow
+
 +
* Improved management of diagram files when model changes
  
−
Deadlock Freedom PO: 34 pages of ASCII, could not be loaded in Rodin "Java Heap Space Error". Counter examples found for 8 versions in 1-18 seconds.
+
* Add preference for line routing style (default rectilinear) for each diagram type
  
−
=== BMotionStudio for Industrial Models ===
+
* Add missing comment fields in properties view
  
−
Previously, we presented BMotion Studio, a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. However, BMotion Studio had not yet reached the status of an Industrial strength tool due to the lack of important features known from modern editors.
 
  
−
In this work we present the improvements to BMotion Studio mainly aimed at upgrading it to an industrial strength tool and to show that we can apply the benefits of BMotion Studio for visualizing more complex models which are on the level of industrial applications. In order to reach this level the contribution of this work consists of three parts:
+
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.
  
−
* We added a lot of new features to the graphical editor known from modern editors like: Copy-paste support, undo-redo support, rulers, guides and error reporting. One step towards was the redesign of the graphical editor with GEF.
+
= Motivations =
−
* Since extensibility is a very important design principle for reaching the level of an industrial strength tool we pointed up the extensibility options of BMotion Studio.
+
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 introduced the visualization for two models which are on the level of industrial applications in order to demonstrate that we can apply the benefits of BMotion Studio for visualizing more complex models. The first model is a mechanical press controller and the second model is a train system which manages the crossing of trains in a certain track network.
 
  
−
=== Various other improvements ===
+
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.
  
−
mainly inspired by Siemens and Bosch Applications
+
= 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.
  
−
Improved AVL algorithms, more operators
+
* 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.
  
−
record support, treatment of infinite sets,
+
= Available Documentation =
 +
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>.
  
−
== Motivations ==
+
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>
  
−
The above works were motivated mainly to support the following three industrial deployments:
+
= Planning =
−
* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
+
During the coming year, special efforts will be made on the following topics,
−
* Bosch: provide animation and constraint-based deadlock detection for the Adaptive Cruise Control
+
* Development of the Project Diagram Plugin for Event-B to make it extensible and/or to automatically cater for future component types.
−
* SAP: provide a way to generate test cases using constraint-based animation
+
: The current version of the Project Diagram Plugin only supports Machines and Contexts and their relationships. Already, several plug-ins are contributing new kinds of components such as theories, tasking machines and compositions. The Project Diagram plug-in will be enhanced to provide an extension mechanism that allow other plug-ins to extend the project diagram to show new kinds of components and their relationship.
 +
* Development of a State-machine diagram plug-in as an integrated part of Event-B modelling
 +
: The State-machine diagram plug-in will provide a diagrammatic modelling environment based on state-machines alongside the usual Event-B modelling format. The two views will contribute to the same model simultaneously.
  
−
== Available Documentation ==
+
In parallel with these new plug-ins, the current version of UML-B will continue to be enhanced. This may include some new modelling features such as better support for synchronisation of state-machines and support for more UML modelling details. However, usability of the current features is seen as the main objective. This will include,
 +
* Support for copy, cut and paste of diagram elements so that they can be moved and/or replicated more easily,
 +
* Support for re-attaching links (e.g. transitions) to different source/target elements,
 +
* Facilities for refactoring/renaming elements,
 +
* Support for the event extension mechanism of Event-B,
 +
* Integration of Context Diagram model elements on Class diagrams,
 +
* Improve facilities for navigating between state-machines and visualising multiple state-machines.
  
−
=== References ===
+
= References =
 
<references/>
 
<references/>
  
−
== Planning ==
+
[[Category:D32 Deliverable]]
−
 
 
−
* Finish Validation Report
 
−
* Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
 
−
* Support mathematical extensions in ProB
 
−
* Further improvements in the constraint-solving kernel of ProB; in particular for relations and operators. A Kodkod translator is being developed.
 

Revision as of 10:17, 20 December 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.
The current version of the Project Diagram Plugin only supports Machines and Contexts and their relationships. Already, several plug-ins are contributing new kinds of components such as theories, tasking machines and compositions. The Project Diagram plug-in will be enhanced to provide an extension mechanism that allow other plug-ins to extend the project diagram to show new kinds of components and their relationship.
  • Development of a State-machine diagram plug-in as an integrated part of Event-B modelling
The State-machine diagram plug-in will provide a diagrammatic modelling environment based on state-machines alongside the usual Event-B modelling format. The two views will contribute to the same model simultaneously.

In parallel with these new plug-ins, the current version of UML-B will continue to be enhanced. This may include some new modelling features such as better support for synchronisation of state-machines and support for more UML modelling details. However, usability of the current features is seen as the main objective. This will include,

  • Support for copy, cut and paste of diagram elements so that they can be moved and/or replicated more easily,
  • Support for re-attaching links (e.g. transitions) to different source/target elements,
  • Facilities for refactoring/renaming elements,
  • Support for the event extension mechanism of Event-B,
  • Integration of Context Diagram model elements on Class diagrams,
  • Improve facilities for navigating between state-machines and visualising multiple state-machines.

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=D32_Model_Animation&oldid=2661’