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

作     者：肖美华 薛锦云 

作者机构：南昌大学计算中心 江西师范大学计算机信息工程学院 

基　　金：国家自然科学基金(60273092) 江西省自然科学基金(0411041) 南昌大学03年度科研基金项目共同资助 

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2004年第31卷第8期

页      码：201-203,208页

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

主 题 词：模型检测 并发系统 软件可靠性 SPIN/Pronlela 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.3969/j.issn.1002-137X.2004.08.059

馆 藏 号：203670127...