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.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

Contributeur : Hongyang Qu <>
Soumis le : vendredi 3 février 2012 - 14:43:55
Dernière modification le : mardi 7 février 2012 - 11:53:56
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 04:03:26


Accord explicite pour ce dépôt


  • HAL Id : hal-00665599, version 1



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



Consultations de la notice


Téléchargements de fichiers