Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Alberti, Marco; Chesani, Federico; Gavanelli, Marco; Lamma, Evelina; Mello, Paola; Montali, Marco; Torroni, Paolo License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-9017

; ; ; ; ; ;

Expressing and Verifying Business Contracts with Abductive



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

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

BibTeX - Entry

  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 =		{},
  URN =		{urn:nbn:de:0030-drops-9017},
  doi =		{10.4230/DagSemProc.07122.15},
  annote =	{Keywords: Contracts, Verification, Abduction}

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

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