License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.07122.15
URN: urn:nbn:de:0030-drops-9017
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2007/901/
Go to the corresponding Portal

Alberti, Marco ; Chesani, Federico ; Gavanelli, Marco ; Lamma, Evelina ; Mello, Paola ; Montali, Marco ; Torroni, Paolo

Expressing and Verifying Business Contracts with Abductive

pdf-format:
07122.AlbertiMarco.Paper.901.pdf (0.4 MB)

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:DagSemProc.07122.15,
  author =	{Alberti, Marco and Chesani, Federico and Gavanelli, Marco and Lamma, Evelina and Mello, Paola and Montali, Marco and Torroni, Paolo},
  title =	{{Expressing and Verifying Business Contracts with Abductive}},
  booktitle =	{Normative Multi-agent Systems},
  pages =	{1--29},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7122},
  editor =	{Guido Boella and Leon van der Torre and Harko Verhagen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2007/901},
  URN =		{urn:nbn:de:0030-drops-9017},
  doi =		{10.4230/DagSemProc.07122.15},
  annote =	{Keywords: Contracts, Verification, Abduction}
}

Keywords: Contracts, Verification, Abduction
Collection: 07122 - Normative Multi-agent Systems
Issue Date: 2007
Date of publication: 12.03.2007

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI