Code Generation Activity
From Event-B
Development Repository
The SVN repository for development of the code generation plug-in is here:
svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/trunk/CodeGeneration
Other information can be found here:
svn+ssh://svn.ecs.soton.ac.uk/projects/deploy-exploratory/CodeGeneration
Completed/Ongoing Work
- Demonstration plug-in,
- ready for deployment.
- deployment/Integration Testing under way.
- The plug-in 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.
- 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.
Metamodels
- Tasking Metamodel - one for both single and multi-tasking?
- Intermediate Language Metamodels based on Ada
- Initial Version is IL1
- Ready for experiments subject to decomposition.
- Metamodel re-structuring; will decompose into:
- Algorithmic structures
- Math. language
Translation Rules
- Tasking Metamodel to IL1 translation rules [[1]]
- Ready for experiments [4 May 2010] subject to decomposition into:
- Algorithmic structures
- Math. language
- Versions for Shared/Non-shared data
- Ready for experiments [4 May 2010] subject to decomposition into:
TODO
- Control flow modelling assistant
- Infrastructure plugin
- Initial version of:
- IL1 to Ada backend plugin
- Small experiments: several small models, reader/writer, heater control, circular buffer