模型检测的理论、技术与工具

模型检测被认为是最成功的形式化方法。模型检测的研究具有理论和实际双重意义，是当前计算机科学基础研究的前沿领域。本项目将从模型检测的逻辑与算法基础、模型检测的关键技术、以及模型检测的工具与实例研究三个层面展开研究。在第一层面上，将探讨传统命题时序逻辑的一阶的和度量的推广，并从博弈和自动机的角度研究mu-演算模型检测的算法；在第二层面上，将围绕克服"状态爆炸"的技术以及非有穷状态系统的模型检测方法，着重研究限界模型检测与带参模型检测的理论与技术；在第三层面上，将设计并实现面向软件的限界模型检测工具和自动化程度较高的面向带参并发系统的模型检测工具，同时应用所提出的理论、方法和所实现的工具，对计算机领域的若干典型应用展开实例研究。

在模型检测的逻辑基础、算法设计、工具实现与实例应用三个层面上进行了深入研究，取得了多项成果，包括CTL的限界语义和基于该限界语义和QBF公式的正确性判定的模型检测方法、基于形式语言理论和反例制导的抽象求精方法的并发递归程序安全性质的自动验证、Applied Pi-演算的符号互模拟理论、带参系统的模型检测的状态聚类和数组截断方法、以及模型检测技术在DSP系统和CPU设计功能验证的实例研究。.基于所取得的理论成果，实现了包括集限界模型检测和符号模型检测方法于一体的模型检测工具VERDS、存储一致性验证工具MOTEC、带参模型检测工具PaMC。这些原型工具为今后的研究工作提供了平台和基础。.项目执行期间开展了高层次的学术交流。组织了2次国际学术讲习班，有240多人次参加，推动了国内在模型检测领域的研究。发表学术论文50篇；培养博士16名、硕士4名、出站博士后1名。全面实现了项目的预定研究目标。