Current Developments

Overview and Motivation

Code generation is an important part of the formal engineering tool chain that will enable complete support for development from high-level models down to executable implementations. Work has commenced on the development of support for code generation from Event-B models. This is a new line of work for DEPLOY that was not identified in the original Description of Work for the project. During the first year of the project, as the Deployment Partners gained experience with deployment of formal modelling, it became clear that having 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 is especially true for Bosch and Space Systems Finland (SSF). During the DEPLOY re-focus at Month 18, it was decided to introduce a code generation task into a revised workplan and devote resources to this task.

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. In essence, this involves programs structured as tasks running concurrently such as supported by the Ada tasking model. The individual tasks are sequential programs and tasks share state variables via some form of monitor mechanism. For real-time control, both periodic and aperiodic task should be supported; tasks should have priorities to ensure appropriate responsiveness of the control software.

For the DEPLOY pilots, it is 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 is required. It is not our intention to develop a fully-fledged industrial-strength code generation framework within the lifetime of the DEPLOY project. Instead an aim is to develop a sufficient framework to act as a proof-of-concept to enable code generation for the Bosch and SSF pilots. A further aim is to gain practical experience with a prototype code generation framework that will serve as a basis for future R&D on a scalable code generation framework. The code generation work is being lead by Southampton with initial input from Newcastle.

Choices/Decisions

Three candidate approaches have been posited as follows; • Enrich Event-B with explicit algorithmic structures for use in later refinement stages and use these explicit structures to guide code generation • Synthesise sequential and concurrent code from existing low-level Event-B models • Exploit the code generation facilities of Atelier-B for “classical” B

Approach 3 will be important for STS in WP2 as it will enable integration of Rodin with the existing development process in STS with AtelierB and some effort will be devoted to this. However, this approach will not address the needs of all the deployments because of the overhead involved in having to use AtelierB alongside Rodin as well as the lack of support for concurrent code generation in AtelierB. Supporting Approach 2 has the attraction that developers can remain within the uniform language framework of Event-B. However, it is not clear that we can meet the real-time performance guarantees required for embedded systems with this approach within the lifetime of the DEPLOY project.

While we will pursue some exploration of this approach, we will focus most effort on Approach 1 as this will enable existing techniques for real-time programming to be incorporated in later stages of development. Language support for explicit sequential and concurrent programs will be defined to enable construction of code-oriented models at low levels of refinement. We refer to this form of Event-B as task-oriented. A code generation framework will be developed to enable automated generation of C and Ada subsets suitable for real-time embedded systems from code-oriented models. A refinement-based proof method for code-oriented models will be defined and incorporated into the Rodin toolset.

An important requirement is that the code generation framework be amenable to extension and tailoring for specific needs. Rather than hard-wiring the code generation rules into the tool, we will aim to support a declarative rule-based approach to defining translation from task-oriented Event-B to a target implementation language. The translation should be tailorable by modifying or extending the declarative translation rules. We will explore the use of a model-based transformation framework such as ATL or ETL for this purpose. Rather than fixing on a specific set of implementation-level data types, we will exploit the mathematical extension facility being developed for Rodin to enable a flexible approach to defining implementation-level data structures. For example, arrays could be supported by defining a new theory of arrays. This theory would define array declarations and operators along with an appropriate set of proof rules for arrays to enable reasoning. Appropriate declarative rules would then be defined to translate array declarations and expressions to appropriate code in the target language.

Tasking Language

The Event-B tasking language will support the following sequential and concurrent algorithmic constructs:

Behaviour	Algorithmic Construct
Sequence	;
Branching	if
Iteration	while
Task/Thread/Process	task
Shared variables	machine

A task-oriented model will be definable using the following abstract syntax

Task :=
	task Name
	variables Variables
	invariants Invariants
	begin TaskBody end

TaskBody :=
	Event
	$|$ TaskBody ; TaskBody
	$|$ if Guard→ TaskBody [] … [] Guard→ TaskBody fi
	$|$ do Guard→ TaskBody [] … [] Guard→ TaskBody od

