Copyright
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-9017
URL: http://drops.dagstuhl.de/opus/volltexte/2007/901/
Alberti, Marco ; Chesani, Federico ; Gavanelli, Marco ; Lamma, Evelina ; Mello, Paola ; Montali, Marco ; Torroni, Paolo

Expressing and Verifying Business Contracts with Abductive

pdf-format:
Dokument 1.pdf (398 KB)

Abstract

In this article, we propose to adopt the SCIFF abductive logic language to specify business contracts, and show how its proof procedures are useful to verify contract execution and fulfilment. SCIFF is a declarative language based on abductive logic programming, which accommodates forward rules, predicate definitions, and constraints over finite domain variables. Its declarative semantics is abductive, and can be related to that of deontic operators; its operational specification is the sound and complete SCIFF proof procedure, defined as a set of transition rules, which has been implemented and integrated into a reasoning and verification tool. A variation of the SCIFF proof-procedure (g-SCIFF) can be used for static verification of contract properties. We demonstrate the use of the SCIFF language for business contract specification and verification, in a concrete scenario. In order to accommodate integration of SCIFF with architectures for business contract, we also propose an encoding of SCIFF contract rules in RuleML.

BibTeX - Entry

@InProceedings{alberti_et_al:DSP:2007:901,
  author =	{Marco Alberti and Federico Chesani and Marco Gavanelli and Evelina Lamma and Paola Mello and Marco Montali and Paolo Torroni},
  title =	{Expressing and Verifying Business Contracts with Abductive},
  booktitle =	{Normative Multi-agent Systems},
  year =	{2007},
  editor =	{Guido Boella and Leon van der Torre and Harko Verhagen },
  number =	{07122},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2007/901},
  annote =	{Keywords: Contracts, Verification, Abduction}
}

Keywords: Contracts, Verification, Abduction
Seminar: 07122 - Normative Multi-agent Systems
Documenttype: InProceedings
Issue date: 2007
Date of publication: 12.03.2007

DROPS-Home | Fulltext Search | Imprint Published by LZI