面向航空关键系统的AADL转换语义及其特性保持证明研究

航空航天等领域的嵌入式实时系统日趋复杂，由于分式结构以及模式变换、分区等机制的引入，给系统性质验证和分析带来了新的挑战。AADL是近年提出来的一种嵌入式实时系统体系结构分析与设计语言国际标准。当前，AADL模型验证、分析以及自动代码生成，主要是采用模型转换方式，而精确的转换语义及其特性保持是模型转换的基础。课题提出了一种基于时间抽象状态机(TASM)的AADL转换语义方法，形式化刻画AADL和时间抽象状态机的抽象语法、类型系统及操作语义，使转换语义更加精确、抽象；提出了一种基于定理证明器Coq的AADL特性保持证明方法，采用Coq对AADL转换语义进行重写，提供通用的AADL语义基础，并给出特性保持的证明；研究该转换语义模型的可调度、资源优化等关键性质验证和分析方法；最后，基于模型转换语言ATL实现AADL模型到TASM模型的自动转换，构建一体化的验证与分析框架。

航空航天等领域的嵌入式实时系统是一种安全关键实时系统，如何设计与实现高质量的安全关键实时系统，是学术界和工业界共同面临的难题。作为复杂嵌入式实时系统的体系结构设计与分析语言标准，AADL已成为一个新的研究热点,而对AADL模型进行形式验证与分析是实现高可信安全关键实时系统的一个关键环节。目前，模型转换是AADL验证与分析的主要途径。其关键问题在于：（1）对AADL标准定义的语义是否有清晰和正确的理解；（2）AADL语义在模型转换中是否得到保持；（3）用户期望验证的性质在模型转换中是否得到保持。.本项目提出了一种新的AADL模型形式验证与分析方法，重点研究了AADL形式转换语义、AADL模型转换的语义保持以及验证性质保持证明（合称为特性保持）方法三个关键问题，并设计和开发了一体化的AADL建模与验证框架。主要研究成果如下：.（1）提出了一种基于时间抽象状态机（Timed Abstract State Machine，TASM）的AADL 形式转换语义框架－AADL2TASM。针对一个较为完整的AADL研究子集，给出了研究子集的形式定义和抽象语法，给出了TASM 的抽象语法及其操作语义，并基于语义函数和类ML的元语言形式定义转换语义规则。.（2）提出了一种基于双版本形式语义的AADL 模型转换的语义保持证明方法。给出了时间变迁系统TTS及其操作的定义；和形式转换语义对应，基于TTS以操作语义的方式给出了相应AADL 研究子集的语义；同时，将转换语义定义中的TASM表示和TASM语言本身的操作语义进行组合，构成TTS；最后，通过证明两个TTS满足模拟等价关系，证明了AADL研究子集的语义在AADL到TASM 的模型转换中得到保持。为了提高证明的可信度，基于定理证明器Coq对相关定理进行了证明。.（3）提出了AADL模型到TASM模型的验证性质保持证明方法。给出了考虑原子命题的时间变迁系统及其操作的定义；给出了时序逻辑ACTL、ECTL的语法和语义；给出了一种比较通用的验证性质保持的证明思路，基于结构归纳法，从而整个性质得到保持。因此，使用时序逻辑表达的无死锁性、安全性、实时性质以及资源性质能够得到保持。同时，基于定理证明器Coq对相关定理进行了证明。.（4）在上述理论工作的基础上设计并实现了 AADL 建模与验证框架。同时，基于航天器GNC系统中的子系统进行了实例性验证。