The sequence, branching and iteration constructs correspond to their imperative counterparts. The task construct provides a means to specify the actions of interleaving, concurrent executions. A task may be implemented by an Ada task, or a thread in C. A task, in isolation, is a sequential program with clearly identified atomic steps, and each step corresponding to an atomic event.

The standard machine construct provides the mechanism for sharing data between the executing tasks. The interaction between a task and a machine can be represented synchronized event composition as currently supported by the synchronised-event plugin. The generated implementation will need to ensure that a task has mutually exclusive access to the variables represented in the machine. This is provided by a machine’s atomic events. A machine representing shared variables may be implemented by an Ada protected object, or in C by an explicit Mutex variable and appropriate lock acquisition.

To facilitate real-time programming constructs, we introduce the notion of task type, task period, and task priority

Task :=
	task Name
	tasktype periodic(p) $|$ triggered $|$ repeating $|$ oneshot
	priority n
	...

A tasktype is used to indicate the scheduling requirements for the required activity. It is typically the case in real-time systems that the required activity involves some repeating behaviour, this can be a continuously repeating loop, or one that repeats at a predetermined time interval. We introduce repeating and periodic tasktypes. The periodic task is parameterised by a time value. Activity can also be initiated by externally generated interrupts, which may arise from some user action or from the hardware itself. To accommodate this we introduce the triggered tasktype. The last type of activity that we consider is the one-shot task; where some activity is performed and not repeated. To facilitate this we add the oneshot tasktype. In some cases it may be useful to delay a task for a period of time; we introduce a delay to the TaskBody to facilitate this. It may be decided that, during a program’s execution, some of the activities should take precedence over some others. We introduce priority which allows a developer to assign a numerical value indicating the precedence for scheduling. We adopt the convention that higher priority activities have a greater value, and this corresponds to the Ada convention.

Methodological Support

As previously outlined, the atomic steps of a sequential task will be syntactically explicit. This is in order to facilitate a direct mapping of task steps with events of an abstract machine. The development approach that we plan to support fits with the general refinement approach of Event-B in that explicit tasking will be introduced as part of a refinement step. A common approach to specifying a problem is to represent some desired outcome as a single abstract atomic event. Common patterns of refinement of such abstract events found in existing Event-B developments are as follows:

1. Choice refinement: Event E is refined to E1 [] E2 []…[] En, where each Ei refines E
2. Sequential refinement: Event E is refined to E1 ; E2 ; … En, where some Ei refines E and the other Ej refine skip.
3. Loop refinement: Event E is refined to E1 ; do E2 od ; E3, where E3 refines E and E1 and E2 refine skip.

These patterns motivate a simpler subset of the tasking language as follows

TaskBody :=
	Event
	$|$ TaskBody ; TaskBody
	$|$ if Event [] … [] Event fi
	$|$ do Event endwith Event od

Initially we will support refinement to this subset by providing special structure-introduction refinement rules in the manner of the refinement calculus. We will also develop support for a generalisation of this set of rules in which the abstract model consists of a group of atomic events, with each event representing a different possible outcome. An example use of such a group would be to have an event to represent the normal behaviour of some system feature and a separate event to represent the error behaviour of the feature.

The above rules prevent the immediate introduction of nested tasking structures such as nested loops. Following the approach found in the refinement calculus and common practice in Event-B refinements, such nested structures may be introduced through further refinement steps. For example, to introduce a nested loop, the outer loop is first introduced and the inner loop is introduced in a subsequent refinement step. We will explore generalising the refinement support for tasks to support nesting through refinement along these lines.

Timescales

We refer to the tasking language outlined above as Version V1. Our planned timescales for further work on code generation are as follows:

• June 2010: demonstrator tool for language V1
• June 2010: initial support for user defined datatypes (math extn)
• From June to October 2010: experimentation with and assessment of the demonstrator tool on the WP1 and WP3 pilots leading to feedback on V1 and the tool
• Jan 2011: algorithmic language definition V2
• June 2011: prototype tool for V2
• From June to October 2011: experimentation with and assessment of the V2 tool on the WP1 and WP3 pilots