Difference between pages "D23 ProB" and "D32 Code generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Leuschel
 
imported>Tommy
m
 
Line 1: Line 1:
= Overview =
+
= General Overview =
This part of the deliverable describes improvement of the ProB animation and model checking plugin.
 
  
The improvements and development of ProB were mainly carried out by University of Düsseldorf, with some support by the University of Southampton.
+
The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as ''Shared Event Decomposition'' <ref name = "SharedEventDecomp">[[Event_Model_Decomposition]]</ref>, and the ''EMF Framework for Event-B'' <ref name = "EMF4EventB">[[EMF_framework_for_Event-B]]</ref>. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in <ref name = "flow">[[Flows]]</ref> and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their ''Epsilon'' <ref name = "Epsilon"> http://www.eclipse.org/gmt/epsilon/</ref> model-to-model transformation technology.
Furthermore, the work was driven by requirements of Siemens and SAP; some tool development was also undertaken by SAP.
 
 
 
New features:
 
* Multi-level animation and validation
 
* B-Motion Studio
 
* Disprover Support
 
* first steps towards test-case generation
 
 
 
Improvements:
 
* Scalability improvements driven by Siemens and SAP applications
 
* Using proof information to improve model checking
 
 
 
Other works:
 
* First steps towards validation of ProB for usage by Siemens in SIL-4 chain
 
* Evaluation against SAT/SMT/BDD-based approaches
 
  
 
= Motivations =
 
= Motivations =
This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.
 
  
 +
The decision was taken in 2009 to include code generation as a project goal <ref name = "d23"> [[D23_Code_Generation]]</ref>. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.
  
=== Multi-level Animation and Validation ===
+
= Choices / Decisions =
 +
== Strategic Overview ==
 +
During the last year we have focussed on supporting the generation of code for typical real-time embedded control software. To this end we have evolved a multi-tasking approach which is conceptually similar to that of the Ada tasking model. Tasks are modelled by an extension to Event-B, called ''Tasking Machines''. Tasking Machines are an extension of the existing Event-B Machine component. In implementations such as Ada, tasks share the resources and have mutually exclusive access to shared state through the use of a protection mechanism. An Event-B machine can also be viewed as an abstraction of a shared resource, and the  mechanism protecting it. We use existing Event-B machines with minimal extensions (called Shared Machines) to represent shared resources.
  
Thus far ProB only alllowed single-level animation, i.e., the animator would animate a single refinement level in isolation.
+
For real-time control, periodic and one-shot activation is currently supported; and it is planned to support triggered tasks in the near future. Tasks have priorities to ensure appropriate responsiveness of the control software. For the DEPLOY project, it was regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects has been accommodated.  
This meant that ProB was not able to detect a large class of potential errors in the model:
 
* a broken gluing invariant
 
* an invalid witness
 
* violation of guard strengthening
 
* violation of variant decrease (resp. decrease or stability) for convergent (resp. anticipated) events
 
  
The new validation algorithm now can animate a range of refinements together. The user can decide which levels are to be animated together.
+
Our main goal this year has been to devise an approach for, and provide tool support for, code generation (initially to Ada). In accord with the resources available during the year it was decided to limit the provision of tool support to that of a demonstrator tool. The tool is a proof-of-concept only, and lacks the productivity enhancements expected in a more mature tool. Nevertheless much insight has been gained in undertaking this work; it lays a foundation for future research, and will be useful since it will allow interested parties to explore the approach.
As such, all of the above errors can now be detected by ProB.
 
User experience is also improved, as he or she can inspect also the abstract variables.
 
The new algorithm has been sucessfully applied to various case studies, and thus far up to 14 levels have been animated concurrently without problem.
 
  
 +
== The Tasking Extension for Event-B ==
  
=== B-Motion Studio ===
+
The following text can be read in conjunction with the slides<ref name = "Zurich2010Slides">http://deploy-eprints.ecs.soton.ac.uk/260/2/CGSlidesAndy%2520Edmunds%2520-%2520Code%2520Generation%2520Slides.pdf</ref> from the Deploy Plenary Meeting - Zurich 2010.
  
