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] Understanding SIP through Model-Checking
    Zave, Pamela
    PRINCIPLES, SYSTEMS AND APPLICATIONS OF IP TELECOMMUNICATIONS, 2008, 5310 : 256 - 279
  • [42] Testing and model-checking techniques for diagnosis
    Gromov, Maxim
    Willemse, Tim A. C.
    TESTING OF SOFTWARE AND COMMUNICATING SYSTEMS, PROCEEDINGS, 2007, 4581 : 138 - +
  • [43] Symbolic model-checking for biochemical systems
    Fages, F
    LOGIC PROGRAMMING, PROCEEDINGS, 2003, 2916 : 102 - 102
  • [44] LTL Model-Checking for Malware Detection
    Song, Fu
    Touili, Tayssir
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 416 - 431
  • [45] Towards Model-Checking Programs with Lists
    Finkel, Alain
    Lozes, Etienne
    Sangnier, Arnaud
    INFINITY IN LOGIC AND COMPUTATION, 2009, 5489 : 56 - 86
  • [46] Probabilistic model-checking support for FMEA
    Grunske, Lars
    Colvin, Robert
    Winter, Kirsten
    FOURTH INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, 2007, : 119 - +
  • [47] Log auditing through model-checking
    Roger, M
    Goubault-Larrecq, J
    14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, : 220 - 234
  • [48] A logic of probability with decidable model-checking
    Beauquier, D
    Rabinovich, A
    Slissenko, A
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2002, 2471 : 306 - 321
  • [49] Model-checking in simulations of distribution systems
    Geilen, M
    SIMULATION IN INDUSTRY'2000, 2000, : 606 - 611
  • [50] Model-Checking HELENA Ensembles with Spin
    Hennicker, Rolf
    Klarl, Annabelle
    Wirsing, Martin
    LOGIC, REWRITING, AND CONCURRENCY, 2015, 9200 : 331 - 360
12345