Research On The Formalization Of Smart Contract For Supply Chain Management

Supply chain is an industrial application system that centers around core producers and establishes contact with suppliers,sellers,transporters and other main bodies by controlling information flow,logistics and capital flow.There are complex business interactions in the system.Emerging blockchain technology has decentralization,tamper-proof and traceable characteristics,providing a new way to solve the problems of complex information sharing and difficult business collaboration faced by traditional supply chain applications.Blockchain technology is the underlying technology that integrates multiple technologies such as consensus mechanism,distributed storage,and smart contracts.In recent years,serious consequences had been caused by factors such as functional defects of smart contracts and immutability on the chain,obstructing the popularization and application of blockchain technology.Ensuring the security and reliability of smart contracts is critical to the industrial application of blockchain technology.Based on the blockchain supply chain application,the thesis designs a smart contract to support the supply chain business interaction.On the basis of completing the verification of contract functionality using conventional testing methods,a formal modeling and detection method for smart contracts is proposed to verify the functional completeness and logical correctness of the contracts.The main research work is as follows:(1)A smart contract for supply chain business is designed to create the object for formal research work.Firstly,the role positioning of four types of supply chain participants: suppliers,producers,sellers and transporters,as well as the interaction scenarios of procurement,sales and transportation among the participants are analyzed.Secondly,the corresponding functional requirements for supply chain related businesses are analyzed to summarize the functional functions that the smart contract should possess in each stage of the business and the constraints for contract execution.Finally,based on Solidity language,the supply chain business smart contract is designed and implemented.(2)A blockchain industry application platform is built,on which the functionality of the smart contract is verified using conventional testing methods in contrast to the formal verification of the functional completeness of smart contracts below.Firstly,based on FISCO BCOS platform,an alliance chain network environment is built,and a middleware platform is deployed to provide a visual test operation interface.Secondly,on the middleware platform,the supply chain business smart contract is compiled and deployed to the blockchain.Finally,test cases are designed based on supply chain business requirements to test the implementation of contract functions.(3)UPPAAL,a model detection tool suitable for verifying real-time systems,is selected to study the formal modeling method of smart contracts and formally verify the smart contract of supply chain business.By adopting a formal modeling approach that distinguishes between business operations and business states,the smart contract is modeled as user automata and entity automata,and a modeling framework for Solidity contract language is proposed.Based on this modeling method,the supply chain smart contract is first modeled as a time automaton network model.Then,classified from accessibility,security and activity,the specifications and attributes of the smart contract for supply chain business are defined,and formally verified and analyzed.Finally,in order to address issues such as state space explosion that may arise during the formal verification process,the thesis optimizes them by changing the verification method of model detection.