Building on the DEPLOY Legacy: Code Generation and Simulation

TL;DR

This paper extends Event-B code generation to include state-machine diagrams and demonstrates their use in simulating cyber-physical environments with controlled, concurrent state-machine execution.

Contribution

It introduces new code generation capabilities from Event-B state-machines and shows how to use this code for environment simulation and concurrent execution control.

Findings

Generated code from state-machines enables environment simulation.

Controlled traversal of non-deterministic transitions improves simulation fidelity.

Concurrent state-machine execution is feasible within a single task.

Abstract

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.