It is often very important to be able to show a formal model to a domain expert or manager, not versed in formal methods.
+
Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a Tasking Development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see [[#Implementing Events]]) to facilitate code generation.
For example, only a domain expert will be able to detect certain mistakes in the formal model.
 
To enable to easily and quickly build graphical visualisations of Rodin models, we have developed B-Motion Studio.
 
B-Motion Studio comes with a graphical editor to arrange graphical components and link them with the formal model.
 
No new programming language has to be learned: the linking is described in B itself.
 
To run a graphical visualisation, the ProB animator is used.
 
  
=== Test-Case Generation ===
+
A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps associated contexts). In our approach we make use of the Event-B EMF extension mechanism which allows addition of new constructs to a model. The tasking extension consists of the constructs in the following table.
  
During deployment in the SAP workpackage it became clear that test-case generation from the Event-B models
+
<center>
is required for success.
+
{| border="1"
In this task, we have developed a first algorithm for test-case generation, which ensures complete transition coverage of a high-level model, and translates the test-cases into traces of a refined model, so that the tests can be run on the "real" system.
+
|Construct
Optimisations, to reduce the length and number of test cases, as well as to minimise race conditions, have been implemented.
+
|Options
 +
|-
 +
|Machine Type
 +
|DeclaredTask, AutoTask, SharedMachine
 +
|-
 +
|Control
 +
|Sequence, Loop, Branch, EventSynch
 +
|-
 +
|Task Type
 +
|Periodic(n), Triggered, Repeating, OneShot
 +
|-
 +
|Priority
 +
| -
 +
|-
 +
|Event Type
 +
|Branch, Loop, ProcedureDef, ProcedureSynch
 +
|-
 +
|Parameter Type
 +
|ActualIn, ActualOut, FormalIn, FormalOut
 +
|}
 +
</center>
  
=== Scalability and Validation ===
+
The machines in the Tasking Development are extended with the constructs shown in the table, and may be viewed as keywords in a textual representation of the language. With extensions added, a Tasking Development can be translated to a common language model for mapping to implementation source code. There is also a translator that constructs new machines/contexts modelling the implementation, and these should refine/extend the existing elements of the Event-B project.
We tackled  a  case study in WP2, which centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). I
 
  
The motivation then was to try and use ProB for this task.
+
== Tasking Machines ==
This required a considerable amount of work on improving the scalability of the ProB kernel, to be able to deal with large sets and relations.
+
The following constructs relate only to Tasking Machines, and provide implementation details. Timing of periodic tasks is not modelled formally. Tasking Machines are related to the concept of an Ada task. These can be implemented in Ada using tasks, in C using the pthread library C, or in Java using threads.
The ProB parser and type checker also had to be re-developed to be able to deal with large industrial specifications.
 
  
The case study was a succcess:ProB was able to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month.  
+
* Tasking Machines may be characterised by the following types:
 +
** AutoTasks - Singleton Tasks.
 +
** Declared tasks - (Not currently used) A task template relating to an Ada ''tasktype'' declaration.
 +
** TaskType - Defines the scheduling, cycle and lifetime of a task. i.e. one-shot periodic or triggered.
 +
** Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.
  
This leads to the next task: the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens
+
== Shared Machines ==
 +
A Shared Machine corresponds to the concept of a protected resource, such as a monitor. They may be implemented in Ada as a Protected Object, in C using mutex locking, or in Java as a monitor.
  
=== Proof Directed Model Checking ===
+
* Applied to the Shared Machine we have:
 +
** A SharedMachine ''keyword'' that identifies a machine as a Shared Machine.
  
Jens: can you insert something?
+
== Tasks and Events ==
 +
=== Control Constructs ===
 +
Each Tasking Machine has a ''task body'' which contains the flow control, or algorithmic, constructs.
  
 +
* We have the following constructs available in the Tasking Machine body:
 +
** Sequence - for imposing an order on events.
 +
** Branch - choice between a number of mutually exclusive events.
 +
** Loop - event repetition while it's guard remains true.
 +
** Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine. Synchronization corresponds to an subroutine call with atomic (with respect to an external viewer) updates. The updates in the protected resource are implemented by a procedure call to a protected object, and tasks do not share state.  The synchronization construct also provides the means to specify parameter passing, both in and out of the task.
 +
** Event wrappers - The event synchronization construct is contained in an event wrapper. The wrapper may also contain a single event (we re-use the synchronization construct, but do not use it for synchronizing). The event may belong to the Tasking Machine, or to a Shared Machine that is visible to the task. Single events in a wrapper correspond to a subroutine call in an implementation.
  
=== SAT/SMT/Kodkod ===
+
=== Implementing Events ===
 +
An event's role in the implementation is identified using the following extensions which are added to the event. Events used in task bodies are 'references' that make use of existing event definitions from the abstract development. The events are extended. to assist with translation, with a keyword indicating their role in the implementation.
  
In this subtask we investigate alternate approaches for validating high-level B models using techniques and tools based on BDDs, SAT-solving and SMT-solving.
+
* Event implementation.
The overall motivation is to improve the scalability of the animator and model checker.
+
** Branch - In essence a task's event is split in the implementation; guards are mapped to branch conditions and actions are mapped to the branch body. If the branch refers to a Shared Machine event (procedureDef) then this is mapped to a simple procedure call.
 +
** Loop - The task's event guard maps to the loop condition and actions to to loop body. If the loop refers to a Shared Machine event then it is mapped to a simple procedure call.  
 +
** ProcedureSych - This usually indicates to the translator that the event maps to a subroutine, but an event in a task may not require a subroutine implementation if its role is simply to provide parameters for a procedure call.
 +
** ProcedureDef - Identifies an event that maps to a (potentially blocking) subroutine definition. Event guards are implemented as a conditional wait; in Ada this is an entry barrier, and in C may use a pthread condition variable .
  
=== Disprover ===
+
In an implementation, when an subroutine is defined, its formal parameters are replaced by actual parameter values at run-time. To assist the code generator we extend the Event-B parameters. We identify formal and actual parameters in the implementation, and add the following keywords to the event parameters, as follows:
  
In order to help the user, we wanted to make it possible to apply ProB to individual proof obligations.
+
* Event parameter types
In some cases, this enables proving a sequent by exhaustive case analysis.
+
** FormalIn or FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
Also, if ProB finds a counter example, the user gets important feedback: the proof obligation cannot be discharged, along with a reason why.
+
** ActualIn or ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.
  
= Choices / Decisions =
+
== Other Technical Issues ==
This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.
+
=== Translation Technology ===
 +
In order to provide a structured extensible code generation tool it was decided to use a multi-stage translation approach. The Event-B EMF model provided by the Event-B EMF Framework is extended to accommodate the tasking constructs as described above. The Tasking model is then translated to an intermediate model, the Common Language Model. The Common Language Meta-model is an abstraction of some useful generic programming constructs such as sequence, loop, branch and subroutine call/definition and so on. The translation of the Common Language Model to programme source code is then a relatively small step. The main translation activity takes place in the step between Tasking and Common Language models.
  
= Available Documentation =
+
The decision was made to use Epsilon <ref name = "Epsilon"> </ref> to facilitate model to model translation for this stage. It was felt that an extensible, easily maintainable solution was required for this. Various model-to-model technologies (Java code, ATL, Epsilon) were appraised and it was judged that the Epsilon tool best matched our requirements. It proved to be a good choice initially for the specification of translations, especially in simpler areas of the project where the correspondence between models were simple. However the lack of debugging facilities, and productivity enhancements that are found in more mature tools, somewhat hindered rapid development as the project increased in complexity.
  
== User Manual ==
+
=== Implementation - Source Code ===
 +
Early in the current phase of work we identified the possibility of translating the Common Language Model to EMF models of programming languages such as Ada and C, in addition to producing textual source. While the EMF route still remains an option, it was decided that we would produce a PrettyPrinter for the Ada code. This allows a user to cut and paste the Ada source code from the PrettyPrinter window to an Ada editor, and was the optimal route to code for this phase of the code generation activity in DEPLOY.
  
