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