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 条
  • [21] Model-checking hierarchical structures
    Lohrey, M
    LICS 2005: 20TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE - PROCEEDINGS, 2005, : 168 - 177
  • [22] Model-checking iterated games
    Huang, Chung-Hao
    Schewe, Sven
    Wang, Farn
    ACTA INFORMATICA, 2017, 54 (07) : 625 - 654
  • [23] Model-checking hierarchical structures
    Lohrey, Markus
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2012, 78 (02) : 461 - 490
  • [24] Model-Checking Process Equivalences
    Lange, Martin
    Lozes, Etienne
    Guzman, Manuel Vargas
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (96): : 43 - 56
  • [25] Verifying Business Rules Using Model-Checking Techniques for Non-specialist in Model-Checking
    Aoki, Yoshitaka
    Matsuura, Saeko
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2014, E97D (05) : 1097 - 1108
  • [26] Model-checking Timed Temporal Logics
    Bouyer, Patricia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 323 - 341
  • [27] A tool for model-checking Markov chains
    Holger Hermanns
    Joost-Pieter Katoen
    Joachim Meyer-Kayser
    Markus Siegle
    International Journal on Software Tools for Technology Transfer, 2003, 4 (2) : 153 - 172
  • [28] Model-Checking HyperLTL for Pushdown Systems
    Pommellet, Adrien
    Touili, Tayssir
    MODEL CHECKING SOFTWARE, SPIN 2018, 2018, 10869 : 133 - 152
  • [29] Connectivity testing through model-checking
    Godskesen, JC
    Nielsen, B
    Skou, A
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2004, PROCEEDINGS, 2004, 3235 : 167 - 184
  • [30] Foundations of incremental aspect model-checking
    Krishnamurthi, Shriram
    Fisler, Kathi
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (02)
12345