University of Oxford Logo University of OxfordDepartment of Computer Science - Home
Linked in
Linked in
Follow us on twitter
On Facebook

A Compositional Specification Theory for Component Behaviours

Taolue Chen, Chris Chilton, Bengt Jonsson, and Marta Kwiatkowska

In Helmut Seidl, editor, Programming Languages and Systems, Proc. 21st European Symposium on Programming (ESOP'12), Lecture Notes in Computer Science, vol. 7211, pp. 148-168. Springer-Verlag, 2012.


Downloads:   pdf pdf   bib bib   errata errata

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.

A version of this paper including proofs is made available here.

Note that this paper has largely been superseded by CS-RR-13-02.