Interactive specification and verification of behavioral adaptation contracts

Abstract : Context. 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 interaction protocols are considered in service interfaces. Objective. In this article, we propose a tool-based, interactive approach to support the contract design process. Method. Our approach includes: (i) a graphical notation to define port bindings, and an interface compatibility 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. Results. Our results show a reduction both in the amount of effort that the designer has to put into building the contract, as well as in the number of errors present in the final result (noticeably higher in the case of manual specification). Conclusion. We conclude that it is important to provide integrated tool support for the specification and verification of adaptation contracts, since their incorrect specification induces erroneous executions of the system. To the best of our knowledge, such tool support has not been provided by any other approach so far, and hence we consider the techniques described in this paper as an important contribution to the area of behavioral software adaptation.
Document type :
Journal articles
Information and Software Technology, Elsevier, 2012, 54 (7), pp.701-723
Liste complète des métadonnées


https://hal.archives-ouvertes.fr/hal-00694516
Contributor : Gwen Salaün <>
Submitted on : Saturday, May 5, 2012 - 8:18:02 AM
Last modification on : Monday, October 5, 2015 - 5:01:09 PM
Document(s) archivé(s) le : Friday, November 30, 2012 - 11:10:57 AM

File

CSCO-IST3-1.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00694516, version 1

Collections

Citation

Javier Cámara, Gwen Salaün, Carlos Canal, Meriem Ouederni. Interactive specification and verification of behavioral adaptation contracts. Information and Software Technology, Elsevier, 2012, 54 (7), pp.701-723. <hal-00694516>

Share

Metrics

Record views

309

Document downloads

250