User:Jens/Code generation Using Flow Analysis

Concurrent Embedded Programs from Event-B Models

We propose a method for concurrent program development in Event-B. The final step of the method, code generation, is fully automatic so that the user is concerned only with formal Event-B models but not with code generation. The target architecture is AUTOSAR, a cooperative concurrent real-time architecture used in the automotive industry: programs consist threads that are split into blocks, called runnables. These runnables are executed concurrently by an embedded operating systems. From this description we see that we immediately face two problems: how to decompose into threads and how to specify runnables.

Following the method of sequential program development proposed by Abrial, the entire development takes place in Event-B only applying a method for thread and runnable decomposition. Our approach uses formal control flow analysis to compose programs from events on the way removing automatically abstract program counters from the Event-B model.

In order for the method to work four techniques need to be developed:

1. thread decomposition
2. runnable decomposition
3. control flow analysis
4. event composition

Concerning 1. and 2. we can rely on existing work on (concurrent) decomposition. Concerning 3. we have made preliminary experiments that look promising, and 4. has been developed by Abrial.