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
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSC.2011.55
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.
Validation, Patterns, Formal methods, Model checking, Web-based services, Web Services Interoperability, Stateful Web Services, Formalization of Services Composition
Aysu Betin-Can, Sylvain Halle, Tevfik Bultan, "Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces", IEEE Transactions on Services Computing, , no. 1, pp. , PrePrints PrePrints, doi:10.1109/TSC.2011.55