Tasking Event-B Tutorial

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