实时嵌入系统被广泛用于安全关键系统中,这类系统一旦发生错误,将会造成重大的生命及财产损失,因此实时嵌入系统的可靠性保障至关重要。实时系统的正确性不仅仅依赖于系统逻辑计算结果的正确性,还依赖于计算是否在规定时间内完成。为了提高系统的安全性和可靠性,人们提出了形式化方法来验证系统的正确性。形式化验证具有严格的数学理论基础,并通过完善的数学和逻辑证明发现系统中的错误。模型检验是一种针对有穷状态并发系统的形式化自动验证工具。模型检验使用形式语言描述系统模型和系统规约,通过穷尽遍历状态空间自动检验系统模型是否满足系统规约。如今,模型检验的研究成果已经被很好的应用于工业界的开发设计过程中。本文的主要工作包括以下几个方面：●状态爆炸问题是模型检验中的重要挑战之一。为了缓解这个问题,本文针对并发时间自动机的模型检验提出了一种新的偏序约减方法。这种方法可以在某些符号状态上只枚举部分可能发生的转换,而不再是穷尽遍历所有可达的状态空间。我们给出了偏序约减枚举的充分条件以及如何判断这些偏序枚举条件的有效算法,使得偏序约减方法得到的可达性分析结果与原有的穷尽遍历方法得出的结果一致。基于该偏序约减方法的可达性分析优化算法在初次访问可达状态时仅仅计算其中部分可能发生转换的符号后继。稍后,当算法重新访问已生成的可达状态时再判断是否需要计算这个状态上所有可能发生的转换的后继状态。通过实验表明,使用这种优化偏序约减方法可以显著减少状态空间遍历中生成的符号状态的数量,从而降低了模型检验算法的内存需求和CPU运行时间。●很多实时嵌入式系统都使用中断驱动的体系结构。为了帮助系统设计人员在系统设计过程中应用模型检验技术来提高实时系统的正确性,我们提出了一种中断驱动系统建模的方法和模型转换技术。我们首先确定了中断驱动系统中与时序性质相关的系统要素(包括系统调度任务、中断源、中断处理程序)和相关参数,并要求设计人员在设计阶段明确指出这些要素的参数。然后,我们提出了将这些要素和参数自动转化为形式化模型的方法：使用时间自动机对中断事件进行建模,使用中断向量表和CPU处理栈对中断处理过程进行建模。● 中断驱动系统通常由中断处理程序和操作系统调度的任务组成,前者由中断源触发后处理中断事件,后者则负责处理系统的日常任务以及某些中断处理事件的后续处理。因为这类系统是实时控制系统,对中断事件的处理需要在规定时间内响应并完成,否则可能造成严重的系统失效。基于前文中的建模方法和模型转换技术,我们进一步给出了针对中断处理超时错误的模型检验方法,并在此基础上给出了共享资源的完整性、子程序原子性的检验方法。●基于前文的系统建模方法和模型转换技术,我们进一步扩展了系统模型,系统中的中断事件和任务可以通过控制变量相互关联,当控制变量取值不同时,执行的代码也有所不同,这样可以描述更精确地描述系统的复杂行为。对于扩展后的模型系统,我们进一步给出了一个有界模型检验算法。该算法使用深度优先的方式搜索所有的可行路径,并在遍历过程中使用SMT实现了对时间约束和规约的处理。