Difference between pages "D32 Scalability" and "D45 Code Generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
m
 
imported>Andy
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
−
Regarding scalability of the Rodin platform, the following contributions has been made:
+
The code generation plug-in allows the generation of code for typical real-time embedded control software from refined Event-B models. Such a feature will be an important factor in ensuring eventual deployment of the DEPLOY approach within industrial organisations.
−
 
 
−
* Flows plug-in development. The main purpose of the Flows plug-in <ref name="flow>A. Iliasov. Augmenting Event-B Specifications with Control Flow Information. Nodes 2010. Copenhagen June 3-4 2010, Technical University of Denmark</ref> is to give a modeller a clean and concise view of the control flow aspects of a model without cluttering the model with program counter variables and associated guards and actions. The plug-in is essentially a graphical notation for formulating certain kind of theorems. The new version is to be released in February 2011 and this will include facilities for expressing a wider range of enabledness properties as well as tools for describing event refinement. It is going to address one of the critical shortcomings of the previous version: generation of unwieldy proof obligations (a large disjunction in a goal comprising several hundreds of terms). The tool is developed by Newcastle University with the requirements and suggestions from Bosch and SAP.
 
−
 
 
−
* Group Refinement. Group refinement plug-in is a tool realising an alternative set of Event-B refinement laws in the Rodin platform. It lets a modeller to switch to differing style of event atomicity refinement for the scope of a single refinement steps. For a certain case of atomicity refinement the alternative laws result in a more natural and compact model with fewer and simpler proof obligations. The method and the tool were development by Newcastle University, the pattern of refinement was discovered by the Bosch formal modelling team.
 
−
 
 
−
* Modes. The Mode and Fault Tolerance Views plug-in is a modelling environment for constructing modal and fault tolerance features in a concise manner and formally linking them to Event-B models. As many systems are developed using the notion of operation modes, the tool allows to separate the modal modelling as a refinement chain from the main Event-B models. This makes possible to model explicitly modal behaviour and certain fault tolerance aspects of systems and formally show the consistency between the models and their views. The theory and plug-in were developed by Newcastle University.
 
−
 
 
−
* Emre Yilmaz and Thai Son Hoang (ETH Zurich) has developed a plug-in supporting an extension of Event-B with qualitative reasoning. The extension allows developer to declare an event converges probabilistically (with probability 1). This is in contrast with standard certain termination, where convergent events ''must decrease'' the declared variant. Provided that the variant is bounded above, an event probabilistically converges if it ''might decrease'' the variant. The extension enables Event-B to model systems with ''almost certain termination'' properties, e.g. IEEE 1394 Firewire protocol<ref name="ieee1394">J.-R. Abrial, D. Cansell, D. Mery.  A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol. ''Formal Asp. of Comput.'' 14(3):215-227, 2003</ref> or Rabin's Choice Coordination algorithm <ref name="rabin">M. Rabin. The Choice Coordination Problem. ''Acta Informatica, 17:121-134'', 1982.</ref>.
 
  
 
= Motivations =
 
= Motivations =
 +
DEPLOY industrial partners are interested in the formal development of multi-tasking, embedded control systems. During the project, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems
 +
<ref name="aaa">http://eprints.soton.ac.uk/270824/ "Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010"</ref><ref name="aab">http://eprints.soton.ac.uk/272006/ "Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany"</ref><ref name="aac">http://eprints.soton.ac.uk/272771/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B Models to Code: Sensing, Actuating, and the Environment. At SBMF2011, Sao Paulo, Brazil, 28 - 26 Sep 2011."</ref><ref name="aad">http://eprints.soton.ac.uk/335400/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp. (In Press)"</ref><ref name="aae">http://eprints.soton.ac.uk/336226/ "Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp. (In Press)"</ref>. Initially, we chose to translate to the Ada programming language<ref>J. Barnes. Programming in Ada 2005. International Computer Science Series. Addison Wesley, 2006.</ref>, and use it as a basis for the abstractions used in our approach.<br>
 +
