● 摘要
安全关键实时系统广泛应用于航空电子、航天器、武器装备、核能、汽车控制等关键信息领域。由于功能和非功能要求不断提高，系统的复杂度急剧增加，如何设计与实现高质量的安全关键实时系统，并有效控制开发时间和成本，是学术界和工业界共同面临的难题。近年来，模型驱动开发方法逐渐成为安全关键实时系统设计与开发的重要手段，而作为复杂嵌入式实时系统的体系结构设计与分析语言标准，AADL(Architecture Analysis and Design Language)日益受到关注，并逐渐发展成为一个新的研究热点。 AADL语言提供了一种标准、全面的方式，对安全关键实时系统的软/硬件体系结构、运行时环境、功能以及非功能属性进行表达，而对AADL模型进行形式验证与分析是实现高可信安全关键实时系统的一个关键环节。本文的工作正是围绕这一重要研究问题展开的。目前，模型转换是AADL模型形式验证与分析的主要途径，如转换到BIP(Behavior Interaction Priority)、Fiacre、动作时序逻辑TLA+、同步语言等，目的是为了重用这些形式模型上已有的验证和分析能力。然而，其关键问题在于：(1) 对AADL标准定义的语义是否有清晰和正确的理解，这是AADL模型转换的基础，然而，AADL大部分语义是非形式化的；(2) AADL模型转换是否正确或有效，即AADL语义在模型转换中是否得到保持；(3) AADL模型上满足的验证性质，在目标模型上是否也满足，反之亦然，即用户期望验证的性质在模型转换中是否得到保持。 本文提出了一种新的AADL模型形式验证与分析方法，重点研究了AADL形式转换语义、AADL模型转换的语义保持证明方法以及AADL模型转换的验证性质保持证明方法三个关键问题，并设计和开发了一体化的AADL建模与验证平台。主要研究成果如下： (1)针对“大部分AADL转换语义研究不够完整和形式化，且较少关注资源行为的表达”的问题，提出了一种基于时间抽象状态机(Timed Abstract State Machine, TASM)的AADL形式转换语义框架－AADL2TASM。针对一个较为完整的AADL研究子集，给出了研究子集的形式定义和抽象语法，给出了TASM的抽象语法及其操作语义，并基于语义函数和类ML的元语言形式定义转换语义规则。与已有AADL转换语义研究相比，该框架具有较为完整的AADL研究子集、较强的目标语言表达能力以及对对象语言、目标语言和转换语义规则精确描述等优点。 (2)针对“已有AADL模型转换较少进行语义保持证明”的问题，提出了一种基于双版本形式语义的AADL模型转换的语义保持证明方法－ASemPre。给出了时间变迁系统(Timed Transition System, TTS)及其操作的定义；和形式转换语义对应，基于TTS以操作语义的方式给出了相应AADL研究子集的语义，作为语义保持证明的一个前提，同时，将转换语义定义中的TASM表示和TASM语言本身的操作语义进行组合，构成TTS，作为语义保持证明的另一个前提，最后，证明了两个TTS满足模拟等价关系(Simulation Equivalence)，即AADL研究子集的语义在AADL到TASM的模型转换中得到保持，为了提高证明的可信度，基于定理证明器Coq对相关定理进行了证明。该方法克服了已有AADL模型转换研究中仅采用手工确认或者假设语义是保持的缺点，从理论上证明了AADL研究子集的语义在AADL到TASM的模型转换中得到保持。 (3)针对“已有AADL模型验证与分析方法较少进行验证性质保持证明”的问题，提出了AADL模型到TASM模型的验证性质保持证明方法－AVerPre。给出了考虑原子命题的时间变迁系统及其操作的定义；给出了时序逻辑ACTL、ECTL的语法和语义；给出了一种比较通用的验证性质保持的证明思路，其关键在于原子命题、原子命题的满足关系和原子命题的映射关系的定义以及原子命题满足关系保持的证明，基于结构归纳法，从而整个性质得到保持。证明结果表明，本文提出的AADL到TASM的模型转换满足模拟等价关系，且原子命题的满足关系得到保持，因此，使用时序逻辑ACTLUECTL表达的无死锁性、安全性、活性、实时性质以及资源性质能够得到保持。同时，基于定理证明器Coq对相关定理进行了证明。 (4)在上述理论工作的基础上，设计并实现了AADL建模与验证平台－CertA2T，同时，基于航天器导航、制导与控制系统(Guidance, Navigation and Control, GNC)进行了实例性验证，由于GNC系统非常复杂，提出了分层建模方法，包括系统与子系统层、任务层和行为层三个层次，并且详细讨论了如何使用CertA2T平台对AADL模型进行验证和分析。