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 条
  • [21] Validation of Requirements for Hybrid Systems: a Formal Approach
    Cimatti, Alessandro
    Roveri, Marco
    Susi, Angelo
    Tonetta, Stefano
    [J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2012, 21 (04)
  • [22] Cook S, 2017, UNIFIED MODELING LAN
  • [23] CSM Lab, 2020, SYMB CONF CHECK
  • [24] CSM Lab and University of Trento, 2020, SYMB PROP CHECK NUXM
  • [25] GOAL-DIRECTED REQUIREMENTS ACQUISITION
    DARDENNE, A
    VANLAMSWEERDE, A
    FICKAS, S
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 1993, 20 (1-2) : 3 - 50
  • [26] Modelling legal contracts as processes
    Daskalopulu, A
    [J]. 11TH INTERNATIONAL WORKSHOP ON DATABASE AND EXPERT SYSTEMS APPLICATION, PROCEEDINGS, 2000, : 1074 - 1079
  • [27] Daskalopulu A.K., 1999, THESIS
  • [28] Digital Asset Holdings, 2020, DAML
  • [29] Dwyer M. B., 1999, Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), P411, DOI 10.1109/ICSE.1999.841031
  • [30] Formal Specification and Automatic Verification of Conditional Commitments
    El Kholy, Warda
    El Menshawy, Mohamed
    Bentahar, Jamal
    Qu, Hongyang
    Dssouli, Rachida
    [J]. IEEE INTELLIGENT SYSTEMS, 2015, 30 (02) : 36 - 44
123456789