Oxford logo
[CCJK12b] T. Chen, C. Chilton, B. Jonsson and M. Kwiatkowska. A Compositional Specification Theory for Component Behaviours. Technical report CS-RR-12-01, Department of Computer Science, University of Oxford. 2012. [pdf] [bib]
Downloads:  pdf pdf (973 KB)  bib bib
Notes: This is the technical report accompanying [CCJK12].
Abstract. We propose a compositional specification theory for reasoning about components that interact by synchronisation of input and output (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a theory is motivated by the need to support composability of components, in addition to modelling environmental assumptions, and reasoning about run-time behaviour. Models can be specified operationally by means of I/O labelled transition systems augmented by an inconsistency predicate on states, or in a purely declarative manner by means of traces. We introduce a refinement preorder that supports safe-substitutivity of components. Our specification theory includes the operations of parallel composition for composing components at run-time, logical conjunction for independent development, and quotient for incremental development. We prove congruence properties of the operations and show correspondence between the operational and declarative frameworks.