Specification and analysis of legal contracts with Symboleo

被引：9

作者：

Parvizimosaed, Alireza ^{[1
]}

Sharifi, Sepehr ^{[1
]}

Amyot, Daniel ^{[1
]}

Logrippo, Luigi ^{[1
,2
]}

Roveri, Marco ^{[3
]}

Rasti, Aidin ^{[1
]}

Roudak, Ali ^{[4
]}

Mylopoulos, John ^{[1
]}

机构：

[1] Univ Ottawa, Sch EECS, Ottawa, ON, Canada

[2] Univ Quebec Outaouais, Gatineau, PQ, Canada

[3] Univ Trento, Dept Informat Engn & Comp Sci, Trento, Italy

[4] Univ Duisburg Essen, Duisburg, Germany

来源：

SOFTWARE AND SYSTEMS MODELING | 2022年 / 21卷 / 06期

基金：

加拿大自然科学与工程研究理事会;

关键词：

Legal contracts; Software requirements specifications; Formal specification languages; Model checking; nuXmv; Smart contracts; BUSINESS CONTRACTS; FORMAL ANALYSIS; TEMPORAL LOGIC; REQUIREMENTS; COMMITMENTS; BLOCKCHAIN;

D O I：

10.1007/s10270-022-01053-6

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Legal contracts specify the terms and conditions-in essence, requirements-that apply to business transactions. This paper proposes a formal specification language for legal contracts, called Symboleo, where contracts consist of collections of obligations and powers that define a legal contract's compliant executions. Symboleo offers execution time operations such as subcontracting, assignment, and substitution. Its formal semantics is defined in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations, and powers. We have implemented two tools to support the analysis of contract specifications. One is a conformance validation tool that enables checking that a specification is consistent with the expectations of contracting parties. The other tool enables model-checking of desired contract properties, expressed in temporal logic. We envision Symboleo with its associated tools as enablers for the formal verification of contracts to detect requirements-level issues. Our proposal includes an evaluation through the specification of two real life-inspired contracts.

引用

页码：2395 / 2427

页数：33

共 90 条

[31] Formal Specification and Automatic Verification of Conditional Commitments [J].