Automata for Analysing Service Contracts