论文部分内容阅读
随着计算机软硬件系统规模的日益复杂化、重要化，如何保证计算机系统的正确性和可靠性，逐渐成为当前理论界和产业界共同关心的重要问题。其实，令计算机更好地为我们服务的主要障碍，不是现有机器的硬件速度和计算能力，而是我们在设计和实现正确而可靠的系统方面的能力还比较有限。长期以来，常用的系统设计检验方法是以经验为基础的测试方法。但是，测试方法只能证明错误的存在，但不能证明错误的不存在，所以，对于高可靠性系统来说，测试方法有明显的局限性。
在过去二十多年间，各国研究人员为解决这个问题付出了巨大的努力，取得了重要的进展。在为此提出的诸多理论和方法中，模型检查(ModelChecking)以其简洁明了和自动化程度高而引人注目。
本文首先介绍了模型检查技术的基本思想、研究方向和最新研究进展以及相关背景工具和VHDL语言，然后介绍了模型检查技术的理论基础，即时态逻辑。本文针对一般的VHDL系统，研究并设计了两种模型检查系统方案。这两种方案是：使用美国CarnegieMellon大学开发的基于VHDL的模型检查工具CV进行验证，以及使用基于命题μ-演算方法进行验证。
本文的主要内容可以概括为以下几个方面：1.针对使用VHDL模型检查工具CV进行系统验证必须要完成的前期工作和接口工作进行了研究和设计，包括CV工作机制的研究、VHDL系统子集的规范化处理研究、目标系统规约语言的特征研究以及CV运行环境的分析。
2.提出了一种新的VHDL模型检查系统设计方案，包括VHDL系统到有限状态机(FSM)的转化方案，以及在此基础上进行的基于命题μ-演算的模型检查系统设计方案；这两个方案配合起来，就可以实现与CV的功能很相似的VHDL系统模型检查功能。
3.重点研究了基于命题μ-演算的模型检查系统，建立了μ-演算系统框架，设计了基本时序算子、不动点算子、μ-演算公式以及从CTL公式到μ-演算公式的转换的计算方法，提出了基于命题μ-演算的VHDL模型检查方案，并且实现了上述设计与方案，同时还实现了对不动点算子复杂度进行优化的方案。
4.运用以上两种模型检查方法对目标系统进行了验证测试，对这两种模型检查工具和方案进行了比较与分析，并对今后的研究工作进行了展望。