An Algebraic Theory for Web Service Contracts

We study the foundations of Web service technologies for connecting abstract and concrete service definitions and for discovering services according to their observable behavior. We pursue this study addressing a subset of BPEL activities that include concurrency constructs. We present a formal semantics-called compliance preorder-of this subset of BPEL and we define a behavioral type discipline that guarantees the correctness of client-server interactions. The types of our discipline, called contracts, are De Nicola and Hennessy tau-less, finite-state CCS processes. We show that contracts are BPEL normal forms according to the compliance preorder and that the compliance preorder does coincide with a well-known equivalence in concurrency theory, the must-testing preorder. The compliace preorder is not fully adequate for discovering Web services though, since it does not support width and depth extensions of Web services. To address this issue, we propose a sound generalization of the compliance preorder, called subcontract relation, that admits a notion of principal service contract-the dual contract-compliant with a given client contract and that exhibits good precongruence properties when choreographies of Web services are considered.