Skip to Main content Skip to Navigation
New interface
Preprints, Working Papers, ...

A Compositional Specification Theory for Component Behaviours

Abstract : We propose a compositional specification theory for reason- ing about components that interact by synchronisation of input and out- put (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a the- ory 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 predi- cate 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 correspon- dence between the operational and declarative frameworks.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Hongyang Qu Connect in order to contact the contributor
Submitted on : Friday, February 3, 2012 - 2:43:55 PM
Last modification on : Tuesday, September 8, 2020 - 4:58:02 PM
Long-term archiving on: : Wednesday, December 14, 2016 - 4:03:26 AM


Explicit agreement for this submission


  • HAL Id : hal-00665599, version 1



Taolue Chen, Chris Chilton, Bengt Jonsson, Marta Kwiatkowska. A Compositional Specification Theory for Component Behaviours. 2012. ⟨hal-00665599⟩



Record views


Files downloads