Title :
On compatibility and behavioural substitutability of component protocols
Author :
Hameurlain, Nabil
Author_Institution :
LIUPPA Lab., Pau Univ., France
Abstract :
Component based development (CBD) aims to facilitate the construction of large-scale applications by supporting the composition of simple building blocks into complex applications. Components specification is thus needed to ensure the safety of composing systems from components. This paper focus on component protocols specification and provides a framework for modelling protocols together with their composition. We start by investigating compatibility of component protocols based on service observation. Two compatibility relations together with their characterisation by the preservation to their degree of change property are proposed. Safety and liveness properties such as deadlock-freeness and proper termination of protocols are preserved up to different extents. Then, we propose some behavioural subtyping relations for component protocols related to the principle of substitutability. Finally, we address the soundness of our subtyping relations by showing the existing link between compatibility and substitutability concepts, namely their combination, which have found necessary when dealing with incremental design of components.
Keywords :
formal specification; formal verification; object-oriented programming; protocols; component based development; component protocol specification; component specification; formal verification; Application software; Assembly systems; Laboratories; Large-scale systems; Petri nets; Protocols; Safety; Software engineering; Software systems; System recovery;
Conference_Titel :
Software Engineering and Formal Methods, 2005. SEFM 2005. Third IEEE International Conference on
Print_ISBN :
0-7695-2435-4
DOI :
10.1109/SEFM.2005.30