Abstract: An important issue, in open environments like the web, is guaranteeing the interoperability of a set of services. When the interaction scheme that the services should follow is given (e.g. as a choreography or as an interaction protocol), it becomes possible to verify, before the interaction takes place, if the interactive behavior of a service (e.g. a BPEL process specification) respects it. This verification is known as 'conformance test'. Recently some attempts have been done for defining conformance tests w.r.t. a protocol but these approaches fail in capturing the very nature of interoperability, turning out to be too restrictive. In this work we give a representation of protocol, based on message exchange and on finite state automata, and we focus on those properties that are essential to the verification of the interoperability of a set of services. In particular, we define a conformance test that can guarantee, a priori, the interoperability of a set of services by verifying properties of the single service against the protocol. This is particularly relevant in open environments, where services are identified and composed on demand and dynamically, and the system as a whole cannot be analyzed.

This research has partially been funded by the European Commission and by the Swiss Federal Office for Education and Science within the 6th Framework Programme project REWERSE number 506779 (cf. http://rewerse.net), and it has also been supported by MIUR PRIN 2005 'Specification and verification of agent interaction protocols' national project.

Short Bio: Matteo Baldoni was born in Torino in 1968. He took his ``Laurea'' degree ``summa cum laude'' in Computer Science in February 1993 and his Ph.D. in Computer Science in May 1998, both at the University of Turin, Italy. Currently he is associate professor at the Department of Computer Science, Universita degli Studi di Torino where he is member of the Logic Programming & Automatic Reasoning group. From July 1999 through September 2006 he was a researcher at the Department of Computer Science, Universita degli Studi di Torino. From February through October 1998 he has been visiting the Laboratoire d'Informatique de Marseille (LIM) where he worked in the group of 'Representation et traiement logique des connaissances' under the supervision of Camilla Schwind.

He has a background in computational logic, modal and nonmonotonic extensions of logic programming, multimodal logics, reasoning by actions and change. His current research interests include issues in communication protocol design and implementation, conformance and interoperabilty for agents and web services, agent programming languages, and personalization by reasoning in the semantic web.