{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T04:21:11Z","timestamp":1743913271965,"version":"3.40.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031664557"},{"type":"electronic","value":"9783031664564"}],"license":[{"start":{"date-parts":[[2024,9,29]],"date-time":"2024-09-29T00:00:00Z","timestamp":1727568000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,9,29]],"date-time":"2024-09-29T00:00:00Z","timestamp":1727568000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-66456-4_10","type":"book-chapter","created":{"date-parts":[[2024,9,28]],"date-time":"2024-09-28T06:01:58Z","timestamp":1727503318000},"page":"179-198","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Template-Based Smart Contract Verification: A Case Study on\u00a0Maritime Transportation Domain"],"prefix":"10.1007","author":[{"given":"Xufeng","family":"Zhao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qiuyang","family":"Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2832-5590","authenticated-orcid":false,"given":"Xue-Yang","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenhui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,29]]},"reference":[{"key":"10_CR1","unstructured":"Maritime code of PRC (1993). https:\/\/www.gov.cn\/guoqing\/2020-12\/24\/content_5572935.htm"},{"key":"10_CR2","unstructured":"Marismart framework (2023). https:\/\/github.com\/MariSmartSourceCode\/MariSmart"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"44905","DOI":"10.1109\/ACCESS.2021.3066503","volume":"9","author":"RW Ahmad","year":"2021","unstructured":"Ahmad, R.W., Salah, K., Jayaraman, R., Yaqoob, I., Omar, M., Ellahham, S.: Blockchain-based forward supply chain and waste management for Covid-19 medical equipment and supplies. IEEE Access 9, 44905\u201344927 (2021)","journal-title":"IEEE Access"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Alqahtani, S., He, X., Gamble, R., Mauricio, P.: Formal verification of functional requirements for smart contract compositions in supply chain management systems (2020)","DOI":"10.24251\/HICSS.2020.650"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: 1990 Proceedings of Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 414\u2013425. IEEE (1990)","DOI":"10.1109\/LICS.1990.113766"},{"key":"10_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/bfb0032042","volume-title":"ICALP 1990","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/bfb0032042"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 66\u201377 (2018)","DOI":"10.1145\/3176245.3167084"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Bai, X., Cheng, Z., Duan, Z., Hu, K.: Formal modeling and verification of smart contracts. In: Proceedings of the 2018 7th International Conference on Software and Computer Applications, pp. 322\u2013326 (2018)","DOI":"10.1145\/3185089.3185138"},{"key":"10_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.tre.2021.102539","volume":"156","author":"G Balci","year":"2021","unstructured":"Balci, G., Surucu-Balci, E.: Blockchain adoption in the maritime supply chain: examining barriers and salient stakeholders in containerized international trade. Transp. Res. Part E: Logist. Transp. Rev. 156, 102539 (2021)","journal-title":"Transp. Res. Part E: Logist. Transp. Rev."},{"issue":"3","key":"10_CR10","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011)","journal-title":"IEEE Softw."},{"key":"10_CR11","unstructured":"Bavosa, A.: Smart contracts (2018). https:\/\/github.com\/ajb413\/eth-shipment-tracking\/tree\/master"},{"key":"10_CR12","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL 4.0. Department of Computer Science, Aalborg University (2006)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et\u00a0al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 91\u201396 (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"10_CR14","unstructured":"Buterin, V., et\u00a0al.: A next-generation smart contract and decentralized application platform. White Paper 3(37), 2\u20131 (2014)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495\u2013499. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_44"},{"key":"10_CR17","volume-title":"Model Checking","author":"EM Clarke Jr","year":"2018","unstructured":"Clarke, E.M., Jr., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking. MIT Press, Cambridge (2018)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Elmay, F.K., Madine, M., Salah, K., Jayaraman, R.: NFTs for trusted traceability and management of digital twins for shipping containers. In: 2023 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events (PerCom Workshops), pp. 433\u2013438. IEEE (2023)","DOI":"10.1109\/PerComWorkshops56833.2023.10150331"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"124507","DOI":"10.1109\/ACCESS.2022.3225000","volume":"10","author":"FK Elmay","year":"2022","unstructured":"Elmay, F.K., Salah, K., Jayaraman, R., Omar, I.A.: Using NFTs and blockchain for traceability and auctioning of shipping containers and cargo in maritime industry. IEEE Access 10, 124507\u2013124522 (2022)","journal-title":"IEEE Access"},{"key":"10_CR20","unstructured":"Foundation, T.: Michelson: the language of smart contracts in Tezos. https:\/\/tezos.gitlab.io\/active\/michelson.html#language-semantics"},{"key":"10_CR21","unstructured":"Ganne, E.: Can blockchain revolutionize international trade? [online] (2018). https:\/\/www.wto.org\/english\/res_e\/booksp_e\/blockchainrev18_e.pdf"},{"key":"10_CR22","unstructured":"Group, B.C.: Digital innovation in trade finance: have we reached a tipping point? (2017). https:\/\/www.swift.com\/news-events\/news\/digital-innovation-trade-finance-have-we-reached-tipping-point"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.cie.2019.07.022","volume":"136","author":"H Hasan","year":"2019","unstructured":"Hasan, H., AlHadhrami, E., AlDhaheri, A., Salah, K., Jayaraman, R.: Smart contract-based approach for efficient shipment management. Comput. Ind. Eng. 136, 149\u2013159 (2019)","journal-title":"Comput. Ind. Eng."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"da\u00a0Horta, L.P.A., Reis, J.S., de\u00a0Sousa, S.M., Pereira, M.: A tool for proving Michelson smart contracts in WHY3. In: 2020 IEEE International Conference on Blockchain (Blockchain), pp. 409\u2013414. IEEE (2020)","DOI":"10.1109\/Blockchain50366.2020.00059"},{"key":"10_CR26","unstructured":"Keith, M., Edward, S.: Master ex-ship LNG sales agreement between Cheniere Marketing, Inc. and Gaz De France International Trading S.A.S (2007). https:\/\/www.sec.gov\/Archives\/edgar\/data\/3570\/000119312507106384\/dex102.html"},{"key":"10_CR27","unstructured":"Kernighan, B.W., Ritchie, D.M.: The C programming language (2002)"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254\u2013269 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-662-58387-6_28","volume-title":"Financial Cryptography and Data Security","author":"A Mavridou","year":"2018","unstructured":"Mavridou, A., Laszka, A.: Designing secure Ethereum smart contracts: a finite state machine based approach. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957, pp. 523\u2013540. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-58387-6_28"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-030-32101-7_27","volume-title":"Financial Cryptography and Data Security","author":"A Mavridou","year":"2019","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: VeriSolid: correct-by-design smart contracts for Ethereum. In: Goldberg, I., Moore, T. (eds.) FC 2019. LNCS, vol. 11598, pp. 446\u2013465. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32101-7_27"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Mikk, E., Lakhnech, Y., Siegel, M., Holzmann, G.J.: Implementing statecharts in PROMELA\/SPIN. In: Proceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques, pp. 90\u2013101. IEEE (1998)","DOI":"10.1109\/WIFT.1998.766303"},{"key":"10_CR32","unstructured":"Mueller, B.: A framework for bug hunting on the Ethereum blockchain. ConsenSys\/mythril (2017)"},{"key":"10_CR33","doi-asserted-by":"publisher","DOI":"10.1016\/j.tre.2022.102764","volume":"163","author":"S Nguyen","year":"2022","unstructured":"Nguyen, S., Chen, P.S.L., Du, Y.: Risk assessment of maritime container shipping blockchain-integrated systems: an analysis of multi-event scenarios. Transp. Res. Part E: Logist. Transp. Rev. 163, 102764 (2022)","journal-title":"Transp. Res. Part E: Logist. Transp. Rev."},{"key":"10_CR34","doi-asserted-by":"publisher","DOI":"10.1016\/j.cie.2022.107995","volume":"167","author":"IA Omar","year":"2022","unstructured":"Omar, I.A., Debe, M., Jayaraman, R., Salah, K., Omar, M., Arshad, J.: Blockchain-based supply chain traceability for COVID-19 personal protective equipment. Comput. Ind. Eng. 167, 107995 (2022)","journal-title":"Comput. Ind. Eng."},{"key":"10_CR35","doi-asserted-by":"publisher","first-page":"167756","DOI":"10.1109\/ACCESS.2021.3137307","volume":"9","author":"PK Patro","year":"2021","unstructured":"Patro, P.K., Ahmad, R.W., Yaqoob, I., Salah, K., Jayaraman, R.: Blockchain-based solution for product recall management in the automotive supply chain. IEEE Access 9, 167756\u2013167775 (2021)","journal-title":"IEEE Access"},{"key":"10_CR36","unstructured":"ShipChain: Shipchain smart contracts (2020). https:\/\/github.com\/ShipChain\/smart-contracts\/tree\/master"},{"issue":"2","key":"10_CR37","doi-asserted-by":"publisher","first-page":"41","DOI":"10.3390\/logistics5020041","volume":"5","author":"D Song","year":"2021","unstructured":"Song, D.: A literature review, container shipping supply chain: planning problems and research opportunities. Logistics 5(2), 41 (2021)","journal-title":"Logistics"},{"key":"10_CR38","unstructured":"Szabo, N.: Smart contracts (1994). http:\/\/www.fon.hum.uva.nl\/rob\/Courses\/InformationInSpeech\/CDROM\/Literature\/LOTwinterschool2006\/szabo.best.vwh.net\/smart.contracts.html"},{"issue":"7","key":"10_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3464421","volume":"54","author":"P Tolmach","year":"2021","unstructured":"Tolmach, P., Li, Y., Lin, S.W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. (CSUR) 54(7), 1\u201338 (2021)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"10_CR40","unstructured":"Uncitral: Hamburg rules (1987). https:\/\/uncitral.un.org\/zh\/texts\/transportgoods\/conventions\/hamburg_rules"},{"key":"10_CR41","unstructured":"Zhao, X., Lu, Y.: Marismart verifier webpage (2023). http:\/\/124.16.137.30:50002\/#\/dashboard-en"},{"key":"10_CR42","doi-asserted-by":"publisher","unstructured":"Zhao, X., Wei, Q., Zhu, X.Y., Zhang, W.: A smart contract development framework for maritime transportation systems. In: 2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security Companion (QRS-C), pp. 310\u2013319 (2023). https:\/\/doi.org\/10.1109\/QRS-C60940.2023.00091","DOI":"10.1109\/QRS-C60940.2023.00091"},{"issue":"8","key":"10_CR43","first-page":"2875","volume":"33","author":"Y Zhao","year":"2022","unstructured":"Zhao, Y., Zhu, X., Li, G., Bao, Y.: Time constraint patterns of smart contracts and their formal verification. J. Softw. 33(8), 2875\u20132895 (2022)","journal-title":"J. Softw."}],"container-title":["Lecture Notes in Computer Science","Engineering of Complex Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66456-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T21:04:52Z","timestamp":1743887092000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66456-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,29]]},"ISBN":["9783031664557","9783031664564"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66456-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,29]]},"assertion":[{"value":"29 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"ICECCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Engineering of Complex Computer Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"iceccs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cyprusconferences.org\/iceccs2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}