We described our previous code generation feature as a demonstrator tool; chiefly a tool designed as a proof of concept, used by us to validate the approach. In this sense, the tool as it stands now, is the first prototype intended to be used by developers, and thus motivated numerous evolutions and new features such as:
 +
* allowing a more seamless edition of tasking Event-B,
 +
* supporting extensibility,
 +
* supporting other target languages than just Ada,
 +
* supporting programming concepts reification using abstract translators.
  
−
== Flow plug-in ==
+
= Choices / Decisions =
−
The flows tool was applied by Bosch in the development of the cruise control model to verify deadlock-freedom and liveness properties of the model. Being a sizable case-study, this was an important test for the ideas and techniques behind the plug-in. The general conclusion was that a tool of this kind is essential and the current version should be improved in many directions. This experience has uncovered a rather fundamental issues with the size and complexity of the generated proof obligations. These were the largest theorems ever generated in Rodin and the only positive aspect is that this helped to stress-test and debug the proof handling facilities of the Rodin. It was clear that such proof obligations can never be comfortably handled by Rodin tools (although there were some encouraging results in the application of ProB as a disprover for these kind of proofs) and it was decided that the approach to proof generation requires a complete redesign.  
+
Considering the demonstrator as a baseline, we can list the new features as follows:
−
 
+
* Tasking Event-B is now integrated with the Event-B explorer. It uses the extensibility mechanism of Event-B EMF (In the previous version it was a separate model).
−
== Group Refinement ==
+
* Tasking Event-B is now integrated with the Event-B model editors. Tasking Event-B features can now be edited in the same place as the other Event-B features.
−
One of the project industrial partners (Bosch) has identified a recurring refinement pattern that did not fit well the existing laws of refinement. It is a case of atomicity refinement where a previously atomic action (event) is split into a number of steps which combined effect achieves the effect of the abstract atomic event. The Event-B approach is to introduce new variables in a refinement machine and thus have a hidden concrete state on which the steps are defined. There is a further event summarising the effect of the computations accomplished on the hidden state and explicitly relating it to the abstract state. This is the event for which the refinement relation is demonstrated while the events defining the actual computation steps would have no formal link to the abstract event.
+
* We have the ability to translate to Java and C, in addition to Ada source code; and the source code is placed in appropriate files within the project.
−
 
+
* We use theories to define translations of the Event-B mathematical language (Theories for Ada and C are supplied).
−
When the hidden state does not naturally follow as a part of the modelling process this refinement style leads to a contrived model. There appear auxiliary variables and auxiliary events that play no part in the characterisation of the system behaviour but are a codification of the refinement relation to an abstract model. Since such elements accumulate during refinement this has a profound effect on the development of a large model.  
+
* We use the theory plug-in as a mechanism for defining new data types , and the translations to target data types.
−
 
+
* The Tasking Event-B to Event-B translator is fully integrated. The previous tool generated a copy of the project, but this is no longer the case.
−
== Modes ==
+
* The translator is extensible.
−
We have conducted a study of approaches to complex critical systems development, and the requirements documents within DEPLOY, and arrived at the following:
+
* The composed machine component is used to store event 'synchronizations'.
−
* Separation of concerns is a major approach to tackle the complexity of the systems development.
+
* Minimal use is made of the EMF tree editor in Rose.
−
* A large amount of critical systems are developed using a notion of operation modes.
 
−
* All critical systems involve operations with important aspects of human activity (e.g. lives, finance) hence critical. And all of them inevitably have faults due to changing environmental conditions, hardware failures etc. A high percentage of requirements to such systems (up to 40% according to our study within DEPLOY) include fault tolerance as a way to mitigate the consequences of errors.
 
−
* Requirements evolve, including FT.
 
−
 
 
−
There were neither mode nor fault tolerance viewpoints in the state of the art Event-B development. The UML-B approach of statecharts is closely related to modal views. However, the statecharts drive the development by generating Event-B models as opposed to the mode views which facilitate the development by leaving the Event-B modelling activity with the user. On the fault tolerance side, we are aware of the work on ProR framework for tracing requirements, and we plan to integrate the tracing framework with our modelling approach.
 
