Specification and analysis of legal contracts with Symboleo

被引：7
作者：
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 条
  • [1] Expressing and verifying business contracts with abductive logic programming
    Alberti, Marco
    Chesani, Federico
    Gavanelli, Marco
    Lamma, Evelina
    Mello, Paola
    Montali, Marco
    Torroni, Paolo
    [J]. INTERNATIONAL JOURNAL OF ELECTRONIC COMMERCE, 2008, 12 (04) : 9 - 38
  • [2] Allard MP., 2001, CAN TAX J, V49, P1726
  • [3] TOWARDS A GENERAL-THEORY OF ACTION AND TIME
    ALLEN, JF
    [J]. ARTIFICIAL INTELLIGENCE, 1984, 23 (02) : 123 - 154
  • [4] Alqahtani S., 2020, HAWAII INT C SYSTEM
  • [5] Alt Leonardo, 2018, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. 8th International Symposium, ISoLA 2018. Proceedings: Lecture Notes in Computer Science (LNCS 11247), P376, DOI 10.1007/978-3-030-03427-6_28
  • [6] Alt L., 2020, ETHEREUM FORMAL VERI
  • [7] [Anonymous], 1987, Foundations of Logic Programming
  • [8] [Anonymous], 2020, ERG
  • [9] Athan T, 2013, P 14 INT C ART INT L, P3, DOI DOI 10.1145/2514601.2514603
  • [10] LegalRuleML: Design Principles and Foundations
    Athan, Tara
    Governatori, Guido
    Palmirani, Monica
    Paschke, Adrian
    Wyner, Adam
    [J]. REASONING WEB: WEB LOGIC RULES, 2015, 9203 : 151 - 188
123456789