Modelling and Refinement in CODA

Authors :: Andrew Edmunds
Michael Butler
John Colley
Helen Marshall
Neil Evans
Neil Grant
Colin Snook
Source :: Electronic Proceedings in Theoretical Computer Science, Vol 115, Iss Proc. Refine 2013, Pp 36-51 (2013), Refine@IFM
Publication Year :: 2013
Publisher :: arXiv, 2013.
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.<br />Comment: In Proceedings Refine 2013, arXiv:1305.5634

Database :: OpenAIRE
Journal :: Electronic Proceedings in Theoretical Computer Science, Vol 115, Iss Proc. Refine 2013, Pp 36-51 (2013), Refine@IFM
Accession number :: edsair.doi.dedup.....e8ee617222cbfaa89dd07bd5ff9cddcf
Full Text :: https://doi.org/10.48550/arxiv.1305.6112