Oxford logo
[CCJK12] T. Chen, C. Chilton, B. Jonsson, and M. Kwiatkowska. A Compositional Specification Theory for Component Behaviours. In H. Seidl (editor), Programming Languages and Systems, Proc. 21st European Symposium on Programming (ESOP'12), volume 7211 of LNCS, pages 148-168, Springer. March 2012. [pdf] [bib]
Downloads:  pdf pdf (364 KB)  bib bib
Notes: A list of errata is available here. A version of this paper including proofs is made available as [CCJK12b]. The original publication is available at www.springerlink.com.
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.