• Publication
  • PrePrints
  • Abstract - Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces
PrePrint
ISSN: 1939-1374
Aysu Betin-Can, Middle East Tehcnical University, Ankara
Sylvain Halle, University of Quebec at Chicoutimi, Chicoutimi
Tevfik Bultan, University of California at Santa Barbara, Santa Barbara
A crucial problem in service oriented computing is the specification and analysis of interactions among multiple peers that communicate via messages. We propose a design pattern that enables the specification of behavioral interfaces acting as communication contracts between peers. This "peer controller pattern" provides a modular, assume-guarantee style verification strategy that consists of three phases. 1) Each individual peer is statically verified for conformance to its part of the contract, using software model checking. 2) Alternately, an enforcement mechanism blocks the communication events that violate the interface specification at runtime. 3) Using either of these two mechanisms, it can be assumed that the participating peers behave according to their interfaces. Safety and liveness properties about the global behavior of the composite web service can then be verified directly on the communication contract. The interface verification of each peer and the behavior verification are hence handled in separate steps. A Java implementation of this pattern is developed and tested on a series of examples; we show that by working in such a modular fashion, it is possible to automatically and efficiently verify properties about service interactions that would otherwise be impossible to verify.
Index Terms:
Validation, Patterns, Formal methods, Model checking, Web-based services, Web Services Interoperability, Stateful Web Services, Formalization of Services Composition
Citation:
Aysu Betin-Can, Sylvain Halle, Tevfik Bultan, "Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces," IEEE Transactions on Services Computing, 02 Nov. 2011. IEEE computer Society Digital Library. IEEE Computer Society, <http://doi.ieeecomputersociety.org/10.1109/TSC.2011.55>
Usage of this product signifies your acceptance of the Terms of Use.