−
 
 
−
The Mode/FT Views approach is to assist the main Event-B development by an additional set of abstractions and a toolset to facilitate modal and fault tolerance development. We were motivated by the following stimuli:
 
−
* Facilitate the modal and fault tolerance development in Event-B with a comprehensible modelling approach.
 
−
* Stimulate the consideration of fault tolerance at the very first phases of development.
 
−
* Explicitly covering mode and fault tolerance concerns, we wanted to improve the requirement traceability and fulfilment.
 
−
* Help make planning decisions. Focusing the developer attention on specific aspects of development leads to better understanding of the problem and planning of the solution.
 
−
* Provide consistent way of stepwise development of mode and FT aspects by a notion of views refinement.
 
−
 
 
−
== Qualitative Reasoning ==
 
−
Probability is used in many distributed systems for breaking the symmetry between different components/processes, e.g. IEEE 1394 Firewire protocol <ref name="ieee1394"/>, Rabin Choice Coordination algorithm <ref name="rabin"/>. For such systems, termination cannot be guaranteed for certain. Instead, a slightly weaker property is mostly appropriate: ''termination with probability one''. As an example for this type of systems is to consider tossing a coin until it comes up tail. Provided that the coin is fair (in that sense that no face is ignored forever), eventually, the coin will eventually come up head.
 
  
−
Qualitative probabilistic reasoning has been integrated into Event-B <ref name="ifm07">S. Hallerstede, T.S. Hoang. Qualitative Probabilistic Modelling in Event-B. ''iFM 2007: Integrated Formal Methods'', Oxford, U.K. July 2007</ref>: a new kind of actions is added, namely ''probabilistic actions'' with an assumption that the probability for each possible alternative is bounded away from 0 or 1.  Most of the time, probabilistic actions behave the same as (standard) non-deterministic actions (e.g. invariant preservation).  The difference between probabilistic and non-deterministic actions is with convergence proof obligation: probabilistic actions are interpreted ''angelically'', whereas non-deterministic actions are interpreted ''demonically''.  The result is a practical method for handling qualitative reasoning that generates proof obligations in the standard first-order logic of Event-B.
+
These evolutions will be detailed hereafter. Moreover, the code generators have been completely re-written. The translators are now implemented using Java only. In our previous work we attempted to make use of the latest model-to-model transformation technology, available in the Epsilon tool set<ref name="aag">http://www.eclipse.org/epsilon/</ref>, but we decided to revert to Java since Epsilon lacked the debugging and productivity features of the Eclipse Java editor.
  
−
The plug-in allows developers to declare an event to be probabilistic convergent and generate appropriate proof obligations. Since the obligations are in standard first-order logic supported by the Rodin platform, we do not need to make any extension for the provers to handle the new proof obligations.
+
== Tasking Event-B and its edition ==
 +
A text-based task body editor was added, to minimize the amount of editing required with the EMF tree editor. The task body editor is associated with a parser-builder; after the text is entered in the editor the EMF representation is generated (by clicking a button) that is, assuming parsing is successful. If the parser detects an error, information about the parse error is displayed in an adjoining text box. When specifying events in the task body, there is no longer a need to specify two events involved in a synchronization. The code generator automatically finds the corresponding event of a synchronization, based on the event name, and using the composed machine component
 +
<ref name="aah">http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B</ref>. Composed machines are used to store event 'synchronizations', and 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 new feature also overcomes the 'problem' that we previously experienced, with duplicate event names in a development, and event selection, when specifying the task body. The EMF tree editor in Rose is now only used minimally; to add annotations for Tasking, Shared and Environ Machines; typing annotations, and parameter direction information; and sensing/actuating annotations, where necessary. Further work is under way to integrate the code generation feature with the new Rodin editor.
  
−
= Choices/Decisions =
+
== Allowing Extensibility ==
 +
