实时系统是一类重要的计算机应用系统,它经常被使用在对安全性要求极高的操作环境中,因此确保此类系统的正确性至关重要,并且需要我们使用形式化的方法对实时系统进行规范验证。 本文在R. Alur等人提出的时间自动机的基础上深入研究了系统模型验证理论及其实际应用。我们通过判定实时系统以及它的规范说明所对应的时间正则语言的交集是否为空对实时系统进行规范验证,比较常用的验证方法包括构造区域自动机和带自动机。通过对这些方法分析研究,我们发现当系统规模较大时,规范建模过程就会相对复杂,而且还可能会出现状态组合爆炸的问题。因此,系统需要一种能较好解决这些问题的自动规范验证技术。 UPPAAL是一种以时间自动机作为行为模型、在实时系统和通讯协议的自动规范验证中占据重要位置的验证工具。在对UPPAAL的基本结构和工作原理分析之后,我们发现它采用的限制技术和快速验证技术可以避免构建状态空间中的不可达状态,能在一定程度上解决状态空间爆炸问题。但是系统在自动规范验证时没能有效利用问题求解过程中的启发性信息,并且存在一些无用状态循环,就会导致问题求解效率低下。本文针对这些问题对快速前向验证算法进行改进,提出了一种带有启发性信息的快速前向验证算法。文中设计估价函数用于估算每一个全局状态到达目标全局状态需要付出的代价,定义无用状态循环用来避免对无用状态重复分析,这样既节省了系统存储空间,又提高了求解问题的效率。接下来,本文对一个通讯协议进行分析和规范,并且利用UPPAAL对该协议的时间自动机模型进行自动规范验证,证明了协议的正确性和安全性。 带有时间特性的Petri网也是一种适合描述和分析实时系统的模型工具,但是它的性能分析能力有一定局限性。因此,本文利用将时延Petri网转换到时间自动机的语义等价转换算法,将一个带有单处理器的铁路岔道系统的时延Petri网模型转换成与其语义等价的一组时间自动机模型,并且利用UPPAAL对转换后系统模型的安全性和受限活性进行自动规范验证。