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 条
  • [31] Model-checking TRIO specifications in SPIN
    Morzenti, A
    Pradella, M
    San Pietro, P
    Spoletini, P
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 542 - 561
  • [32] Model-checking access control policies
    Guelev, DP
    Ryan, M
    Schobbens, PY
    INFORMATION SECURITY, PROCEEDINGS, 2004, 3225 : 219 - 230
  • [33] On complexity of model-checking for the TQL logic
    Boneva, I
    Talbot, JM
    EXPLORING NEW FRONTIERS OF THEORETICAL INFORMATICS, 2004, 155 : 381 - 394
  • [34] 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
  • [35] QCTL model-checking with QBF solvers
    Hossain, Akash
    Laroussinie, Francois
    INFORMATION AND COMPUTATION, 2021, 280
  • [36] Systematic construction of abstractions for model-checking
    Gurfinkel, A
    Wei, O
    Chechik, M
    VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2006, 3855 : 381 - 397
  • [37] Model-checking trace event structures
    Madhusudan, P
    18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, : 371 - 380
  • [38] Model-checking based data retrieval
    Dovier, A
    Quintarelli, E
    DATABASE PROGRAMMING LANGUAGES, 2002, 2397 : 62 - 77
  • [39] Practical model-checking using games
    Stevens, P
    Stirling, C
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 : 85 - 101
  • [40] 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
12345