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

A Distributed Model Checking Based on DivinE and Protocol Verification

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

Model checking is an effective and easy way to check if a concurrent program meets a sequential logical formula. Based on the exhaustive search of system state space,it usually adopts depth-first search algorithm（ DFS）. However,due to its continuity,it may need certain data structure and synchronization mechanism to consume lots of computer resources. Thus the problem of the explosion may exist in the state space. This problem was handled through the improvement of the traditional DFS algorithm via DivinE tools.