摘要:本文介绍了一个就线性时段特性验证实时系统的正确性的工具的设计思想以及相关算法.我们使用和时间自动机作为实时系统的描述模型.同时,为了便于描述并发实时系统,我们使用带共享变量和通道的时间自动机网作为并发实时系统的描述模型.在检验时间自动机网时,用户可以使用工具提供的合成程序将其合作为一个时间自动机然后进行检验.由于时间自动机的状态空间是无穷的,我们通过引入整数状态和状态等价关系的概念,将整个状态空间划分为有限的状态等价类空间.模型检验过程只需要通过对等价类空间的搜索就可以完成.但往往等价类空间的规模很大,超出了现在计算机的处理能力,原始搜索算法仅仅在理论上是可行的.为了增强工具的使用性,工具中使用的算法运用了一些优化技术来避免了对等价类空间的穷尽搜索,使得工具在使用时具有比较好的时间和空间效率.