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] On Model-Checking Higher-Order Effectful Programs
    Dal Lago, Ugo
    Ghyselen, Alexis
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (POPL):
  • [22] 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
  • [23] Model-checking Timed Temporal Logics
    Bouyer, Patricia
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 323 - 341
  • [24] Model-Checking Structured Context-Free Languages
    Chiari, Michele
    Mandrioli, Dino
    Pradella, Matteo
    COMPUTER AIDED VERIFICATION, PT II, CAV 2021, 2021, 12760 : 387 - 410
  • [25] On the use of Probabilistic Model-Checking for the Verification of Prognostics Applications
    Aizpurua, Jose Ignacio
    Catterson, Victoria M.
    2015 IEEE SEVENTH INTERNATIONAL CONFERENCE ON INTELLIGENT COMPUTING AND INFORMATION SYSTEMS (ICICIS), 2015, : 7 - +
  • [26] Model-checking software library API usage rules
    Song, Fu
    Touili, Tayssir
    SOFTWARE AND SYSTEMS MODELING, 2016, 15 (04) : 961 - 985
  • [27] Model-checking based data retrieval
    Dovier, A
    Quintarelli, E
    DATABASE PROGRAMMING LANGUAGES, 2002, 2397 : 62 - 77
  • [28] A Model-Checking Tool for Families of Services
    Asirelli, Patrizia
    ter Beek, Maurice H.
    Fantechi, Alessandro
    Gnesi, Stefania
    FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, 2011, 6722 : 44 - 58
  • [29] Model-checking TRIO specifications in SPIN
    Morzenti, A
    Pradella, M
    San Pietro, P
    Spoletini, P
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 542 - 561
  • [30] Direct Model-checking of SysML Models
    Calvino, Alessandro Tempia
    Apvrille, Ludovic
    PROCEEDINGS OF THE 9TH INTERNATIONAL CONFERENCE ON MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT (MODELSWARD), 2021, : 216 - 223
12345