郑　涵，龙士工，潘怀宇，刘照祥

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



基于DivinE的分布式模型检测及协议验证

郑涵，龙士工*，潘怀宇，刘照祥

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

模型检测是一个高效且简单的方法来检测一个并发程序是否满足一个时序逻辑公式，它基于对系统状态空间的穷举搜索，通常采用深度优先搜索算法(DFS)。然而由于DFS算法固有的连续性，并且需要用到某些数据结构和同步机制，使得计算机的资源被大量的消耗，因此长期存在状态空间爆炸的问题。本文通过改进传统的DFS算法，利用DivinE工具，使状态空间爆炸问题能够在分布式环境下得到缓解。

模型检测；DFS；状态爆炸；分布式；DivinE

近年来，计算机技术进入高速发展的时代，人们对于计算机的应用需求也越来越高，为了保证计算机系统和网络更好地满足人们的要求，确保系统的正确性、安全性及活性等属性，我们需要对系统进行检测，找出系统存在的缺陷，并不断对其进行优化。模型检测(model checking)以其简洁明了和自动化程度高而引人注目。

模型检测是一个高效且简单的方法来检测一个并发程序是否满足一个时序逻辑公式，它主要检测有限状态程序，并把程序看成是一个结构，进而解释时序逻辑和评估公式，它比时序推论证明要简单得多，并且容易高效地实现。

模型检测的基本思想是用状态迁移系统(S)表示系统的行为，用模态/时序逻辑公式(F)描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态迁移系统S是否是公式F的一个模型？……