潘怀宇，龙士工，郑　涵

(贵州大学 计算机科学与技术学院，贵州 贵阳 550025)



模型检测空间分解分布式算法的优化与研究

潘怀宇，龙士工*，郑涵

(贵州大学 计算机科学与技术学院，贵州 贵阳 550025)

模型检测对于系统的校验有着适用范围广、自动化验证程度高、验证速度快等优势。但是其状态爆炸问题制约了其应用，使用分布式技术缓解状态爆炸问题引来了新的问题——如何对状态空间进行分解。本文介绍了分布式SCC分解的两个算法：FB与MP-MS算法，并在其基础上，引入了OWCTY技术，对算法进行优化。通过实验，证明优化后的算法有着更高的效率和更小的时间开销，对于缓解状态爆炸问题有着重要的意义。

模型检测;状态爆炸;OWCTY;分布式技术

日常生活中，人们对于ICT系统(Information and Communication Technology)的依赖正在迅速增长。随着需求的增长，这些系统的结构与分层也越来越复杂，类似的复杂系统我们随处可见，比如智能卡、个人PC、手机和智能家居等。对于此类系统的可靠性、正确性与安全性保障，是系统在设计过程中的一个关键问题。模型检测[1](Model Checking)作为形式化验证方法的主要技术之一，其实质是基于时序逻辑(LTL，CTL)的计算机自动化形式验证的方法，利用穷举搜索状态空间来检验既有模型与一个时序逻辑公式，验证该系统模型是否满足此时序逻辑公式描述的具体性质。模型检测技术适用范围广、自动化验证程度高、验证速度快，只要计算机有足够的处理能力，最终总能终止并给出验证结果，当验证属性不满足时，还可以给出反例(Counterexample)，便于发现错误并进行修改。……