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

Optimization and Research of Distributed Algorithm for Model Checking Space Decomposition

模型检测对于系统的校验有着适用范围广、自动化验证程度高、验证速度快等优势。但是其状态爆炸问题制约了其应用,使用分布式技术缓解状态爆炸问题引来了新的问题——如何对状态空间进行分解。本文介绍了分布式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.