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] Model-Checking with Coverability Graphs
Karsten Schmidt
Formal Methods in System Design, 1999, 15 : 239 - 254
[22] Model-checking iterated games
Huang, Chung-Hao
Schewe, Sven
Wang, Farn
ACTA INFORMATICA, 2017, 54 (07) : 625 - 654
[23] Model-Checking Process Equivalences
Lange, Martin
Lozes, Etienne
Guzman, Manuel Vargas
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (96): : 43 - 56
[24] Model-checking hierarchical structures
Lohrey, Markus
JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2012, 78 (02) : 461 - 490
[25] Verifying Business Rules Using Model-Checking Techniques for Non-specialist in Model-Checking
Aoki, Yoshitaka
Matsuura, Saeko
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2014, E97D (05) : 1097 - 1108
[26] Model-checking Timed Temporal Logics
Bouyer, Patricia
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 323 - 341
[27] Model-Checking HyperLTL for Pushdown Systems
Pommellet, Adrien
Touili, Tayssir
MODEL CHECKING SOFTWARE, SPIN 2018, 2018, 10869 : 133 - 152
[28] 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
[29] Foundations of incremental aspect model-checking
Krishnamurthi, Shriram
Fisler, Kathi
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (02)
[30] Connectivity testing through model-checking
Godskesen, JC
Nielsen, B
Skou, A
FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2004, PROCEEDINGS, 2004, 3235 : 167 - 184

← 1 2 3 4 5 →