Behavioural contracts with request–response operations

In the context of service-oriented computing, behavioural contracts are abstract descriptions of the message-passing behaviour of services. They can be used to check properties of service compositions such as, for instance, client-service compliance. To the best of our knowledge, previous formal models for contracts consider unidirectional send and receive operations. In this paper, we present two models for contracts with bidirectional request–response operations, in the presence of unboundedly many instances of both clients and servers. The first model takes inspiration from the abstract service interface language WSCL, the second one is inspired by Abstract WS-BPEL. We prove that two different notions of client-service compliance (one based on client satisfaction and another one requiring mutual completion) are decidable in the former while they are undecidable in the latter, thus showing an interesting expressiveness gap between the modelling of request–response operations in WSCL and in Abstract WS-BPEL.

► We study two models for contracts with bidirectional request–response operations. ► We study decidability of different notions of client-service compliance in both. ► We prove that compliance is decidable in the first model, inspired by WSCL. ► We prove that compliance is not decidable in the second model, inspired by WS-BPEL. ► We detect an expressiveness gap between request–response operations in the two models.