The code generation approach is now extensible; in that, 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. 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.
  
−
== Flow plug-in ==
+
== Targeting new Languages ==
−
The single most important feature of the new version of the Flows plug-in is the introduction of a new form of diagram structuring to prevent the appearance of large proof obligations. The typical source of such proof obligations is demonstrating that an event enables one or more events from a long list of events. Technically, the proof would state that the after-state of the event implies the disjunction of the guards of the next events. To prevent the appearance of such a disjunction a modeller is encouraged to split the list into a set of sub-models. Each sub-model has a pre- and post-conditions and there are proof obligations demonstrating that all the entry events of the sub-model are enabled when the precondition is satisfied and, symmetrically, every exit event satisfies the sub-model post-condition. Externally, a sub-model appears to be a simple atomic event.
+
Making the step from Event-B to code is a process that can be aided through automatic code generation.
 +
The code generation plug-in for Rodin is a new tool for translating Event-B models to concurrent programmes.
 +
However users of such a tool will likely require a diverse range of target languages and target platforms, for which we do not currently provide translations.Some of these languages may be subtly different to existing languages and only have modest differences between the translation rules, for example C and C++, whilst others may have more fundamental differences. As the translation from Event-B to executable code is non-trivial and to reduce the likelihood of error, we want to generalize as much of the translation as possible so that existing translation rules are re-used.
 +
Therefore significant effort is needed to ensure that such a translation tool is extensible to allow additional languages to be included with relative ease. Here we concentrate on translation from a previously defined Common Language Meta-model, the intermediary language IL1, which Event-B translates to directly. IL1 is an EMF metamodel representation of generic properties and functionality found in many programming languages. It has representations for key structural concepts such as variables, subroutines, function calls and parameters. The translation of predicates and expressions contained within the code are handled by a new extension to the theory plug-in, which allows translation rules to be developed for specific target languages within the Rodin environment. The generic nature of the intermediary language is designed to allow for a wide range of different target languages. Developers of new target languages are required to write translators in Java for the conversion from the EMF representation to the code of their target language. To do this we provide a central translation manager, that takes an IL1 model and automatically calls the appropriate translators for each element of the model, whilst also providing the link to the predicate and expression translators provided by the new theory plug-in. The developer registers their translators for the target language through an extension point, where currently there are 15 light-weight translators required for a new target language.
 +
To aid the developer, we provide abstract translators for each required element in the IL1 model that has to be translated. These translators perform the majority of the translation automatically, meaning that in most cases all the developer is required to do is format strings into the appropriate structure for their target language.
 +
For example in an branch statement, the developer would be required to write a method stating how a branch is defined and structured in their language, using a set of previously translated guard conditions and actions.
 +
Importantly, the flexibility remains for the developer to re-write any of the translations if the ones provided are not suitable.
  
−
== Group Refinement ==
+
== Using Abstract Translators ==
−
In this work one obvious source of inspiration is the Classical B method <ref name="bbook">J. R. Abrial. The B-Book: Assigning Programs to Meanings</ref>where an abstract atomic statement may be refined into an operation which body is made of a sequence of assignments. However, the introduction of the semicolon operator in Event-B is a substantial change affecting most aspects of the method. This would also reintroduce one of the problems of the Classical B that Event-B tries to address: proof scalability. Accumulation of sequential composition through refinement steps may result in unmanageable proof obligations. It is also more difficult to conduct subsequent refinement of events with sequential actions.
+
To test our approach, we have built translators for C, Ada and Java using the same underlying abstract translators.  
−
 
