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 条
  • [1] SYMBOLEOPC: checking properties of legal contracts
    Parvizimosaed, Alireza
    Roveri, Marco
    Rasti, Aidin
    Anda, Amal Ahmed
    Alfuhaid, Sofana
    Amyot, Daniel
    Logrippo, Luigi
    Mylopoulos, John
    SOFTWARE AND SYSTEMS MODELING, 2024,
  • [2] Model-Checking of Smart Contracts
    Nehai, Zeinab
    Piriou, Pierre-Yves
    Daumas, Frederic
    IEEE 2018 INTERNATIONAL CONGRESS ON CYBERMATICS / 2018 IEEE CONFERENCES ON INTERNET OF THINGS, GREEN COMPUTING AND COMMUNICATIONS, CYBER, PHYSICAL AND SOCIAL COMPUTING, SMART DATA, BLOCKCHAIN, COMPUTER AND INFORMATION TECHNOLOGY, 2018, : 980 - 987
  • [3] The model-checking kit
    Schröter, C
    Schwoon, S
    Esparza, J
    APPLICATIONS AND THEORY OF PETRI NETS 2003, PROCEEDINGS, 2003, 2679 : 463 - 472
  • [4] QLTL Model-Checking
    Laroussinie, Francois
    Leclercq, Loriane
    Sangnier, Arnaud
    32ND EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC, CSL 2024, 2024, 288
  • [5] Model-checking quantum systems
    Mingsheng Ying
    Yuan Feng
    National Science Review, 2019, 6 (01) : 28 - 31
  • [6] Model-Checking Parse Trees
    Boral, Anudhyan
    Schmitz, Sylvain
    2013 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2013, : 153 - 162
  • [7] Model-checking quantum systems
    Ying, Mingsheng
    Feng, Yuan
    NATIONAL SCIENCE REVIEW, 2019, 6 (01) : 28 - 31
  • [8] Talking model-checking technology
    Hoffman, Leah
    COMMUNICATIONS OF THE ACM, 2008, 51 (07) : 112 - 111
  • [9] Model-checking process equivalences
    Lange, Martin
    Lozes, Etienne
    Guzman, Manuel Vargas
    THEORETICAL COMPUTER SCIENCE, 2014, 560 : 326 - 347
  • [10] Model-Checking Iterated Games
    Huang, Chung-Hao
    Schewe, Sven
    Wang, Farn
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 154 - 168
12345