Electronic Proceedings in Theoretical Computer Science (May 2013)

Modelling and Refinement in CODA

  • Michael Butler,
  • John Colley,
  • Andrew Edmunds,
  • Colin Snook,
  • Neil Evans,
  • Neil Grant,
  • Helen Marshall

DOI
https://doi.org/10.4204/EPTCS.115.3
Journal volume & issue
Vol. 115, no. Proc. Refine 2013
pp. 36 – 51

Abstract

Read online

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.