Model-Checking Legal Contracts with SymboleoPC

被引：3
作者：
Parvizimosaed, Alireza [1 ]
Roveri, Marco [2 ]
Rasti, Aidin [1 ]
Amyot, Daniel [1 ]
Logrippo, Luigi [3 ]
Mylopoulos, John [1 ]
机构：
[1] Univ Ottawa, Ottawa, ON, Canada
[2] Univ Trento, Trento, Italy
[3] Univ Quebec Outaouais, Gatineau, PQ, Canada
来源：
PROCEEDINGS OF THE 25TH INTERNATIONAL ACM/IEEE CONFERENCE ON MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, MODELS 2022 | 2022年
关键词：
Legal contracts; smart contracts; software requirements specifications; formal specification languages; model checking; performance analysis; nuXmv; LOGIC; VERIFICATION; CHALLENGES;
D O I：
10.1145/3550355.3552449
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Legal contracts specify requirements for business transactions. As any other requirements specification, contracts may contain errors and violate properties expected by contracting parties. Symboleo was recently proposed as a formal specification language for legal contracts. This paper presents SymboleoPC, a tool for analyzing Symboleo contracts using model checking. It highlights the architecture, implementation and testing of the tool, as well as a scalability evaluation with respect to the size of contracts and properties to be checked through a series of experiments. The results suggest that SymboleoPC can be usefully applied to the analysis of formal specifications of contracts with real-life sizes and structures.
引用
收藏
页码：278 / 288
页数：11
相关论文
共 50 条
  • [31] Model-checking temporal behaviour in CSP
    Ouaknine, J
    Reed, GM
    INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, PROCEEDINGS, 1999, : 295 - 304
  • [32] QCTL model-checking with QBF solvers
    Hossain, Akash
    Laroussinie, Francois
    INFORMATION AND COMPUTATION, 2021, 280
  • [33] Model checking smart contracts for Ethereum
    Osterland, Thomas
    Rose, Thomas
    PERVASIVE AND MOBILE COMPUTING, 2020, 63
  • [34] Model-checking Synthesizable System Verilog Descriptions of Asynchronous Circuits
    Bouzafour, Aymane
    Renaudin, Marc
    Garavel, Hubert
    Mateescu, Radu
    Serwe, Wendelin
    2018 24TH IEEE INTERNATIONAL SYMPOSIUM ON ASYNCHRONOUS CIRCUITS AND SYSTEMS (ASYNC), 2018, : 34 - 42
  • [35] Introducing time in an industrial application of model-checking
    van den Berg, Lionel
    Strooper, Paul
    Winter, Kirsten
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2008, 4916 : 56 - 67
  • [36] Model-Checking Linear-Time Properties of Quantum Systems
    Ying, Mingsheng
    Li, Yangjia
    Yu, Nengkun
    Feng, Yuan
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (03)
  • [37] Model-checking Driven Design of Interactive Systems
    Cerone, Antonio
    Elbegbayan, Norzima
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 183 : 3 - 20
  • [38] A model-checking verification environment for mobile processes
    Ferrari, GL
    Gnesi, S
    Montanari, U
    Pistore, M
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2003, 12 (04) : 440 - 473
  • [39] Model-Checking Behavioral Specification of BPEL Applications
    Nakajima, Shin
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 151 (02) : 89 - 105
  • [40] Weighted Timed Automata: Model-Checking and Games
    Bouyer, Patricia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 158 (01) : 3 - 17
12345