Verification of Concurrent Go Programs using Timed Trace Theory
DOI:
https://doi.org/10.59796/jcst.V15N2.2025.94Keywords:
concurrent program, conformance checking, Go program, goroutine, time Petri net, timed trace theory, verifyAbstract
The Go programming language, or Go, plays a critical role in developing concurrent programs because it provides features such as goroutines and channels that support program concurrency. Even though concurrency makes programs efficient, verification is required to ensure their correctness. This paper proposes a novel approach to verifying concurrent Go programs using timed trace theory. The proposed approach is specifically designed to verify concurrent systems. Verifying a Go program using timed trace theory is divided into two tasks: modeling and verification. Modeling involves transforming a Go program into time Petri nets using a proposed algorithm. Verification involves checking the conformance between the Go program and its specification. This can be done automatically by the timed trace theoretic verification tool, which supports a partial order reduction technique to mitigate the state explosion problem. We demonstrate the verification of the Philosopher problem using both the total order method and the partial order reduction method. Experiments with the Go program of the Philosopher problem demonstrate the effectiveness of the proposed method.
References
Dill, D. L. (1988). Trace theory for automatic hierarchical verification of speed-independent circuits. Advanced Research in VLSI: Proceedings of the 5th MIT Conference. MIT Press. https://doi.org/10.7551/mitpress/1102.001.0001
Dilley, N., & Lange, J. (2021). Automated verification of Go programs via bounded model checking [Conference presentation]. 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), November 15-19, 2021, Melbourne, Australia. https://doi.org/10.1109/ASE51524.2021.9678571
Fu, S., & Zhang, K. (2023). Network asset sensitive information management system based on Golang [Conference presentation]. International Conference on Algorithms, Computing and Data Processing (ACDP), June 23-25, 2023, Qingdao, China. https://doi.org/10.1109/ACDP59959.2023.00030
Gabet, J., & Yoshida, N. (2020). Static race detection and mutex safety and liveness for Go programs (extended version) [Conference presentation]. European Conference on Object-Oriented Programming, Online Conference, November 15-17, 2020, Berlin, Germany. https://doi.org/10.48550/arXiv.2004.12859
Gao, C., Lv, H., & Tan, Y. (2023). Multithreading technology based on Golang implementation [Conference presentation]. 3rd Asia-Pacific Conference on Communications Technology and Computer Science (ACCTCS), February 25-27, 2023, Shenyang, China. https://doi.org/10.1109/ACCTCS58815.2023.00116
Ghosh, P., & Karsai, G. (2023). Distributed cyber physical systems software model checking using timed automata [Conference presentation]. IEEE 26th International Symposium on Real-Time Distributed Computing (ISORC), May 23-25, 2023, Nashville, TN, USA. https://doi.org/10.1109/ISORC58943.2023.00030
Go. (2019). Documentation. Retrieved July 2, 2024, from https://go.dev/doc
Hu, J., & Zhang, Y. (2023). Design of remote monitoring system for ventilator based on Golang and MongoDB [Conference presentation]. 6th International Conference on Artificial Intelligence and Big Data (ICAIBD), May 26-29, 2023, Chengdu, China. https://doi.org/10.1109/ICAIBD57115.2023.10206318
Kitahara, Y., Nakamura, M., & Sakakibara, K. (2022). An investigation of formal verification of control policy of multi-car elevator systems using statistical Model checking [Conference presentation]. International Conference on Machine Learning and Cybernetics (ICMLC), September 9-11, 2022, Japan. https://doi.org/10.1109/ICMLCp6445.2022.9941319
Lange, J., Ng, N., Toninho, B., & Yoshida, N. (2018). A static verification framework for message passing in Go using behavioural types [Conference presentation]. IEEE/ACM 40th International Conference on Software Engineering (ICSE), May 27-June 3, 2018, Gothenburg, Sweden. https://doi.org/10.1145/3180155.3180157
Meyerson, J. (2014). The Go Programming Language. IEEE Software, 31(5), 101-104. https://doi.org/10.1109/MS.2014.127
Pang, S., Bian, Z., Zhang, Z., Meng, L., & Jiao, J. (2024). A safety analysis method based on model checking [Conference presentation]. 10th International Symposium on System Security, Safety, and Reliability (ISSSR), March 16-17, 2024, Xiamen, China. https://doi.org/10.1109/ISSSR61934.2024.00014
Pradubsuwun, D., Yoneda, T., & Myers, C. (2005). Partial order reduction for detecting safety and timing failures of timed circuits. IEICE transactions on information and systems, 88(7), 1646-1661. https://doi.org/10.1093/ietisy/e88-d.7.1646
Prasertsang, A., & Pradubsuwun, D. (2016). Formal verification of concurrency in Go [Conference presentation]. 13th International Conference on Computer Science and Software Engineering (JCSSE), July 13-15, 2016, Khonkaen, Thailand. https://doi.org/10.1109/JCSSE.2016.7748882
Zhou, B., Yoneda, T., & Myers, C. (2001). Framework of timed trace theoretic verification revisited [Conference presentation]. Proceedings of the 10th Asian Test Symposium, November 19-20, 2001, Kyoto Japan. https://doi.org/10.1109/ATS.2001.990323
Zhu, W., & Wang, Y. (2023). Model checking for scheduling on flight decks of aircraft carriers [Conference presentation]. IEEE 6th Information Technology, Networking, Electronic and Automation Control Conference (ITNEC), February 24-26, 2023, Chongqing, China. https://doi.org/10.1109/ITNEC56291.2023.10082464
Downloads
Published
How to Cite
Issue
Section
Categories
License
Copyright (c) 2025 Journal of Current Science and Technology
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
