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

A Distributed Model Checking Based on DivinE and Protocol Verification

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

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

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

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

摘　　要：模型检测是一个高效且简单的方法来检测一个并发程序是否满足一个时序逻辑公式,它基于对系统状态空间的穷举搜索,通常采用深度优先搜索算法(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.

关 键 词：模型检测 DFS 状态爆炸 分布式 DivinE 

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