{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,3]],"date-time":"2026-02-03T17:09:13Z","timestamp":1770138553352,"version":"3.49.0"},"reference-count":44,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2022,2,16]],"date-time":"2022-02-16T00:00:00Z","timestamp":1644969600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Singapore-UK Cyber Security of EPSRC","award":["EP\/N020170\/1"],"award-info":[{"award-number":["EP\/N020170\/1"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems"],"abstract":"<jats:p>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-empowered 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 (Discrete-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.<\/jats:p>","DOI":"10.3390\/systems10010019","type":"journal-article","created":{"date-parts":[[2022,2,16]],"date-time":"2022-02-16T20:28:59Z","timestamp":1645043339000},"page":"19","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Verifying the Smart Contracts of the Port Supply Chain System Based on Probabilistic Model Checking"],"prefix":"10.3390","volume":"10","author":[{"given":"Yang","family":"Liu","sequence":"first","affiliation":[{"name":"Institute of Logistics Science and Engineering, Shanghai Maritime University, Shanghai 200120, China"}]},{"given":"Ziyu","family":"Zhou","sequence":"additional","affiliation":[{"name":"Institute of Logistics Science and Engineering, Shanghai Maritime University, Shanghai 200120, China"}]},{"given":"Yongsheng","family":"Yang","sequence":"additional","affiliation":[{"name":"Institute of Logistics Science and Engineering, Shanghai Maritime University, Shanghai 200120, China"}]},{"given":"Yan","family":"Ma","sequence":"additional","affiliation":[{"name":"School of Accounting, Nanjing University of Finance and Economics, Nanjing 210023, China"},{"name":"School of Computing, National University of Singapore, Singapore 117417, Singapore"}]}],"member":"1968","published-online":{"date-parts":[[2022,2,16]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/j.ajsl.2018.06.009","article-title":"Assessing the impacts of port supply chain integration on port performance","volume":"34","author":"Han","year":"2018","journal-title":"Asian J. Shipp. Logist."},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Botti, A., Monda, A., Pellicano, M., and Torre, C. (2017). The Re-Conceptualization of the Port Supply Chain as a Smart Port Service System: The Case of the Port of Salerno. Systems, 5.","DOI":"10.20944\/preprints201704.0002.v1"},{"key":"ref_3","doi-asserted-by":"crossref","first-page":"893","DOI":"10.1016\/j.conengprac.2010.03.013","article-title":"The impact of ICT on intermodal transportation systems: A modelling approach by Petri nets","volume":"18","author":"Dotolia","year":"2010","journal-title":"Control. Eng. Pract."},{"key":"ref_4","first-page":"100","article-title":"Exploring the impact of digital transformation on technology entrepreneurship and technological market expansion: The role of technology readiness, exploration and exploitation","volume":"12","author":"Candelo","year":"2021","journal-title":"J. Bus. Res."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"93","DOI":"10.32604\/csse.2021.015547","article-title":"Smart Contract: Security and Privacy","volume":"38","author":"Alotaibi","year":"2021","journal-title":"Comput. Syst. Sci. Eng."},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"103325","DOI":"10.1016\/j.cities.2021.103325","article-title":"Blockchain-based smart contracts as new governance tools for the sharing economy","volume":"117","author":"Fiorentino","year":"2021","journal-title":"Cities"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1108\/RIBS-04-2019-0051","article-title":"Blockchain-based applications in shipping and port management: A literature review towards defining key conceptual frameworks","volume":"2","author":"Tsiulin","year":"2020","journal-title":"Rev. Int. Bus. Strategy"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.techfore.2019.03.015","article-title":"Supply chain re-engineering using blockchain technology: A case of smart contract based tracking process","volume":"144","author":"Chang","year":"2019","journal-title":"Technol. Forecast. Soc. Change"},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"601","DOI":"10.1108\/SCM-08-2019-0300","article-title":"Blockchain: Case studies in food supply chain visibility","volume":"25","author":"Rogerson","year":"2020","journal-title":"Supply Chain. Manag. Int. J."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"De Giovanni, P. (2019). Digital supply chain through dynamic inventory and smart contracts. Mathematics, 7.","DOI":"10.3390\/math7121235"},{"key":"ref_11","doi-asserted-by":"crossref","first-page":"2184","DOI":"10.1080\/00207543.2019.1627439","article-title":"Blockchain-oriented dynamic modelling of smart contract design and execution in the supply chain","volume":"58","author":"Dolgui","year":"2020","journal-title":"Int. J. Prod. Res."},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.cie.2019.07.022","article-title":"Smart contract-based approach for efficient shipment management","volume":"136","author":"Hasan","year":"2019","journal-title":"Comput. Ind. Eng."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/j.comcom.2021.03.008","article-title":"A security framework for Ethereum smart contracts","volume":"172","author":"Vivar","year":"2021","journal-title":"Comput. Commun."},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"e407","DOI":"10.7717\/peerj-cs.407","article-title":"Blockchain and smart contract for IoT enabled smart agriculture","volume":"7","author":"Pranto","year":"2021","journal-title":"PeerJ Comput. Sci."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"37397","DOI":"10.1109\/ACCESS.2021.3062471","article-title":"Automating procurement contracts in the healthcare supply chain using blockchain smart contracts","volume":"9","author":"Omar","year":"2021","journal-title":"IEEE Access"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"120786","DOI":"10.1016\/j.techfore.2021.120786","article-title":"Implementing decentralized auctions using blockchain smart contracts","volume":"168","author":"Omar","year":"2021","journal-title":"Technol. Forecast. Soc. Change"},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Ahmed, M., Taconet, C., Ould, M., Chabridon, S., and Bouzeghoub, A. (2021). IoT Data Qualification for a Logistic Chain Traceability Smart Contract. Sensors, 21.","DOI":"10.3390\/s21062239"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Yoo, M., and Won, Y. (2018). A study on the transparent price tracing system in supply chain management based on blockchain. Sustainability, 10.","DOI":"10.3390\/su10114037"},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"1771","DOI":"10.1007\/s00607-020-00880-z","article-title":"A scheme for intelligent blockchain-based manufacturing industry supply chain management","volume":"103","author":"Xu","year":"2021","journal-title":"Computing"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1016\/j.future.2019.05.042","article-title":"Elastic and cost-effective data carrier architecture for smart contract in blockchain","volume":"100","author":"Liu","year":"2019","journal-title":"Future Gener. Comput. Syst."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"107855","DOI":"10.1016\/j.ijpe.2020.107855","article-title":"Blockchain and smart contracts in supply chain management: A game theoretic model","volume":"228","year":"2020","journal-title":"Int. J. Prod. Econ."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/bs.adcom.2018.03.007","article-title":"Blockchain technology: Supply chain insights from ERP","volume":"111","author":"Banerjee","year":"2018","journal-title":"Adv. Comput."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"2501","DOI":"10.1016\/j.ifacol.2019.11.582","article-title":"Smart contracts for smart supply chains","volume":"52","author":"Prause","year":"2019","journal-title":"IFAC-PapersOnLine"},{"key":"ref_24","first-page":"40","article-title":"Formalization of BPMN based on extended Petri net model","volume":"43","author":"Li","year":"2016","journal-title":"Comput. Sci."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Najem, T., and Perucci, A. (2019). Mapping BPMN2 Service Choreographies to Colored Petri Nets. Proceedings of the International Conference on Software Engineering and Formal Methods, Oslo, Norway, 16\u201320 September 2019, Springer.","DOI":"10.1007\/978-3-030-57506-9_8"},{"key":"ref_26","doi-asserted-by":"crossref","unstructured":"Sun, T., and Yu, W. (2020). A formal verification framework for security issues of blockchain smart contracts. Electronics, 9.","DOI":"10.3390\/electronics9020255"},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Hang, L., and Kim, D.H. (2020). Reliable task management based on a smart contract for runtime verification of sensing and actuating tasks in IoT environments. Sensors, 20.","DOI":"10.3390\/s20041207"},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"101654","DOI":"10.1016\/j.cose.2019.101654","article-title":"Blockchain smart contracts formalization: Approaches and challenges to address vulnerabilities","volume":"88","author":"Singh","year":"2020","journal-title":"Comput. Secur."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Huh, J.H., and Kim, S.K. (2020). Verification plan using neural algorithm blockchain smart contract for secure P2P real estate transactions. Electronics, 9.","DOI":"10.3390\/electronics9061052"},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"101129","DOI":"10.1016\/j.pmcj.2020.101129","article-title":"Model checking smart contracts for ethereum","volume":"63","author":"Osterland","year":"2020","journal-title":"Pervasive Mob. Comput."},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"101227","DOI":"10.1016\/j.pmcj.2020.101227","article-title":"Verification of smart contracts: A survey","volume":"67","author":"Almakhour","year":"2020","journal-title":"Pervasive Mob. Comput."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.icte.2019.07.002","article-title":"Policy specification and verification for blockchain and smart contracts in 5G networks","volume":"6","author":"Unal","year":"2020","journal-title":"ICT Express"},{"key":"ref_33","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1080\/09540091.2020.1854181","article-title":"A novel blockchain-based privacy-preserving framework for online social networks","volume":"33","author":"Zhang","year":"2020","journal-title":"Connect. Sci."},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"e18623","DOI":"10.2196\/18623","article-title":"Combating health care fraud and abuse: Conceptualization and prototyping study of a blockchain antifraud framework","volume":"22","author":"Mackey","year":"2020","journal-title":"J. Med. Internet Res."},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"e266","DOI":"10.7717\/peerj-cs.266","article-title":"Towards a blockchain-based certificate authentication system in Vietnam","volume":"6","author":"Nguyen","year":"2020","journal-title":"PeerJ Comput. Sci."},{"key":"ref_36","first-page":"3872","article-title":"Puncturable Signatures and Applications in Proof-of-Stake Blockchain Protocols","volume":"15","author":"Li","year":"2020","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"101519","DOI":"10.1016\/j.tele.2020.101519","article-title":"Smart Contracts on the Blockchain\u2013A Bibliometric Analysis and Review","volume":"57","author":"Ante","year":"2020","journal-title":"Telemat. Inform."},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Prashar, D., Jha, N., Jha, S., Joshi, G.P., and Seo, C. (2020). Integrating IOT and blockchain for ensuring road safety: An unconventional approach. Sensors, 20.","DOI":"10.3390\/s20113296"},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"7752","DOI":"10.1109\/TII.2021.3057595","article-title":"A Model for Verification and Validation of Law Compliance of Smart-Contracts in IoT Environment","volume":"17","author":"Amato","year":"2021","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.knosys.2013.06.017","article-title":"Model checking epistemic\u2013probabilistic logic using probabilistic interpreted systems","volume":"50","author":"Wan","year":"2013","journal-title":"Knowl.-Based Syst."},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"100018","DOI":"10.1016\/j.bcra.2021.100018","article-title":"Model-driven engineering for multi-party business processes on multiple blockchains","volume":"2","author":"Corradini","year":"2021","journal-title":"Blockchain Res. Appl."},{"key":"ref_42","first-page":"100","article-title":"Blockchain: Research on the Application Progress of the Internet of Things","volume":"8","author":"Liang","year":"2018","journal-title":"Internet Things Technol."},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1016\/j.jik.2021.01.002","article-title":"Factors influencing blockchain adoption in supply chain management practices: A study based on the oil industry","volume":"6","author":"Aslam","year":"2021","journal-title":"J. Innov. Knowl."},{"key":"ref_44","doi-asserted-by":"crossref","first-page":"1162","DOI":"10.1002\/spe.2702","article-title":"Caterpillar: A business process execution engine on the Ethereum blockchain","volume":"49","author":"Dumas","year":"2019","journal-title":"Softw. Pract. Exp."}],"container-title":["Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2079-8954\/10\/1\/19\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T22:20:38Z","timestamp":1760134838000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2079-8954\/10\/1\/19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,16]]},"references-count":44,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2022,2]]}},"alternative-id":["systems10010019"],"URL":"https:\/\/doi.org\/10.3390\/systems10010019","relation":{},"ISSN":["2079-8954"],"issn-type":[{"value":"2079-8954","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,2,16]]}}}