Verifying the Smart Contracts of the Port Supply Chain System Based on Probabilistic Model Checking

Abstract

Port supply chains play a very important role in the process of economic globalization. Lack of trust of the mechanism is the main factor in restricting the development of port supply chains. Blockchains have great potential to solve the trust problem among all participants using port supply chains, which can reduce costs and improve efficiency. As the bridge between blockchains and port supply chains, smart contracts reconstruct the business process of blockchain‐empowered port supply chains. In this article, we present an architecture of a consortium blockchain‐empow-ered port supply chain system, and propose a system verification framework for the smart contracts of port supply chains with probabilistic behaviors. The smart contracts are modeled as DTMCs (Dis-crete‐Time Markov Chains), which are automatically transformed through the BPMN (Business Process Model and Notation) description of the smart contracts. The requirements are specified by PCTL (Probabilistic Computation Tree Logic). Moreover, we implement the customs clearance process of the Shanghai Yangshan Port based on blockchain Hyperledger Fabric, and reconstruct the clearance process with smart contracts. We use it to demonstrate the effectiveness of this framework, and identify the smart contracts that do not meet the expected needs of users.