Modelling and Refinement in CODA

Michael Butler
(University of Southampton)
John Colley
(University of Southampton)
Andrew Edmunds
(University of Southampton)
Colin Snook
(University of Southampton)
Neil Evans
(AWE)
Neil Grant
(AWE)
Helen Marshall
(AWE)

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.

In John Derrick, Eerke Boiten and Steve Reeves: Proceedings 16th International Refinement Workshop (Refine 2013), Turku, Finland, 11th June 2013, Electronic Proceedings in Theoretical Computer Science 115, pp. 36–51.
Published: 24th May 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.115.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org