The Overview of SPIN in Software Model Checking
Yaning Zheng, Kaiqi Ru, Xuewei Feng, Dongxia Wang · 2021
With the rapid development of the Internet, people are becoming more dependent on the Internet. However, the security of the network is an issue that cannot be ignored. As a formal verification method, model checking has the advantage of automation in security property verification. In this paper, we organized much literature about model checking and SPIN. SPIN is one of the most widely used model checking tools. We tracked the application and development of SPIN in the past 30 years. In addition, we also discussed the optimization problems of SPIN, such as the problem of source code automation modeling. And we gave a theoretical framework for modeling to help professional researchers solve the problem faster and better. In the application of model checking and SPIN, we mainly focus on network protocols and cyberspace vulnerability. Finally, we discussed the challenges and future work.