Maritime transportation business suffers from trust issues and burdensome paperwork. Blockchain-based smart contracts are a promising solution. Due to the nature of the blockchain, it is important to verify smart contracts before deployment, especially for its functionality and legality. In this paper, we propose a verification framework that automatically verifies the functionality and legality requirements of maritime transportation smart contracts. Smart contracts of an application, based on a set of templates, are modeled in a network of timed automata; domain-specific requirements are collected and formulated as temporal logic formulas; real-time model checking tool UPPAAL is then used to check whether these requirements are satisfied. We carry out experiments on nine real-world smart contracts to show the effectiveness and feasibility of our framework. We also compare our work with existing tools to show its effectiveness and efficiency.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Template-Based Smart Contract Verification: A Case Study on Maritime Transportation Domain

  • Xufeng Zhao,
  • Qiuyang Wei,
  • Xue-Yang Zhu,
  • Wenhui Zhang

摘要

Maritime transportation business suffers from trust issues and burdensome paperwork. Blockchain-based smart contracts are a promising solution. Due to the nature of the blockchain, it is important to verify smart contracts before deployment, especially for its functionality and legality. In this paper, we propose a verification framework that automatically verifies the functionality and legality requirements of maritime transportation smart contracts. Smart contracts of an application, based on a set of templates, are modeled in a network of timed automata; domain-specific requirements are collected and formulated as temporal logic formulas; real-time model checking tool UPPAAL is then used to check whether these requirements are satisfied. We carry out experiments on nine real-world smart contracts to show the effectiveness and feasibility of our framework. We also compare our work with existing tools to show its effectiveness and efficiency.