Model checking contracts - A case study

被引：0
|
作者：
Pace, Gordon [1 ]
Prisacariu, Cristian [2 ]
Schneider, Gerardo [2 ]
机构：
[1] Univ Malta, Dept Comp Sci & AI, Msida, Malta
[2] Univ Oslo, Dept Informat, N-0316 Oslo, Norway
来源：
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS | 2007年 / 4762卷
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Contracts are agreements between distinct parties that determine rights and obligations on their signatories, and have been introduced in order to reduce risks and to regulate inter-business relationships. In this paper we show how a conventional contract can be written in the contract language CL, model the contract and verify properties of the model using the NuSMV model checking tool.
引用
收藏
页码：82 / +
页数：3
相关论文
共 50 条
  • [1] Model-Checking of Smart Contracts
    Nehai, Zeinab
    Piriou, Pierre-Yves
    Daumas, Frederic
    [J]. 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
  • [2] Model checking smart contracts for Ethereum
    Osterland, Thomas
    Rose, Thomas
    [J]. PERVASIVE AND MOBILE COMPUTING, 2020, 63
  • [3] Model-Checking Legal Contracts with SymboleoPC
    Parvizimosaed, Alireza
    Roveri, Marco
    Rasti, Aidin
    Amyot, Daniel
    Logrippo, Luigi
    Mylopoulos, John
    [J]. PROCEEDINGS OF THE 25TH INTERNATIONAL ACM/IEEE CONFERENCE ON MODEL DRIVEN ENGINEERING LANGUAGES AND SYSTEMS, MODELS 2022, 2022, : 278 - 288
  • [4] Model checking correctness properties of electronic contracts
    Solaiman, E
    Molina-Jimenez, C
    Shrivastava, S
    [J]. SERVICE-ORIENTED COMPUTING - ICSOC 2003, 2003, 2910 : 303 - 318
  • [5] On Verification of Smart Contracts via Model Checking
    Bao, Yulong
    Zhu, Xue-Yang
    Zhang, Wenhui
    Shen, Wuwei
    Sun, Pengfei
    Zhao, Yingqi
    [J]. THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, TASE 2022, 2022, 13299 : 92 - 112
  • [6] Statically Checking Missing Input Validations in Solidity Smart Contracts - A Case Study
    Munir, Sundas
    Baig, Mirza Samna Iqbal
    Noor, Mali
    Murad, Syeda Nina
    [J]. 2023 IEEE INTERNATIONAL CONFERENCE ON BLOCKCHAIN, BLOCKCHAIN, 2023, : 47 - 54
  • [7] A case study in model checking software systems
    Wing, JM
    VaziriFarahani, M
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 1997, 28 (2-3) : 273 - 299
  • [8] Combination model checking: Approach and a case study
    Choi, YJ
    Heimdahl, MPE
    [J]. 19TH INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2004, : 354 - 357
  • [9] ATL Model Checking for Analysis of Ethereum Smart Contracts
    Nam, Wonhong
    Kil, Hyunyoung
    [J]. Transactions of the Korean Institute of Electrical Engineers, 2021, 70 (12): : 2006 - 2014
  • [10] Scaling up model-checking - A case study
    Kulkarni, Aniket
    Metta, Ravindra
    Shrotri, Ulka
    Venkatesh, R.
    [J]. Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, 2007, : 275 - 283
12345