Template-Based Smart Contract Verification: A Case Study on Maritime Transportation Domain
摘要
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.