Difference between pages "Code Generation Activity" and "D32 Model Animation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Andy
 
imported>Leuschel
 
Line 1: Line 1:
Tasking Event-B is the extension of Event-B for defining concurrent systems sharing data, for details see the [[Tasking Event-B Overview]] page. For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk, or Chris Lovell mailto:cjl3@ecs.soton.ac.uk
+
= Model Animation =  
=== Code Generation Feature - Version 0.2.2 For Rodin 2.4===
 
Interim Release
 
  
local update site soon available from:
+
== Overview ==
[https://sourceforge.net/projects/codegenerationd/files/?]
+
=== Siemens Application===
 
+
The most important additions of the last 12 months are:
=== Code Generation Feature - Version 0.2.1 For Rodin 2.3===
+
* 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>Leuschel et al. FM'2009</ref> only contained the initial San Juan case study, which was used to evaluate the potential of our approach.
Contains Bug Fixes for previous release. 14-12-2011
+
* 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.
=== Code Generation Feature - Version 0.2.0 For Rodin 2.3===
+
* 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.
We have release a new version of the code generator on 30-11-2011, and updated documentation.
 
===== Changes to the Tooling and Approach =====
 
The main changes are:
 
* The code generators have been completely re-written. The translators are now implemented in Java, i.e. there is no longer a dependence on the Epsilon tool set. This was undertaken for code maintenance reasons.
 
* Tasking Event-B is now integrated with the Event-B explorer.
 
* The Rose Editor is used for editing the Tasking Event-B, and
 
* a text-based editor is provided, using the Rose extension, for editing the TaskBody. This feature has been added to address some of the usability concerns. It also overcomes the 'problem' experienced with duplicate event names in a development, since the parser-builder that has been implemented automatically selects the correct event.
 
* The EMF tree editor in Rose is only used minimally; we plan enhancements to further reduce its use.
 
* Composed machines are used to store event 'synchronizations'; these are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events.
 
* The code generation approach is now extensible; new target language constructs can be added using the Eclipse extension mechanism.
 
* The translation of target's mathematical language is now specified in the theory plug-in. This improves clarity since the the translation from source to target is achieved by specifying pattern matching rules. Extensibility is also improved; the theory plug-in is used to specify new data-types, and how they are implemented.
 
* Translated code is deposited in a directory in the appropriate files. An Ada project file is generated for use with AdaCore's GPS workbench. Eventually this could be enabled/disabled in a preferences dialog box.
 
* The Tasking Event-B to Event-B translator is now properly integrated. Control variable updates to the Event-B model are made in a similar way to the equivalent updates in the state-machine plug-in. The additional elements are added to the Event-B model and marked as 'generated'. This prevents users from manually modifying them, and allows them to be removed through a menu choice.
 
 
 
===== Changes to the Documentation =====
 
The following Pages have been updated:
 
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Overview Tasking Event-B Overview]
 
