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 条
  • [31] Reducing model checking commitments for agent communication to model checking ARCTL and GCTL
    El Menshawy, Mohamed
    Bentahar, Jamal
    El Kholy, Warda
    Dssouli, Rachida
    [J]. AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, 2013, 27 (03) : 375 - 418
  • [32] El-Menshawy Mohamed., 2011, P 10 INT C AUTONOMOU, P483
  • [33] USING BRANCHING TIME TEMPORAL LOGIC TO SYNTHESIZE SYNCHRONIZATION SKELETONS
    EMERSON, EA
    CLARKE, EM
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 1982, 2 (03) : 241 - 266
  • [34] A Calculus Supporting Contract Reasoning and Monitoring
    Emilia Cambronero, Maria
    Llana, Luis
    Pace, Gordon J.
    [J]. IEEE ACCESS, 2017, 5 : 6735 - 6745
  • [35] Ethereum Foundation, 2020, SOL
  • [36] Farmer W.M., 2016, 4 IEEE INT WORKSHOP, P190
  • [37] Farrell ADH, 2004, FIRST IEEE INTERNATIONAL WORKSHOP ON ELECTRONIC CONTRACTING, PROCEEDINGS, P17
  • [38] Specifying and analyzing early requirements in Tropos
    Fuxman, A
    Liu, L
    Mylopoulos, J
    Pistore, M
    Roveri, M
    Traverso, P
    [J]. REQUIREMENTS ENGINEERING, 2004, 9 (02) : 132 - 150
  • [39] Goedertier S, 2006, LECT NOTES COMPUT SC, V4103, P5
  • [40] Dealing with contract violations: formalism and domain specific language
    Governatori, G
    Milosevic, Z
    [J]. Ninth IEEE International EDOC Enterprise Computing Conference, Proceedings, 2005, : 46 - 57
123456789