论文部分内容阅读
实时系统的模型检验方法是一种保证计算机实时系统安全性和可靠性的严格的形式化方法，随着计算机科学的发展，这种方法已经被广泛地接受和使用。由于模型检验方法在对系统建模时存在状态空间爆炸问题，因此模型验证核心问题是状态空间最小化问题。使用时间自动机对实时系统规范和验证，主要包括对实时系统建模即构造系统的时间自动机和安全可靠性验证。这两方面的核心问题是状态空间的简化和状态可达性分析。而这一核心问题是本文研究的重点。 在实时系统规范验证中。考虑到系统中多数待检验问题仅仅是一些简单的性质。因此我们不必构造系统的所有状态集合，而仅仅考虑对可达性问题的判断。论文对时间自动机的可达性问题进行了深入研究，对不同的可达性分析方法进行了比较，并着重对基于时间约束的可达性分析方法进行分析。在此基础上，针对基于时间约束的可达性分析方法，本文给出了该方法的机器表示，并提出了一种新的后继计算方法，通过该方法能够较好地减少后继状态空间的个数，从而使问题规模减小；另外给出了可达性算法的预处理方法，通过预处理可以节省算法占用的内存空间，提高了算法的运行效率。