+
Additionally we consider the case where a new language may be required that has only modest differences to an existing language. A good example of this is to consider the case where a different library may want to be used from one used in an existing translation. For instance in C, concurrency can be achieved through different mechanisms such as OpenMP or Pthreads. In this case it may be that all but the mechanism for handling a subroutine call are the same, meaning that the majority of the translation can occur using common translators, with separate translators for the different methods of handling a subroutine call. To allow for this we allow the developer to assign a core and specialisation language to each translator they build. In cases where a translator for the specialisation language does not exist, the translator will automatically defer to the default core language translator, if one exists. This means that default translators for a particular core language can be written for the majority of the translation, with specialisations being provided where differences occur. The core and specialisation of the language is also reflected in the theory translator, meaning that language theories are only required for the core languages, rather than for each individual specialization.
−
Actions Systems <ref name="as">R.J.R. Back and R.Kurki-Suonio, Decentralization of process nets with centralized control. 2nd annual symposium on principles of distributed computing, Montreal 1983</ref>has an atomicity refinement technique where one can refine an atomic action into a loop of new actions<ref name="ref"> R.J.R. Back. Atomicity Refinement in a Refinement Calculus Framework (Back92:atomicity)</ref>. This is general enough to address the problem but, seemingly, the associated proof cost is prohibitively high and there is no evidence that such proofs may be efficiently mechanised.
 
−
 
 
−
The challenge was addressed by offering a method that lets a modeller to select an alternative set of refinement laws whenever the identified pattern of refinement is encountered. The new refinement laws are based on a different interpretation of a model: split refinement (a case of event refinement when an abstract event is refined into two or more concrete alternatives) is understood as a refinement into a composite event made of the concrete events arranged in some way. One simple arrangement case is when the concrete events are understood to execute sequentially. Then the refinement relation is demonstrated for the after-state produced by executing one event after another.
 
−
 
 
−
The method is not limited to sequential composition and there is also a form of parallel composition. An essential property of the method is that the group refinement relation is demonstrated not just for a single arrangement of concrete events but for a whole set of traces of concrete events. There is a simple notation for the removal of undesired traces and constraining the model to specific traces. For each trace there appears one instance of action simulation proof obligation (and possibly other refinement and consistency proof obligations). Thus, for practical reasons, it is necessary to keep number of traces low. This is best accomplished by doing small refinement steps with few concrete events.
 
−
 
 
−
== Modes ==
 
−
The main objective in the tool design was to make a simple to use environment that can be used by a non-Event-B user (e.g. requirements engineer, fault tolerance specialist), yet provides the necessary functionality for an Event-B modeller. The tool was designed to be as much an external environment to Event-B models as possible.
 
−
* We decided not to extend the Rodin database with modal and fault tolerance elements and to keep them as separate models. This led to less platform dependencies and easier maintenance.
 
−
* The static check is separated from the Rodin SC, and realized by the GMF validation since it does not logically belong to Rodin / Event-B. However, since the proofs are a part of the modelling process, we properly extended the Rodin proof obligation generator.
 
−
* A modal/FT documents form a refinement chain that mimics the Event-B refinement. This allows our tool to be used with the existing types of decomposition / modularisation.
 
−
* During the initial experiments we have identified a possible need for multiple views on a single model. The tool supports this by keeping the references to the models in the views and not the opposite.
 
−
 
 
−
== Qualitative Reasoning ==
 
−
* Ideally, we would like to have a new value for the '''convergence''' attribute of Event-B events. However, this is not currently supported by the Rodin platform.  Instead, a new '''probabilistic''' attribute is defined for events, with the value is either ''standard'' or ''probabilistic''.
 
−
 
 
−
* Since standard refinement does not maintain probabilistic convergent property, we put a restriction on the development method for ''almost-certain termination systems'' in two steps as follows.
 
−
*# Establish the model of the systems with various ''anticipated'' events
 
−
*# While proving convergence properties of events (either standard or probabilistic), we keep the variable and event system the same (i.e. no refinement is allowed).
 
−
 
 
−
* For probabilistic convergence, the variant need to be bounded above.  A combination of standard and probabilistic convergence events results in a probabilistic convergence system. Moreover, the use of anticipated events and refinement allowed us to construct an lexicographic variant by combining the sub-variant at different level of refinements. For probabilistic convergence system, this lexicographic variant need to be bounded above, which require all the sub-variants to be bounded above (not only those variant concern with probabilistic events).
 
