Analyzing Web Service Contracts

Web services should be dependable, because businesses rely on them. For that purpose the service oriented architecture has standardized specifications at a syntactical level. In this paper, we demonstrate how such specifications are used to derive semantic models in the form of (timed) automata. These can be used to model check functional and behavioural properties of a given service. Since there might be several specifications dealing with different aspects, one must also check that these automata are consistent, where we propose to set up a suitable simulation relation. The proposed techniques are illustrated with a small case study.