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

Optimization and Research of Distributed Algorithm for Model Checking Space Decomposition

作　　者：潘怀宇[1] 龙士工[1] 郑涵[1] 

机构地区：[1]贵州大学计算机科学与技术学院,贵州贵阳550025

出　　处：《贵州大学学报（自然科学版）》2016年第3期86-90,共5页Journal of Guizhou University:Natural Sciences

基　　金：国家自然科学基金(61163001)

摘　　要：模型检测对于系统的校验有着适用范围广、自动化验证程度高、验证速度快等优势。但是其状态爆炸问题制约了其应用,使用分布式技术缓解状态爆炸问题引来了新的问题——如何对状态空间进行分解。本文介绍了分布式SCC分解的两个算法:FB与MP-MS算法,并在其基础上,引入了OWCTY技术,对算法进行优化。通过实验,证明优化后的算法有着更高的效率和更小的时间开销,对于缓解状态爆炸问题有着重要的意义。Model Checking has many advantages in system verification： wide range of applications,high degree of automation and high speed. But its state explosion problem restricts its application. Using the distributed technology to mitigate state explosion leads to a new problem-- how to decompose the state space？ Two algorithms about distributed SCC decomposition were described： FB and MP-MS algorithm. Then the OWCTY technology was applied in optimizing these two algorithms. Through the experiment,the results show that the optimization algorithm has a higher efficiency and less time cost. It has important significance to alleviating the problem of state explosion.

关 键 词：模型检测 状态爆炸 OWCTY 分布式技术 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]