* [http://wiki.event-b.org/index.php/Tasking_Event-B_Tutorial Tutorial]
 
 
 
===== Downloads =====
 
* The Code Generation feature is available by accessing the main Rodin Update Site. In Eclispe click on Help/Install new Software. Find the Rodin update site from the list. In Utilities add Code Generation.
 
The approach makes use of the following:
 
*Model Decomposition: Download from the main Rodin Update Site, in the Decomposition section.
 
*Shared Event Composition: Download from the main Rodin Update Site, in the Decomposition section.
 
*Theory Plug-in: Download from the main Rodin Update Site, in the Modelling Extensions section.
 
  
 +
The validation also lead to the discovery of errors in the English version of the Atelier B reference manual.
 
   
 
   
* Tutorial, and example, projects are available from the Examples directory: [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/v0.2.2/ SVN].
+
Also, since  <ref>Leuschel et al. FM'2009</ref>, ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).
* Test projects are also available from the Examples directory [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/v0.2.1/CG_v0.2.0_Tests SVN].
 
* Sources at: [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration SVN]
 
* Example Theories at: [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/TheoriesForCG SVN]
 
 
 
 
 
TODO
 
* Add addressed variables (for direct read/write access to memory)
 
* Flattening of composed machines/implementation machines.
 
* Interrupts
 
 
 
=== Sensing and Actuating for Tasking Event-B ===
 
Version 0.1.5. Sensing and actuating events, and an Environ Machine have been added to allow simulation of the environment and implementation using memory mapped IO.
 
 
 
* The new v0.1.5 feature is available from the Rodin Update Site, it resides in the Utilities Category.
 
 
 
* As in previous releases, the code generation plug-in relies on the Epsilon tool suite. Add the following Epsilon interim update site to the list of available update sites in the Eclipse menu ''help/install new software'': http://download.eclipse.org/modeling/gmt/epsilon/interim/
 
 
 
* Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
 
 
 
A new [http://wiki.event-b.org/index.php?title=Tasking_Event-B_Tutorial Code Generation Tutorial] has been produced, that makes use of these new features. There is an explanation of the heating controller, upon which it is based, [http://wiki.event-b.org/index.php/Development_of_a_Heating_Controller_System here].
 
 
 
The example/tutorial projects, and also and a Bundled Windows 7 version, are available in the [http://deploy-eprints.ecs.soton.ac.uk/304/ Deploy E-Prints archive] or [https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd/Examples/HeatingController_Tutorial_v0.1.4/ Examples SVN site].
 
 
 
=== The Code Generation Demonstrator for Rodin 2.1.x ===
 
 
 
Released 24 January 2011.
 
 
 
The Rodin 2.1.x compatible code generation demonstrator plug-ins have been released into the Rodin Sourceforge repository at:
 
 
 
  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp/trunk/CodeGeneration
 
 
 
The update-site is available through the Rodin update site in the ''Utilities'' category.
 
 
 
The code generation tutorial examples are available for download at:
 
 
 
  https://sourceforge.net/projects/codegenerationd/files/DemoFiles/
 
 
 
The code generation plug-in relies on the Epsilon tool suite. Install Epsilon manually, since the automatic install utility does not seem to work for this feature. We currently use the Epsilon interim update site available at:
 
 
 
  http://download.eclipse.org/modeling/gmt/epsilon/interim/
 
 
 
Select 'the Epsilon Core (Incubation)' component, this is the only component that is required for Tasking Event-B.
 
 
 
== Code Generation Status ==
 
=== Latest Developments ===
 
* Demonstrator plug-in feature version 0.1.0
 
** for Rodin 2.1.x version is available.
 
 
 
* The Code Generation feature consists of,
 
** a tasking Development Generator.
 
** a tasking Development Editor (Based on an EMF Tree Editor).
 
** a translator, from Tasking Development to Common Language Model (IL1).
 
** a translator, from the Tasking Development to Event-B model of the implementation.
 
** a pretty-printer for the Tasking Development.
 
** a pretty-printer for Common Language Model, which generates Ada Source Code.
 
 
 
* A tutorial is available [[Code Generation Tutorial]]
 
** Step 1 - Create the tasking development.
 
** Step 2 - Add annotations.
 
** Step 3 - Invoke translators.
 
  
=== Ongoing Work ===
+
More details:
 +
* <ref>Leuschel et al. FAC, special issue of FM'2009</ref>
 +
* <ref>Leuschel et al. Draft of Validation Report</ref>
  
* Full Rodin Integration
+
=== Multi-level Animation ===
* Sensed Variables
+
(ABZ'2010 & SCP journal paper)
* Branching in Shared Machines
 
  
=== Future Work ===
+
=== Improvements to the ProB Constraint solver and empirical evaluation ===
* Support for Interrupts.
+
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.
* Richer DataTypes.
+
 
* Accommodation of duplicate event names in tasking developments.
+
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. For some others, 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.
  
== Metamodels ==
+
=== Constraint-Based Deadlock Checking ===
* In the plug-in we define several meta-models:
+
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
** CompositeControl: for the control flow (algorithmic) constructs such as branch, loop and sequence etc. These constructs may be used in the specification of either  sequential or concurrent systems.
+
chosen.
** Tasking Meta-model: defines the tasking model where we attach tasking specific details, such as task priority, task type. The tasking structures provide the ability to define single tasking or multi-tasking (concurrent) systems. We make use of the composite control plug-in to specify the flow of control.  
 
** Common Language (IL1) Meta-model: defines an abstraction of common programming language constructs for use in translations to implementations.
 
  
== Translation Rules ==
+
Idea: solve constraints of axioms, invariant together with a constraint specifying a deadlock.
* Tasking to IL1/Event-B translation rules [[http://wiki.event-b.org/images/Translation.pdf]]
 
  
== Release History ==
+
Required Developments:
=== The Code Generation Demonstrator for Rodin 1.3.x ===
+
* 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;
 +
relevance of Counter=10 due to flow
  
First release: 30 November 2010.
+
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.
  
available from:
+
=== BMotionStudio for Industrial Models ===
  
https://sourceforge.net/projects/codegenerationd/files/
+
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.
  
The zip file contains a windows XP bundle, and a Windows V7 bundle. Alternatively, if you wish to build using an update-site, this is also included in the zip file, along with some notes on installation. However, note that the demonstrator tool is only compatible with Rodin 1.3.
+
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:
  
A simple shared buffer example is provided. This will form the basis of a tutorial (which is work in progress). The WindowsBundles directory contains a Rodin 1.3.1 platform with the Code Generation plug-ins, together with a patch plug-in. The patch plug-in is required to correct an inconsistency in the org.eventb.emf.persistence plug-in. For the bundles, simply extract the appropriate zip file into a directory and run the rodin.exe. The plug-ins are pre-installed - the only configuration necessary may be to switch workspace to ''<installPath>\rodin1.3bWin7\workspace''. When using the update-site the example projects, and the project forming the basis of a simple tutorial, are provided in the accompanying zip file. These should be imported manually.
+
* 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.
 +
* 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.
 +
* 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.
  
Mac users - no bundled version available at present, but use the update site in the 'advanced' folder.
+
=== Various other improvements ===
  
'''A step-by-step [[Code Generation Tutorial]] is available'''
+
mainly inspired by Siemens and Bosch Applications
  
==== About the Initial Release ====
+
Improved AVL algorithms, more operators
The Code Generation (CG) Feature in the initial release is a demonstration tool; a proof of concept, rather than a prototype. The tool has no static checker and, therefore, there will be a heavy reliance on docs and dialogue to facilitate exploration of the tools and concepts.
 
  
==== Source Code ====
+
record support, treatment of infinite sets,
  
The sources are available from,
+
== Motivations ==
  
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
+
The above works were motivated mainly to support the following three industrial deployments:
 +
* Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
 +
* Bosch: provide animation and constraint-based deadlock detection for the Adaptive Cruise Control
 +
* SAP: provide a way to generate test cases using constraint-based animation
  
Note - I used Eclipse 3.5 Galileo, and you will need to install (or have sources from) Epsilon's interim update site. There is also dependency on Camille v2.0.0
+
== Available Documentation ==
  
 +
=== References ===
 +
<references/>
  
 +
== Planning ==
  
[[Category:Work in progress]]
+
* Finish Validation Report
 +
* Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
 +
* Support mathematical extensions in ProB

Revision as of 09:44, 29 November 2010

Model Animation

Overview

Siemens Application

The most important additions of the last 12 months are:

  • 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 [1] 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.

Also, since [2], ProB itself has been further improved inspired by the application, resulting in new optimisations in the kernel (see below).

More details:

Multi-level Animation

(ABZ'2010 & SCP journal paper)

Improvements to the ProB Constraint solver and empirical evaluation

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. For some others, 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

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.

Required Developments:

  • 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; relevance of Counter=10 due to flow

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.

BMotionStudio for Industrial Models

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:

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

mainly inspired by Siemens and Bosch Applications

Improved AVL algorithms, more operators

record support, treatment of infinite sets,

Motivations

The above works were motivated mainly to support the following three industrial deployments:

  • Siemens: enable Siemens to use ProB in their SIL4 development chain, replacing Atelier B for data validation.
  • Bosch: provide animation and constraint-based deadlock detection for the Adaptive Cruise Control
  • SAP: provide a way to generate test cases using constraint-based animation

Available Documentation

References

  1. Leuschel et al. FM'2009
  2. Leuschel et al. FM'2009
  3. Leuschel et al. FAC, special issue of FM'2009
  4. Leuschel et al. Draft of Validation Report

Planning

  • Finish Validation Report
  • Write up Constraint-Based Deadlock Checking and integrate fully into Rodin Platform
  • Support mathematical extensions in ProB