基于SPIN/Promela的并发系统验证

Verification of Concurrent Systems Using SPIN/Promela

并发系统安全性分析是当前计算机科学中一个重要的研究领域。模型检测是最成功的自动验证技术之一,其成功应用归功于有效验证工具的支持。SPIN 是一种著名的分析验证并发系统逻辑一致性的工具。本文在阐述 SPIN工作机理的基础上,详细分析了基于 SPIN 的系统建模语言 Promela 中通道操作、基本数据结构及其功能,并设计了SPIN 形式化验证软件系统的基本算法,最后运用 SPIN 对一个并发系统实例进行验证,得出了相应验证输出图。

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.