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)
TL;DR
This paper introduces CODA, a framework extending Event-B and UML-B for component-based embedded system modeling, supporting refinement, timing, and communication constructs within the Rodin toolset.
Contribution
It presents CODA, a novel extension of Event-B and UML-B that enables component-based modeling with timing and communication features, integrated into the Rodin environment.
Findings
CODA supports layered refinement of component models.
The framework integrates UML-B state machines with Event-B semantics.
CODA facilitates formal verification of embedded system models.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.