Expressing and Verifying Business Contracts with Abductive Logic Programming
Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali, and Paolo Torroni
International Journal of Electronic Commerce,
Volume 12, Number 4, Summer 2008, pp. 9.
Abstract: SCIFF is a declarative language, based on abductive logic programming, that accommodates forward rules, predicate definitions, and constraints over finite domain variables. Its abductive declarative semantics 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 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. The use of SCIFF for business contract specification and verification is demonstrated in a concrete scenario. En-coding of SCIFF contract rules in RuleML accommodates integration of SCIFF with architectures for business contracts.
Key Words and Phrases: Abductive logic programming, business contracts, declarative specifications, g-SCIFF, SCIFF, runtime verification, static verification.