Tasking Event-B Tutorial: Difference between revisions
imported>Andy |
imported>Andy |
||
| Line 11: | Line 11: | ||
{| border="1" | {| border="1" | ||
|Heating_ControllerTutorial_Completed | |Heating_ControllerTutorial_Completed | ||
|An example project generating an environment simulation. Generates code, where environment variables are monitored and controlled using subroutine calls. Contains a completed Tasking Development | |An example project generating an environment simulation. Generates code, where environment variables are monitored and controlled using subroutine calls. Contains a completed Tasking Development with generated Event-B and Ada code. | ||
|- | |- | ||
|Heating_ControllerTutorial_Step1 | |Heating_ControllerTutorial_Step1 | ||
| Line 21: | Line 18: | ||
|Heating_ControllerTutorial_Step2 | |Heating_ControllerTutorial_Step2 | ||
|A partially completed tasking development for steps 2, and 4 of the [[Code_Generation_Tutorial#The_Tutorial |tutorial]] (step 3 not required here). | |A partially completed tasking development for steps 2, and 4 of the [[Code_Generation_Tutorial#The_Tutorial |tutorial]] (step 3 not required here). | ||
|- | <!--|- > | ||
|Heating_Controller5AddressedSim_Completed | <!--|Heating_Controller5AddressedSim_Completed> | ||
|A completed example that uses Addressed Variables in the tasks, and also in the environment simulation. Generates Memory Mapped IO for sensing and actuation. | <!--|A completed example that uses Addressed Variables in the tasks, and also in the environment simulation. Generates Memory Mapped IO for sensing and actuation. > | ||
|- | <!--|-> | ||
|Heating_Controller5AddressedNotSim_Completed | <!--|Heating_Controller5AddressedNotSim_Completed> | ||
|A completed example that uses Addressed Variables in the tasks only. Generates Deployable Memory Mapped IO for sensing and actuation. Similar to above but we discard the environment task from generated code. | <!--|A completed example that uses Addressed Variables in the tasks only. Generates Deployable Memory Mapped IO for sensing and actuation. Similar to above but we discard the environment task from generated code.> | ||
|} | |} | ||
Revision as of 09:14, 29 November 2011
For more information contact Andy Edmunds - University of Southampton - mailto:ae2@ecs.soton.ac.uk
Tasking Event-B Tutorial Overview
This tutorial follows on from the abstract development described here.
This code generation tutorial extends the Heating Controller tutorial example, and makes use of example projects from the download site. The code generation stage produces implementable Ada code, and also an Event-B model. It is a model of the implementation, and contains flow control variables that model the flow of execution through the task body. The Ada code is produced from an intermediate model that is not visible to the user. The Common Language model (CLM), is generated from the Tasking Event-B by a translation tool. Ada (and other implementations) may be generated from the CLM. An overview of Tasking Event-B can be found here.
In the example so far, the Heating Controller has been refined to the point where we wish to add implementation constructs. The Event-B language is not expressive enough to fully describe the implementation. Tasking Event-B facilitates this final step to implementation, by extending Event-B with the necessary constructs. Event-B machines modelling tasks, shared objects and the environment are identified, and extended with the appropriate implementation details.
The example/tutorial projects are are available in the e-prints archive, or on SVN.
| Heating_ControllerTutorial_Completed | An example project generating an environment simulation. Generates code, where environment variables are monitored and controlled using subroutine calls. Contains a completed Tasking Development with generated Event-B and Ada code. |
| Heating_ControllerTutorial_Step1 | A bare project for step 1 of the tutorial. |
| Heating_ControllerTutorial_Step2 | A partially completed tasking development for steps 2, and 4 of the tutorial (step 3 not required here). |