[http://asap0.cs.uni-duesseldorf.de/trac/prob/wiki/ ProB User Manual]
+
=== Editing the Tasking Model ===
 +
The editor for the Tasking Development is based on a EMF tree-editor. The tree editor provides a facility for adding the extensions to Event-B constructs. The readability of the editor is enhanced by a PrettyPrinter, which provides a textual version of the Tasking Development, which is easier to read. It is envisaged that the textual notation will be fully integrated as a Camille extension when the facility/resources become available.
  
== Published Papers ==
+
== The Tool Deliverable ==
 +
The demonstrator tool was released on 30 November 2010, and is available as an update site, or bundled Rodin package from:
 +
https://sourceforge.net/projects/codegenerationd/files
  
Below is a list of published papers, along with an abstract.
+
Sources are available from:
 +
https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd
  
=== Improved Kernel to deal with large sets and relations ===
+
The tool is based on a build of Rodin 1.3.1 (not Rodin 2.0.0 due to dependency conflicts).
In this part we describe the successful application of the ProB validation tool on an industrial case study. The case study centres on the San Juan metro system installed by Siemens. The control software was developed and formally proven with B. However, the development contains certain assumptions about the actual rail network topology which have to be validated separately in order to ensure safe operation. For this task, Siemens has developed custom proof rules for AtelierB. AtelierB, however, was unable to deal with about 80 properties of the deployment (running out of memory). These properties thus had to be validated by hand at great expense (and they need to be revalidated whenever the rail network infrastructure changes). In this paper we show how we were able to use ProB to validate all of the about 300 properties of the San Juan deployment, detecting exactly the same faults automatically in around 17 minutes that were manually uncovered in about one man-month. This achievement required the extension of the ProB kernel for large sets as well as an improved constraint propagation phase. We also outline some of the effort and features that were required in moving from a tool capable of dealing with medium-sized examples towards a tool able to deal with actual industrial specifications. Notably, a new parser and type checker had to be developed. We also touch upon the issue of validating ProB, so that it can be integrated into the SIL4 development chain at Siemens
 
  
 +
* The Code Generation tool 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.
  
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=248 Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge. Automated Property Verification for Large Scale B Models, FM'2009.]
+
= Available Documentation =
 
+
== Technical Background ==
=== Multi-Level Animation and Validation ===
 
We provide a detailed description of refinement in Event-B, both as a contribution in itself and as a foundation for the approach to simultaneous animation of multiple levels of refinement that we propose.
 
We present an algorithm for simultaneous multi-level animation of refinement, and show how it can be used to detect a variety of errors that occur frequently when using refinement.
 
The algorithm has been implemented in ProB and we applied it to several case studies, showing that multi-level animation is tractable also on larger models.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=256 Stefan Hallerstede, Michael Leuschel, Daniel Plagge. Refinement-Animation for Event-B --- Towards a Method of Validation. ABZ'2010 ]
 
 
 
See also [http://www.springerlink.com/content/282p2316x7165588/ Stefan Hallerstede, Michael Leuschel. How to Explain Mistakes. TFM'09.]
 
  
=== Test-Case Generation ===
+
Much insight was gained during the work on code generation reported in the thesis ''Providing Concurrent Implementations for Event-B Developments'' <ref name="aeThesis">http://eprints.ecs.soton.ac.uk/20826/</ref>
Choreography models describe the communication protocols between services. Testing of service choreographies is an important task for the quality assurance of service-based systems as used e.g. in the context of service-oriented architectures (SOA). The formal modeling of service choreographies enables a model-based integration testing (MBIT) approach. We present MBIT methods for our service choreography modeling approach called Message Choreography Models (MCM). For the model-based testing of service choreographies, MCMs are translated into Event-B models and used as input for our test generator which uses the model checker ProB.
 
  
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=252 Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. Applying Model Checking to Generate Model-based Integration Tests from Choreography Models. TESTCOM/FATES 2009.]
+
Tooling issues were reported in a paper ''Tool Support for Event-B Code Generation''
 +
<ref name = "toolSupport">http://eprints.ecs.soton.ac.uk/20824/</ref>
 +
which was presented at ''Workshop on Tool Building in Formal Methods'',
 +
http://abzconference.org/
  
 +
There are technical notes available <ref name = "techNotes">http://wiki.event-b.org/images/Translation.pdf</ref>, that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.
  
=== Proof-Directed Model Checking ===
+
== For Users ==
With the aid of the ProB Plugin, the Rodin Platform provides an integrated environment for editing, proving, animating and model checking Event-B models. This is of considerable benefit to the modeler, as it allows him to switch between the various tools to validate, debug and improve his or her models. The crucial idea of this paper is that the integrated platform also provides benefits to the tool developer, i.e., it allows easy access to information from other tools. Indeed, there has been considerable interest in combining model checking, proving and testing. In previous work we have already shown how a model checker can be used to complement the Event-B proving environment, by acting as a disprover. In this paper we show how the prover can help improve the efficiency of the animator and model checker.
 
  
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=253 Jens Bendisposto, Michael Leuschel. Proof Assisted Model Checking for B. ICFEM 2009.]
+
There is an overview at [[Tasking Event-B Overview for D32 ]]
  
