Analysis and Verification of Service Contracts
Joseph C. Okika · 2010
Service contracts are specifications used by interacting services to agree on ways of interaction to achieve an intended business goal. This raises a number of interesting questions. What languages are used to express service contracts? What are the semantics of the languages? Do the connected services adhere to the contract and behave as expected? Are the specifications consistent? To answer these and other questions, this work reports on a study of service contract specification languages, define semantics of a particular language, and analyze behavioural specification of service contracts using simulation and model checking techniques. Chronologically, the first contribution is an automated technique to check consistency properties across specifications. The results of the consistency checks reveal that the derived processes from the two service contract specifications (WS-CDL and BPEL) are bisimilar and trace equivalent only when certain intricate features, e.g., fault handling, is hidden. Therefore we note that WS-CDL can only be consistent with an abstract version of BPEL without the presence of some intricate features. In the second contribution, we derive semantic models in the form of timed automata and check the absence of deadlock for WS-CDL and BPEL service contract specifications. We check the property that the system is able to progress from start to termination and for a BPEL process, we check that the methods can be executed satisfying the contracts or generating the exceptions. Other contributions include: a classification of languages and standards based on the aspects of service contracts they cover; a structural operational semantics of BPEL activities; a prototype executable semantics of BPEL based on Rewriting Logic and Maude; and a translation process that maps a BPEL process to UppAal timed automata for automatic verification. In conclusion, we argue that introducing (automated) analyses and verification of service contracts at the design and development phase before testing and deployment will improve the reliability of service-based systems. The analyses prototyped here improve our understanding of the behaviour of connected services.