A trace-based model for multiparty contracts

TY - GEN

T1 - A trace-based model for multiparty contracts

AU - Hvitved, Tom

AU - Klaedtke, Felix

AU - Zălinescu, Eugen

N1 - Conference code: 4

PY - 2012/2

Y1 - 2012/2

N2 - In this article we present a model for multiparty contracts in which contract conformance is defined abstractly as a property on traces. A key feature of our model is blame assignment, which means that for a given contract, every breach is attributed to a set of parties. We show that blame assignment is compositional by defining contract conjunction and contract disjunction. Moreover, to specify real-world contracts, we introduce the contract specification language CSL with an operational semantics. We show that each CSL contract has a counterpart in our trace-based model and from the operational semantics we derive a run-time monitor. CSL overcomes limitations of previously proposed formalisms for specifying contracts by supporting: (history sensitive and conditional) commitments, parametrised contract templates, relative and absolute temporal constraints, potentially infinite contracts, and in-place arithmetic expressions. Finally, we illustrate the general applicability of CSL by formalising in CSL various contracts from different domains.

AB - In this article we present a model for multiparty contracts in which contract conformance is defined abstractly as a property on traces. A key feature of our model is blame assignment, which means that for a given contract, every breach is attributed to a set of parties. We show that blame assignment is compositional by defining contract conjunction and contract disjunction. Moreover, to specify real-world contracts, we introduce the contract specification language CSL with an operational semantics. We show that each CSL contract has a counterpart in our trace-based model and from the operational semantics we derive a run-time monitor. CSL overcomes limitations of previously proposed formalisms for specifying contracts by supporting: (history sensitive and conditional) commitments, parametrised contract templates, relative and absolute temporal constraints, potentially infinite contracts, and in-place arithmetic expressions. Finally, we illustrate the general applicability of CSL by formalising in CSL various contracts from different domains.

U2 - 10.1016/j.jlap.2011.04.010

DO - 10.1016/j.jlap.2011.04.010

M3 - Conference article

SN - 2352-2208

VL - 81

SP - 72

EP - 98

JO - Journal of Logic and Algebraic Programming

JF - Journal of Logic and Algebraic Programming

IS - 2

T2 - 4th Workshop on Formal Languages and Analysis of Contract-Oriented Software

Y2 - 17 September 2010 through 18 September 2010

ER -