Andrew Edmunds

Michael Butler, John Colley, Andrew Edmunds et al.

This paper provides an overview of the CODA framework for modelling and refinement of component-based embedded systems. CODA is an extension of Event-B and UML-B and is supported by a plug-in for the Rodin toolset. CODA augments Event-B with constructs for component-based modelling including components, communications ports, port connectors, timed communications and timing triggers. Component behaviour is specified through a combination of UML-B state machines and Event-B. CODA communications and timing are given an Event-B semantics through translation rules. Refinement is based on Event-B refinement and allows layered construction of CODA models in a consistent way.

Andrew Edmunds, Michael Butler, John Colley

The RODIN, and DEPLOY projects laid solid foundations for further theoretical, and practical (methodological and tooling) advances with Event-B. Our current interest is the co-simulation of cyber-physical systems using Event-B. Using this approach we aim to simulate various features of the environment separately, in order to exercise deployable code. This paper has two contributions, the first is the extension of the code generation work of DEPLOY, where we add the ability to generate code from Event-B state-machine diagrams. The second describes how we may use code, generated from state-machines, to simulate the environment, and simulate concurrently executing state-machines, in a single task. We show how we can instrument the code to guide the simulation, by controlling the relative rate that non-deterministic transitions are traversed in the simulation.