Interactive Specification and Verification of Behavioural Adaptation Contracts

Adaptation is a crucial issue when building new applications by reusing existing software services which were not initially designed to interoperate with each other. Adaptation contracts describe composition constraints and adaptation requirements among these services. The writing of this specification by a designer is a difficult and error-prone task, especially when service protocol needs to be considered and service functionality accessed through behavioural interfaces. In this paper, we propose an interactive approach to support the contract design process, and more specifically: (i) a graphical notation to define port bindings, and an interface similarity measure to compare protocols and suggest some port connections to the designer, (ii) compositional and hierarchical techniques to facilitate the specification of adaptation contracts by building them incrementally, (iii) validation and verification techniques to check that the contract will make the involved services work correctly and as expected by the designer. Our approach is fully supported by a prototype tool we have implemented.