=== Debugging Tricky Proof Obligations with the ProB Disprover ===
+
There is a wiki page at [[Code_Generation_Activity]]
While a large number of proof obligations can be discharged automatically by tools such as the RODIN platform, a considerable number still have to be proven interactively.  In this paper, we we describe a disprover plugin for RODIN that utilizes ProB to automatically find counterexamples for a given problematic proof obligation.  In case the disprover finds a counterexample, the user can directly investigate the source of teh problem, as pinpointed by the counterexample.  We also discuss under which circumstances our plug-in can be used as a prover, i.e., when the absence of a counterexample
 
actually is a proof of the proof obligation.
 
  
[http://www.stups.uni-duesseldorf.de/publications_detail.php?id=219 Olivier Ligot, Jens Bendisposto, Michael Leuschel. Debugging Event-B Models using the ProB Disprover Plug-in.  AFADL 2007.]
+
There is a tutorial at [[Code_Generation_Tutorial]]
 
 
=== Inspection of Alternate Approaches ===
 
 
 
ProB is a model checker for high-level B and Event-B models based on constraint-solving. In this paper we investigate alternate approaches for validating high-level B models using techniques and tools based on using BDDs, SAT-solving and SMT-solving. In particular, we examine whether ProB can be complemented or even supplanted by using one of the tools BDDBDDB, Kodkod or SAL.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=249 Daniel Plagge, Michael Leuschel, Ilya Lopatkin, Alexander Romanovsk. SAL, Kodkod, and BDDs for Validation of B Models. Lessons and Outlook. AFM'09.]
 
 
 
=== Validation of ProB ===
 
 
 
Symmetry reduction is a model checking technique that can help alleviate the problem of state space explosion, by preventing redundant state space exploration. In previous work, we have developed three effective approaches to symmetry reduction for B that have been implemented into the ProB model checker, and we have proved the soundness of our state symmetries. However, it is also important to show our techniques are sound with respect to standard model checking, at the algorithmic level. In this paper, we present a retrospective B development that addresses this issue through a series of B refinements. This work also demonstrates the valuable insights into a system that can be gained through formal modelling.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=257 Edd Turner, Michael Butler, Michael Leuschel. A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ABZ'2010.]
 
 
 
 
 
=== B-Motion Studio ===
 
 
 
B-Motion Studio provides a way to quickly generate domain specific visualisations for a formal model, enabling domain experts and managers to understand and validate the model. We also believe that our tool will be of use when teaching formal methods, both during lectures as a way to motivate students to write their own formal models.
 
 
 
[http://www.stups.uni-duesseldorf.de/~leuschel/publication_detail.php?id=258 Lukas Ladenberger, Jens Bendisposto, Michael Leuschel. Visualising Event-B models with B-Motion Studio. FMICS'2009.]
 
  
 
= Planning =
 
= Planning =
This paragraph shall give a timeline and current status (as of 29 Jan 2010).
 
 
=== Model-based Testing ===
 
 
* Directed Model Checking to achieve coverage (Deploy extension; Flow Graphs)
 
* Integrate Algorithm into Rodin
 
* Make Algorithm more generic
 
* Top-down multi-level animation
 
* Move from prototype to real product
 
 
=== B-Motion Studio ===
 
 
* Experiment with existing Flash animation and B model of ClearSy
 
* Improve usability, more widgets
 
 
=== Validation of ProB ===
 
 
* Test coverage analysis for Prolog code
 
* Validation Document to be delivered to Siemens
 
 
=== Scalability ===
 
  
* More experiments with SAT, SMT, BDD techniques
+
During 2011 we plan to develop the code generation tools further, taking on board any feedback from interested parties. The tool support should advance to the prototype stage, with improvements in the tool's usability in terms of features and user experience.
  
* Integration of Kodkod into ProB for solving complicated predicates over first order relations and simple sets
+
== References ==
  
* Adaption of ProB for the upcoming mathematical extensions. Indeed, for the moment the Rodin user is often required to model basic datatypes (records, sequences,...) or operators (transitive closure) herself. This is a big challenge to the animator, which does not know that the constants and variables of the machine (e.g., injective functions) are "simply" meant to model quite basic datatypes. With the introduction of mathematical extensions for records, transitive closure, ... this hurdle will be overcome.
+
<references/>
  
=== Usability ===
+
[[Category:D32 Deliverable]]
* Feedback errors found by ProB into the PO view (as red icons)
 
* Improve Disprover, detect when it is a decision procedure
 
* Further improvments to GUI: 2-D Viewer, better multi-level animation view
 

Revision as of 11:17, 27 January 2011

General Overview

The code generation activity has been undertaken at the University of Southampton. This has been a new line of work for DEPLOY that was not identified in the original Description of Work for the project. The development of the approach, and the tools to support, it involved a number of team members at Southampton; and also at other institutions. This work draws on our recent experience with technologies such as Shared Event Decomposition [1], and the EMF Framework for Event-B [2]. There was collaboration at an early stage with Newcastle University, where we explored the commonalities between their flow plug-in [3] and the flow control structures used in our approach. Collaboration with the University of York was also established since we chose to use their Epsilon [4] model-to-model transformation technology.

Motivations

The decision was taken in 2009 to include code generation as a project goal [5]. It had been recognised that support for generation of code from refined Event-B models would be an important factor in ensuring eventual deployment of the DEPLOY approach within their organisations. This was especially true for Bosch and Space Systems Finland (SSF). After receiving more detailed requirements from Bosch and SSF, it became clear we should focus our efforts on supporting the generation of code for typical real-time embedded control software.

Choices / Decisions

Strategic Overview

During the last year we have focussed on supporting the generation of code for typical real-time embedded control software. To this end we have evolved a multi-tasking approach which is conceptually similar to that of the Ada tasking model. Tasks are modelled by an extension to Event-B, called Tasking Machines. Tasking Machines are an extension of the existing Event-B Machine component. In implementations such as Ada, tasks share the resources and have mutually exclusive access to shared state through the use of a protection mechanism. An Event-B machine can also be viewed as an abstraction of a shared resource, and the mechanism protecting it. We use existing Event-B machines with minimal extensions (called Shared Machines) to represent shared resources.

For real-time control, periodic and one-shot activation is currently supported; and it is planned to support triggered tasks in the near future. Tasks have priorities to ensure appropriate responsiveness of the control software. For the DEPLOY project, it was regarded as sufficient to support construction of programs with a fixed number of tasks and a fixed number of shared variables – no dynamic creation of processes or objects has been accommodated.

Our main goal this year has been to devise an approach for, and provide tool support for, code generation (initially to Ada). In accord with the resources available during the year it was decided to limit the provision of tool support to that of a demonstrator tool. The tool is a proof-of-concept only, and lacks the productivity enhancements expected in a more mature tool. Nevertheless much insight has been gained in undertaking this work; it lays a foundation for future research, and will be useful since it will allow interested parties to explore the approach.

The Tasking Extension for Event-B

The following text can be read in conjunction with the slides[6] from the Deploy Plenary Meeting - Zurich 2010.

Tasking Event-B can be viewed as an extension of the existing Event-B language. We use the existing approaches of refinement and decomposition to structure a development that is suitable for construction of a Tasking Development. At some point during the modelling phase parameters may have to be introduced to facilitate decomposition. This constitutes a natural part of the refinement process as it moves towards decomposition and on to the implementation level. During decomposition parameters form part of the interface that enables event synchronization. We make use of this interface and add information (see #Implementing Events) to facilitate code generation.

A Tasking Development is generated programmatically, at the direction of the user; the Tasking Development consists of a number of machines (and perhaps associated contexts). In our approach we make use of the Event-B EMF extension mechanism which allows addition of new constructs to a model. The tasking extension consists of the constructs in the following table.

Construct Options
Machine Type DeclaredTask, AutoTask, SharedMachine
Control Sequence, Loop, Branch, EventSynch
Task Type Periodic(n), Triggered, Repeating, OneShot
Priority -
Event Type Branch, Loop, ProcedureDef, ProcedureSynch
Parameter Type ActualIn, ActualOut, FormalIn, FormalOut

The machines in the Tasking Development are extended with the constructs shown in the table, and may be viewed as keywords in a textual representation of the language. With extensions added, a Tasking Development can be translated to a common language model for mapping to implementation source code. There is also a translator that constructs new machines/contexts modelling the implementation, and these should refine/extend the existing elements of the Event-B project.

Tasking Machines

The following constructs relate only to Tasking Machines, and provide implementation details. Timing of periodic tasks is not modelled formally. Tasking Machines are related to the concept of an Ada task. These can be implemented in Ada using tasks, in C using the pthread library C, or in Java using threads.

  • Tasking Machines may be characterised by the following types:
    • AutoTasks - Singleton Tasks.
    • Declared tasks - (Not currently used) A task template relating to an Ada tasktype declaration.
    • TaskType - Defines the scheduling, cycle and lifetime of a task. i.e. one-shot periodic or triggered.
    • Priority - An integer value is supplied, the task with the highest value priority takes precedence when being scheduled.

Shared Machines

A Shared Machine corresponds to the concept of a protected resource, such as a monitor. They may be implemented in Ada as a Protected Object, in C using mutex locking, or in Java as a monitor.

  • Applied to the Shared Machine we have:
    • A SharedMachine keyword that identifies a machine as a Shared Machine.

Tasks and Events

Control Constructs

Each Tasking Machine has a task body which contains the flow control, or algorithmic, constructs.

  • We have the following constructs available in the Tasking Machine body:
    • Sequence - for imposing an order on events.
    • Branch - choice between a number of mutually exclusive events.
    • Loop - event repetition while it's guard remains true.
    • Event Synchronisation - synchronization between an event in a Tasking Machine and an event in a Shared Machine. Synchronization corresponds to an subroutine call with atomic (with respect to an external viewer) updates. The updates in the protected resource are implemented by a procedure call to a protected object, and tasks do not share state. The synchronization construct also provides the means to specify parameter passing, both in and out of the task.
    • Event wrappers - The event synchronization construct is contained in an event wrapper. The wrapper may also contain a single event (we re-use the synchronization construct, but do not use it for synchronizing). The event may belong to the Tasking Machine, or to a Shared Machine that is visible to the task. Single events in a wrapper correspond to a subroutine call in an implementation.

Implementing Events

An event's role in the implementation is identified using the following extensions which are added to the event. Events used in task bodies are 'references' that make use of existing event definitions from the abstract development. The events are extended. to assist with translation, with a keyword indicating their role in the implementation.

  • Event implementation.
    • Branch - In essence a task's event is split in the implementation; guards are mapped to branch conditions and actions are mapped to the branch body. If the branch refers to a Shared Machine event (procedureDef) then this is mapped to a simple procedure call.
    • Loop - The task's event guard maps to the loop condition and actions to to loop body. If the loop refers to a Shared Machine event then it is mapped to a simple procedure call.
    • ProcedureSych - This usually indicates to the translator that the event maps to a subroutine, but an event in a task may not require a subroutine implementation if its role is simply to provide parameters for a procedure call.
    • ProcedureDef - Identifies an event that maps to a (potentially blocking) subroutine definition. Event guards are implemented as a conditional wait; in Ada this is an entry barrier, and in C may use a pthread condition variable .

In an implementation, when an subroutine is defined, its formal parameters are replaced by actual parameter values at run-time. To assist the code generator we extend the Event-B parameters. We identify formal and actual parameters in the implementation, and add the following keywords to the event parameters, as follows:

  • Event parameter types
    • FormalIn or FormalOut - event parameters are extended with the ParameterType construct. Extension with formal parameters indicates a mapping to formal parameters in the implementation.
    • ActualIn or ActualOut - Extension with an actual parameter indicates a mapping to an actual parameter in the implementation.

Other Technical Issues

Translation Technology

In order to provide a structured extensible code generation tool it was decided to use a multi-stage translation approach. The Event-B EMF model provided by the Event-B EMF Framework is extended to accommodate the tasking constructs as described above. The Tasking model is then translated to an intermediate model, the Common Language Model. The Common Language Meta-model is an abstraction of some useful generic programming constructs such as sequence, loop, branch and subroutine call/definition and so on. The translation of the Common Language Model to programme source code is then a relatively small step. The main translation activity takes place in the step between Tasking and Common Language models.

The decision was made to use Epsilon [4] to facilitate model to model translation for this stage. It was felt that an extensible, easily maintainable solution was required for this. Various model-to-model technologies (Java code, ATL, Epsilon) were appraised and it was judged that the Epsilon tool best matched our requirements. It proved to be a good choice initially for the specification of translations, especially in simpler areas of the project where the correspondence between models were simple. However the lack of debugging facilities, and productivity enhancements that are found in more mature tools, somewhat hindered rapid development as the project increased in complexity.

Implementation - Source Code

Early in the current phase of work we identified the possibility of translating the Common Language Model to EMF models of programming languages such as Ada and C, in addition to producing textual source. While the EMF route still remains an option, it was decided that we would produce a PrettyPrinter for the Ada code. This allows a user to cut and paste the Ada source code from the PrettyPrinter window to an Ada editor, and was the optimal route to code for this phase of the code generation activity in DEPLOY.

Editing the Tasking Model

The editor for the Tasking Development is based on a EMF tree-editor. The tree editor provides a facility for adding the extensions to Event-B constructs. The readability of the editor is enhanced by a PrettyPrinter, which provides a textual version of the Tasking Development, which is easier to read. It is envisaged that the textual notation will be fully integrated as a Camille extension when the facility/resources become available.

The Tool Deliverable

The demonstrator tool was released on 30 November 2010, and is available as an update site, or bundled Rodin package from:

https://sourceforge.net/projects/codegenerationd/files 

Sources are available from:

https://codegenerationd.svn.sourceforge.net/svnroot/codegenerationd

The tool is based on a build of Rodin 1.3.1 (not Rodin 2.0.0 due to dependency conflicts).

  • The Code Generation tool 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.

Available Documentation

Technical Background

Much insight was gained during the work on code generation reported in the thesis Providing Concurrent Implementations for Event-B Developments [7]

Tooling issues were reported in a paper Tool Support for Event-B Code Generation [8] which was presented at Workshop on Tool Building in Formal Methods, http://abzconference.org/

There are technical notes available [9], that give more precise details of the approach and the mapping between Event-B and the common language meta-model, and its corresponding Event-B model.

For Users

There is an overview at Tasking Event-B Overview for D32

There is a wiki page at Code_Generation_Activity

There is a tutorial at Code_Generation_Tutorial

Planning

During 2011 we plan to develop the code generation tools further, taking on board any feedback from interested parties. The tool support should advance to the prototype stage, with improvements in the tool's usability in terms of features and user experience.

References