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 条
  • [41] On model-checking timed automata with stopwatch observers
    Brihaye, T
    Bruyére, V
    Raskin, JFO
    INFORMATION AND COMPUTATION, 2006, 204 (03) : 408 - 433
  • [42] Model-checking for validation of a Fault Protection system
    Feather, MS
    Fickas, S
    Razermera-Mamy, NA
    SIXTH IEEE INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING, 2001, : 32 - 41
  • [43] Decomposition Theorems and Model-Checking for the Modal μ-Calculus
    Bojanczyk, Mikolaj
    Dittmann, Christoph
    Kreutzer, Stephan
    PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2014,
  • [44] Efficient CTL model-checking for pushdown systems
    Song, Fu
    Touili, Tayssir
    THEORETICAL COMPUTER SCIENCE, 2014, 549 : 127 - 145
  • [45] Model-checking Distributed Components: The Vercors Platform
    Barros, Tomas
    Cansado, Antonio
    Madelaine, Eric
    Rivera, Marcela
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 182 : 3 - 16
  • [46] Model-Checking the Linux Virtual File System
    Galloway, Andy
    Luettgen, Gerald
    Muehlberg, Jan Tobias
    Siminiceanu, Radu I.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2009, 5403 : 74 - +
  • [47] Model-checking the Flooding Time Synchronization Protocol
    McInnes, Allan I.
    2009 IEEE INTERNATIONAL CONFERENCE ON CONTROL AND AUTOMATION, VOLS 1-3, 2009, : 422 - 429
  • [48] TAGED Approximations for Temporal Properties Model-Checking
    Courbis, Romeo
    Heam, Pierre-Cyrille
    Kouchnarenko, Olga
    IMPLEMENTATION AND APPLICATION OF AUTOMATA, PROCEEDINGS, 2009, 5642 : 135 - 144
  • [49] Reasoning About Strategies: On the Model-Checking Problem
    Mogavero, Fabio
    Murano, Aniello
    Perelli, Giuseppe
    Vardi, Moshe Y.
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (04)
  • [50] Compositional model-checking verification of critical systems
    Mendoza, Luis E.
    Capel, Manuel I.
    Pérez, María
    Benghazi, Kawtar
    Lecture Notes in Business Information Processing, 2009, 19 : 213 - 225
12345