[00057752]一种死锁检测验证方法
技术详细介绍
本发明公开了一种死锁检测验证方法，包括：提取出待测进程的状态、状态转移关系；建立不同的死锁检测模板；将进程的状态、状态转移关系以及建模属性按照类别分别写入XML配置文件；读取XML配置文件，选择相应的死锁检测模板进行模型检测：生成时态逻辑表达式CTL，将进程的状态和状态转移关系及时态逻辑表达式CTL转换为SMV模型；执行SMV模型，分析执行结果中时态逻辑表达式CTL的真值，判断设计文档是否包含死锁。本发明通过自动分析死锁检测相关信息的输入自动选择相应模板转换为SMV模型的原型，降低了死锁检测的难度；本方法不受软件开发语言限制，可以在系统设计阶段对设计方案进行死锁检测，比在软件开发阶段再发现死锁更能减少不必要的损失。
