Although stemming from very different research areas, Multi-Agent Systems (MAS) and Service Oriented Computing (SOC) share common topics, problems and settings. One of the common problems is the need to formally verify the conformance of individuals (Agents or Web Services) to common rules and specifications (resp. Protocols/Choreographies), in order to provide a coherent behaviour and to reach the goals of the user. In previous publications, we developed a framework, SCIFF, for the automatic verification of compliance of agents to protocols. The framework includes a language based on abductive logic programming and on constraint logic programming for formally defining the social rules; suitable proof-procedures to check on-the-fly and a-priori the compliance of agents to protocols have been defined. Building on our experience in the MAS area, in this paper we make a first step towards the formal verification of web services conformance to choreographies. We adapt the SCIFF framework for the new settings, and propose a heir of SCIFF, the framework ALLoWS (Abductive Logic Web-service Specification). ALLoWS comes with a language for defining formally a choreography and a web service specification. As its ancestor, ALLoWS has a declarative and an operational semantics. We show examples of how ALLoWS deals correctly with interaction patterns previously identified. Moreover, thanks to its constraint-based semantics, ALLoWS deals seamlessly with other cases involving constraints and deadlines.

An Abductive Framework for A-Priori Verification of Web Services

CHESANI, FEDERICO;MELLO, PAOLA;MONTALI, MARCO
2006

Abstract

Although stemming from very different research areas, Multi-Agent Systems (MAS) and Service Oriented Computing (SOC) share common topics, problems and settings. One of the common problems is the need to formally verify the conformance of individuals (Agents or Web Services) to common rules and specifications (resp. Protocols/Choreographies), in order to provide a coherent behaviour and to reach the goals of the user. In previous publications, we developed a framework, SCIFF, for the automatic verification of compliance of agents to protocols. The framework includes a language based on abductive logic programming and on constraint logic programming for formally defining the social rules; suitable proof-procedures to check on-the-fly and a-priori the compliance of agents to protocols have been defined. Building on our experience in the MAS area, in this paper we make a first step towards the formal verification of web services conformance to choreographies. We adapt the SCIFF framework for the new settings, and propose a heir of SCIFF, the framework ALLoWS (Abductive Logic Web-service Specification). ALLoWS comes with a language for defining formally a choreography and a web service specification. As its ancestor, ALLoWS has a declarative and an operational semantics. We show examples of how ALLoWS deals correctly with interaction patterns previously identified. Moreover, thanks to its constraint-based semantics, ALLoWS deals seamlessly with other cases involving constraints and deadlines.
2006
Proceedings of the Eighth Symposium on Principles and Practice of Declarative Programming, July 10-12, 2006, Venice, Italy
39
50
M. Alberti; F. Chesani; M. Gavanelli; E. Lamma; P. Mello; M. Montali
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/29944
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 29
  • ???jsp.display-item.citation.isi??? ND
social impact