随着科学技术和人工智能的飞速发展,智能化的大型复杂系统已经普遍出现在人类的生产生活当中,在系统运行的过程中,无论规模的大小,都可能会发生故障,而一个很小的故障有可能引起无法估量的损失。为了避免这种情况的发生,故障诊断应运而生。一直以来,故障诊断在复杂的自动控制领域中都是一个严峻的挑战和课题,它的效率决定于系统特性,即可诊断性。可诊断性决定了一个系统在一系列有效可观测序列内能否检测出错误发生的能力。自故障诊断提出以来,得到了学者的广泛关注与研究,并取得了丰硕的研究成果。大量的文献用基于模型诊断(Model-Based Diagnosis,MBD)的方法对离散事件系统(Discrete Event System,DES)的可诊断性做出了分析。在MBD中,可以根据模型逻辑推导出系统的预期行为,同时,可以通过布置在系统中的各种传感器来监测在同样的输入条件下,系统产生的实际行为,然后将预期行为和实际行为进行比较,根据其差异可以得到系统可诊断性的判定结果。但是到目前为止,很少有研究人员针对实时系统(Real-Time System,RTS)研究其可诊断性,因为在实时系统中,有很多的时间约束,导致系统建模困难。在现实生活中,这些时间约束,比如传输延迟、通讯时间和响应时间等都必须被考虑到,它们会影响系统的可诊断性,因此是不能被忽视的。本文主要从两个方面来研究RTS中的有界可诊断性问题。首先,本文考虑到实时系统中的时间约束对系统的影响,引入时间自动机(Timed Automata,TA)对实时系统进行建模。时间自动机是由Alur和David在1994年提出的,可以充分表达时间约束,这是研究实时系统时运用最广泛的工具,在时间自动机中,不同属性事件之间的延迟很容易被表达。同时,采用MBD的方法,用一个六元组的TA对RTS进行建模并分析,类比于离散事件系统的可诊断性,将RTS中的可诊断性概念进行重定义,并通过定义时间关键对的存在来证明系统的可诊断性,说明了在RTS中,满足可诊断性的充分必要条件并作出证明。其次,本文提出基于可满足性模理论(Satisfiability Modulo Theories,SMT)的可诊断性检验方法,在时间自动机上对实时系统的有界可诊断性进行验证。在SMT解决器中,主要通过对时间自动机和满足系统可诊断性的充分必要条件进行编码,来验证系统的可诊断性。在用SMT对系统进行验证的过程中,本文把满足可诊断性的充分必要条件和系统特性根据不同性质,详细划分为12条子规则,并定义了等价路径的概念,在等价路径上对待诊断系统进行判定。在具体判定过程中,把满足可诊断性的条件作为SMT中的背景理论部分,把待诊段系统作为输入得到判定结果。最后,本文选用SMT解决器Z3,运用控制变量法,在标准的实验基准HAVC系统上设置三组对照试验,分别讨论了在单个时钟、多时钟和不同规模的系统下算法的表现,并分析了实验用时、占用内存等情况,证明了本文算法的可行性和高效性。