−
 
 
−
More details of our approach is in our report at AVoCS'10 <ref name="avocs10">[http://deploy-eprints.ecs.soton.ac.uk/258/ E. Yilmaz and T.S. Hoang, Development of Rabin's Choice Coordination Algorithm in Event-B. ''Proceedings of AVoCS'10'', Dusseldorf, Germany, 2010]</ref>.
 
  
 
= Available Documentation =
 
= Available Documentation =
 +
We have updated the documentation, including the Tasking Event-B Overview, and Tutorial materials.
 +
[[TODO]] ''complete''
  
−
== Flow plug-in ==
+
= Status =
−
* An extensive example of the application of the flows in the modelling (the old version) is available to the DEPLOY Project members as a part of the Bosch cruise control case study.
 
−
* There is a wiki page describing the core proof obligations generated by the tool - Flows
 
−
* Tutorial slides available from the project file share
 
−
 
 
−
== Group Refinement ==
 
−
* There is a wiki page - [[Group refinement plugin]] - briefly introducing the approach and the tool
 
−
* Slides
 
−
 
 
−
== Modes ==
 
−
* There is a [http://wiki.event-b.org/index.php/Mode/FT_Views wiki page] with details of the plug-in functionality, installation guide, and a simple example.
 
−
* Papers on modal specifications <ref>[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.148.6369&rep=rep1&type=pdf A.Iliasov, A.Romanovsky, F.L.Dotti. Structuring Specifications with Modes. Fourth Latin-American Symposium on Dependable Computing - LADC 09, September 1-4, 2009]</ref> and <ref>[http://deploy-eprints.ecs.soton.ac.uk/153/1/paper105%2DICFEM09.pdf F.L.Dotti, A.Iliasov, L.Riberiro, A.Romanovsky. Modal Systems: Specification, Refinement and Realisation. In: International Conference on Formal Engineering Methods - ICFEM 09 , December 9 -12, 2009, Rio de Janeiro, Brazil]</ref>, and fault tolerance <ref>[http://www.cs.ncl.ac.uk/publications/trs/papers/1188.pdf I.Lopatkin, A.Iliasov, A.Romanovsky. On Fault Tolerance Reuse during Refinement. In: 2nd International Workshop on Software Engineering for Resilient Systems - SERENE 2010, April 13-16, 2010, London]</ref>.
 
−
* Also, we are working on a medium-scale case study
 
−
 
 
−
== Qualitative Reasoning ==
 
−
* Master thesis of Emre Yilmaz on developing tool support for qualitative reasoning in Event-B <ref>[http://e-collection.ethbib.ethz.ch/view/eth:1677  E. Yilmaz. Tool support for qualitative reasoning in Event-B. Master's thesis, Department of Computer Science, ETH Zurich, Switzerland, Aug. 2010]</ref>.
 
−
 
 
−
* The development of Rabin's Choice Coordination Algorithm is available at the DEPLOY Repository <ref>[http://deploy-eprints.ecs.soton.ac.uk/232/ E. Yilmaz. Rabin's Choice Coordination Development.]</ref>.
 
−
 
 
−
* A paper describing the development of Rabin Choice Coordination algorithm and tool support in the Proceedings of AVoCS'10 <ref name="avocs10"/>.
 
−
 
 
−
= Planning =
 
−
 
 
−
== Flow plug-in ==
 
−
The plan is to gather feedback from the users within the Project and encourage the external users to try out the plug-in and provide feedback and feature requests. There are many ideas on the tool extension, in particular using the tool to document event refinement (split, merge, group, refinement diagrams) and provide mechanised patterns for some of the more important cases.
 
−
 
 
−
== Group Refinement ==
 
−
The immediate plan is to produce a technical report on the semantics of group refinement during the first quarter of 2011. Long term plans are the tool maintenance and the investigation of the possibility of more expressive form of group refinement permitting branches and loops.
 
−
 
 
−
== Modes ==
 
−
Current status is version 1.0.0 for Rodin 2.0
 
−
In a long term we plan:
 
−
* A few usability improvements
 
−
* Integration with ProR requirements tracing framework
 
−
* Event-B model generation and editing driven by FT patterns
 
  
−
== Qualitative Reasoning ==
+
We released a new version of the code generator on 22-03-2012. The changes were made to the methodology, user interface, and tooling. The first version of the code generator supported translation to Ada, and the current version also has limited support for C.
−
In DEPLOY's fourth year, we plan to implement the missing proof obligations. More importantly, we will investigate the interaction between refinement and almost certain termination. This allows us to prove convergence properties early in the development and guarantee that refinement will maintain these convergent properties.
 
  
−
=== References ===
+
= References =
 
<references/>
 
<references/>
  
−
[[Category:D32 Deliverable]]
+
[[Category:D45 Deliverable]]

Revision as of 07:48, 20 April 2012

Overview

The code generation plug-in allows the generation of code for typical real-time embedded control software from refined Event-B models. Such a feature will be an important factor in ensuring eventual deployment of the DEPLOY approach within industrial organisations.

Motivations

DEPLOY industrial partners are interested in the formal development of multi-tasking, embedded control systems. During the project, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems [1][2][3][4][5]. Initially, we chose to translate to the Ada programming language[6], and use it as a basis for the abstractions used in our approach.
We described our previous code generation feature as a demonstrator tool; chiefly a tool designed as a proof of concept, used by us to validate the approach. In this sense, the tool as it stands now, is the first prototype intended to be used by developers, and thus motivated numerous evolutions and new features such as:

  • allowing a more seamless edition of tasking Event-B,
  • supporting extensibility,
  • supporting other target languages than just Ada,
  • supporting programming concepts reification using abstract translators.

Choices / Decisions

Considering the demonstrator as a baseline, we can list the new features as follows:

  • Tasking Event-B is now integrated with the Event-B explorer. It uses the extensibility mechanism of Event-B EMF (In the previous version it was a separate model).
  • Tasking Event-B is now integrated with the Event-B model editors. Tasking Event-B features can now be edited in the same place as the other Event-B features.
  • We have the ability to translate to Java and C, in addition to Ada source code; and the source code is placed in appropriate files within the project.
  • We use theories to define translations of the Event-B mathematical language (Theories for Ada and C are supplied).
  • We use the theory plug-in as a mechanism for defining new data types , and the translations to target data types.
  • The Tasking Event-B to Event-B translator is fully integrated. The previous tool generated a copy of the project, but this is no longer the case.
  • The translator is extensible.
  • The composed machine component is used to store event 'synchronizations'.
  • Minimal use is made of the EMF tree editor in Rose.

These evolutions will be detailed hereafter. Moreover, the code generators have been completely re-written. The translators are now implemented using Java only. In our previous work we attempted to make use of the latest model-to-model transformation technology, available in the Epsilon tool set[7], but we decided to revert to Java since Epsilon lacked the debugging and productivity features of the Eclipse Java editor.

Tasking Event-B and its edition

A text-based task body editor was added, to minimize the amount of editing required with the EMF tree editor. The task body editor is associated with a parser-builder; after the text is entered in the editor the EMF representation is generated (by clicking a button) that is, assuming parsing is successful. If the parser detects an error, information about the parse error is displayed in an adjoining text box. When specifying events in the task body, there is no longer a need to specify two events involved in a synchronization. The code generator automatically finds the corresponding event of a synchronization, based on the event name, and using the composed machine component [8]. Composed machines are used to store event 'synchronizations', and 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 new feature also overcomes the 'problem' that we previously experienced, with duplicate event names in a development, and event selection, when specifying the task body. The EMF tree editor in Rose is now only used minimally; to add annotations for Tasking, Shared and Environ Machines; typing annotations, and parameter direction information; and sensing/actuating annotations, where necessary. Further work is under way to integrate the code generation feature with the new Rodin editor.

Allowing Extensibility

The code generation approach is now extensible; in that, 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. 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.

Targeting new Languages

Making the step from Event-B to code is a process that can be aided through automatic code generation. The code generation plug-in for Rodin is a new tool for translating Event-B models to concurrent programmes. However users of such a tool will likely require a diverse range of target languages and target platforms, for which we do not currently provide translations.Some of these languages may be subtly different to existing languages and only have modest differences between the translation rules, for example C and C++, whilst others may have more fundamental differences. As the translation from Event-B to executable code is non-trivial and to reduce the likelihood of error, we want to generalize as much of the translation as possible so that existing translation rules are re-used. Therefore significant effort is needed to ensure that such a translation tool is extensible to allow additional languages to be included with relative ease. Here we concentrate on translation from a previously defined Common Language Meta-model, the intermediary language IL1, which Event-B translates to directly. IL1 is an EMF metamodel representation of generic properties and functionality found in many programming languages. It has representations for key structural concepts such as variables, subroutines, function calls and parameters. The translation of predicates and expressions contained within the code are handled by a new extension to the theory plug-in, which allows translation rules to be developed for specific target languages within the Rodin environment. The generic nature of the intermediary language is designed to allow for a wide range of different target languages. Developers of new target languages are required to write translators in Java for the conversion from the EMF representation to the code of their target language. To do this we provide a central translation manager, that takes an IL1 model and automatically calls the appropriate translators for each element of the model, whilst also providing the link to the predicate and expression translators provided by the new theory plug-in. The developer registers their translators for the target language through an extension point, where currently there are 15 light-weight translators required for a new target language. To aid the developer, we provide abstract translators for each required element in the IL1 model that has to be translated. These translators perform the majority of the translation automatically, meaning that in most cases all the developer is required to do is format strings into the appropriate structure for their target language. For example in an branch statement, the developer would be required to write a method stating how a branch is defined and structured in their language, using a set of previously translated guard conditions and actions. Importantly, the flexibility remains for the developer to re-write any of the translations if the ones provided are not suitable.

Using Abstract Translators

To test our approach, we have built translators for C, Ada and Java using the same underlying abstract translators. Additionally we consider the case where a new language may be required that has only modest differences to an existing language. A good example of this is to consider the case where a different library may want to be used from one used in an existing translation. For instance in C, concurrency can be achieved through different mechanisms such as OpenMP or Pthreads. In this case it may be that all but the mechanism for handling a subroutine call are the same, meaning that the majority of the translation can occur using common translators, with separate translators for the different methods of handling a subroutine call. To allow for this we allow the developer to assign a core and specialisation language to each translator they build. In cases where a translator for the specialisation language does not exist, the translator will automatically defer to the default core language translator, if one exists. This means that default translators for a particular core language can be written for the majority of the translation, with specialisations being provided where differences occur. The core and specialisation of the language is also reflected in the theory translator, meaning that language theories are only required for the core languages, rather than for each individual specialization.

Available Documentation

We have updated the documentation, including the Tasking Event-B Overview, and Tutorial materials. TODO complete

Status

We released a new version of the code generator on 22-03-2012. The changes were made to the methodology, user interface, and tooling. The first version of the code generator supported translation to Ada, and the current version also has limited support for C.

References

  1. ↑ http://eprints.soton.ac.uk/270824/ "Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010"
  2. ↑ http://eprints.soton.ac.uk/272006/ "Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany"
  3. ↑ http://eprints.soton.ac.uk/272771/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B Models to Code: Sensing, Actuating, and the Environment. At SBMF2011, Sao Paulo, Brazil, 28 - 26 Sep 2011."
  4. ↑ http://eprints.soton.ac.uk/335400/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp. (In Press)"
  5. ↑ http://eprints.soton.ac.uk/336226/ "Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp. (In Press)"
  6. ↑ J. Barnes. Programming in Ada 2005. International Computer Science Series. Addison Wesley, 2006.
  7. ↑ http://www.eclipse.org/epsilon/
  8. ↑ http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B
Retrieved from ‘https://wiki.event-b.org/index.php?title=D32_Scalability&oldid=2748’