Verification of Concurrent Systems Using SPIN/Promela
Xiao Mei, Xue Zhu Jin · 2004
Safety analysis for concurrent systems is a vital research field of computer science.Model Checking is one of the most successful technologies of automatic verfication,its successful application is ascribed to the support of valid verification tools.SPIN is a famous tool for analyzing and retrying the logical consistency of concurrent sys- tem.Based on the introduction of the theory ofSPIN,this paper analyzes the channel operation,basic data structures and their functions of SPIN/Promela in detail.The fundamental verification algorithm is designed for software sys- tems.We use the SPIN to verify an example of concurrent system,the corresponding verification output charts are ob- tained.