当前越来越多的实时系统被应用在我们的日常生活中,如红绿灯、电梯和飞机上的软件系统。这些系统的异常行为会对社会造成巨大的经济损失,因此验证实时系统的正确性十分重要。通过生成大量的测试用例然后检测系统的行为是一种常见的方法,但是由于测试用例总是有限的,总会有一些情况无法被覆盖到。因此通过测试用例的方法来验证正确性从本质上讲是不完备的。形式化方法,或者更具体点,模型检测,对于软硬件系统的验证来说是一种兼顾可靠性和完备性的方法。给定系统的模型,该方法可以检测是否模型满足某些性质,常见的如安全性和活性。然而遗憾的是,在一些模型中某些性质是不可判定的。如图灵机作为强大到能执行任意计算机程序的模型,在该模型上停机问题是不可判定的。因此研究者们在验证某些系统时,总希望能找到合适的并且可判定的模型。在实时系统的验证中时间自动机是一种非常流行的模型。在该模型上许多性质都是可判定的,因此已经有许多基于该模型的工具被提出,如UPPAL。然而,时间自动机并不能直接应用到带有递归的实时系统中,需要表达能力更强的模型来验证这样的复杂系统。为了解决这个问题,嵌套时间自动机(NeTA)被提出并被研究。嵌套时间自动机是一个栈元素为时间自动机的下推系统。在该模型中,每个时间自动机都可以被中止并被压入栈顶,还可以从栈顶出栈并恢复运行。压栈和出栈的操作可以完美的模拟程序中的递归能力。当前在嵌套时间自动机上已经有许多性质及扩展模型被研究,例如冷冻时钟、对角线约束、可达性问题的算法和可调度性问题。本论文也继续对嵌套时间自动机的性质做更为深入的研究,主要贡献如下。本文提出了单可调整嵌套时间自动机模型,其可以看作是嵌套时间自动机和单可调整时钟的结合。该模型非常适合软实时系统的分析,因为单可调整时钟可以用来描述截止时间,且该截止时间可以被环境所更新。本文证明了单可调整嵌套时间自动机的终止性和有界性是可判定的。本文还提出了带有不变式的嵌套时间自动机模型,其在嵌套时间自动机的基础上扩展了不变式。不变式在实时系统中经常被用来约束每个状态下的时间流动。众所周知,带有不变式的时间自动机可以被编码到不带不变式的时间自动机。然而在递归的情况下是否不变式对模型的表达能力有影响,还没有相关研究。本文会分析不变式对嵌套时间自动机的影响。具体来说,本文会研究带有不变式的嵌套时间自动机的可达性问题,最终会说明在带有不变式的嵌套时间自动机上的可达性问题在只有一个全局时钟的情况下是不可判定的,而如果没有不变式则是可判定的。更进一步的,本文会说明在带有不变式的嵌套时间自动机上如果没有全局时钟则是可判定的,这是通过说明一个好的栈依然满足良形式约束得到的。