安全关键软件的AADL模型自动逆向构造方法

邱志凯，杨志斌，谢 健，周 勇，程高辉，陈俊文

1(南京航空航天大学 计算机科学与技术学院，南京 211106) 2(高安全系统的软件开发与验证技术工信部重点实验室，南京 211106) 3(北京控制与电子技术研究所，北京 100038)

1 引 言

安全关键软件(Safety-Critical Software，SCS)[1]是指应用于航空、航天、能源等领域的安全关键系统中，且其运行情况可能引起系统处于危险状态，从而导致财产损失、环境破坏或者人员伤害的一类软件.即，安全关键软件一般为安全关键系统的一部分，它可能引起或者助长不安全的条件，这类软件被认为是安全关键的[2].

模型驱动开发方法(Model-Driven Development，MDD)[3]是一种由对象管理组织(Object Management Group，OMG)提出的基于抽象模型的软件开发方法，该方法具有通用性、可扩展性、可重用性等特点.近年来，模型驱动开发方法逐渐成为安全关键软件开发方法的一种发展趋势，例如国际民航领域使用的机载系统适航审定中的软件开发标准DO-178C[4]就将模型驱动和形式化方法作为其核心标准的重要技术补充.在实际开发过程中，构造模型的途径主要有两种：从需求中构造模型，即正向构造[5]；从代码中构造模型，即逆向构造.在安全关键软件系统开发与维护过程中，部分需求与设计信息往往遗留在源代码中，使用逆向工程将这部分遗留信息从代码中构造到设计模型是十分重要的.

模型驱动的逆向工程(Model-DrivenReverse Engineering，MDRE)是逆向工程领域的一个分支，Favre等人[6]将MDRE定义成“从已经存在的系统中构造描述性模型”.通常来说，MDRE一般包括两步：模型发现和模型理解.MDRE的信息来源包括源代码、二进制代码、API等等多种形式，因此，MDRE是从较低抽象级别的系统模型开始，构造更高抽象级别的视图.相比传统的逆向工程，MDRE继承了模型驱动开发的特点，并具有两个优势：首先，模型构造过程是自动化的，可以对逆向过程进行控制；其次，逆向结果为模型，从而可以分析逆向模型的质量[7].近年来，MDRE也逐渐受到安全关键系统领域的重视和应用，例如适航认证标准DO-178C和DO-254[8]将MDRE作为其重要的技术补充.

我们将MDRE已有研究分为两类：面向通用领域和面向特定领域的逆向构造方法.在通用的模型逆向构造方法方面，Bruneliere[9]等提出MoDisco，MoDisco是一个支持系统模型驱动逆向工程的Eclipse开源项目，为历史遗留系统的理解分析、演化、质量保障等工作提供了支持.在特定领域的模型逆向构造方法方面，在安卓系统领域，Nirumand A[10]提出了一个基于模型驱动逆向工程框架(VAnDroid)，该框架会自动提取Android应用程序中一些与安全有关的信息，并将其表示为特定领域的模型，可以识别通信相关的安全风险和漏洞.

安全关键系统领域常用的建模语言有UML[11]、SysML[12]、EAST-ADL[13]和AADL[14]等.AADL采用统一模型支持多种分析的方式，支持对安全关键嵌入式系统的软硬件混合建模，是一种非常适用于安全关键系统的体系结构建模与分析语言.目前AADL正向代码自动生成方面有较多的研究，例如，OCARINA[15]和RAMSES[16]等工具支持AADL模型到C、Ada、Java的代码自动生成.在逆向工程方面，商业工具STOOD和AADL Inspector支持C/Ada到AADL模型的逆向构造，但并未给出具体逆向方法和规则；Lesovoy[17]等人提出了一种从ARINC 653软件源代码中提取AADL模型的方法，该方法主要面向综合化航空电子设备(IMA)系统；Bordin[18]等人提出了一种Ada spark到AADL模型双向转换方法，该方法为了解决异构系统集成时的完整性验证.

本文提出一种C代码到AADL模型逆向构造方法——C2AADL.安全关键软件常需要考虑安全编码规范，因此，我们考虑安全C子集-MISRAC[19].另外，由于源代码往往运行在各种嵌入式平台上，所以逆向工程需要处理静态结构、动态运行时、功能行为等信息.尤其是，随着多核处理器在未来安全关键软件中广泛使用，多线程同步互斥、通信、线程调度和安全编码规范等关键信息的逆向构造成为重要难题.相比已有的AADL逆向构造方法，本文更为完整地考虑了AADL构件结构、行为、多线程运行时信息和安全编码规范等多个方面的逆向构造.

2 研究背景

2.1 AADL

2004 年，美国汽车工程师协会 SAE(Society of Automotive Engineers)在MetaH、UML 等语言的基础上，提出嵌入式实时系统体系结构分析与设计语言 AADL(Architecture Analysis & Design Language)，并发布为 SAE AS5506 标准.AADL采用单一模型支持多种分析的方式，支持对安全关键嵌入式系统的软硬件混合建模，是一种非常适用于安全关键系统的体系结构建模与分析语言.

安全关键系统是一种将硬件平台、软件和运行时环境深度融合的复杂系统，而AADL是一种基于构件(Component)的软硬件建模语言，并与之对应的提供了硬件、软件、执行模型3种建模概念，核心构件如图1所示.

图1 AADL基本建模概念Fig.1 AADL basic modeling concepts

在AADL核心构件的基础上，AADL还提供了两种扩展机制，分别是基于自定义属性集(Property Set)的扩展和基于附件(Annex)的扩展.构件内部的功能行为描述可以通过AADL Behavior Annex[20]、C和Ada实现.Behavior Annex与执行模型有密切的关系：执行模型的分发机制定义了线程、子程序周期性或非周期性地读取数据、计算、发送数据，BA则是对计算状态内的执行行为进行详细刻画.

2.2 MISRA C

MISRA C是由汽车工业软件可靠性协会 (The Motor Industry Software Reliability Association，MISRA)提出的嵌入式C语言开发标准，目的是提高嵌入式系统的安全性、可读性和可移植性.

在MISRAC：2012中，共有159条规则和指令，其中规则143条，指令16条.而这些指令和规则又分为5个类：建议规则、建议指令、必要规则、必要指令和强制规则.任何符合MISRAC：2012编程规范的代码都应该严格地遵循强制规则的要求，需要遵循必要指令/规则(如果背离，需要注明背离原因)，并应该在条件允许的情况下尽可能符合建议规则/指令.表1列出部分安全编码规范内容.

表1 安全编码规范Table 1 Secure coding standards

3 逆向构造方法

C2AADL逆向构造方法的总体框架如图2所示，主要分为4个部分：

1)源码解析：将输入的多线程C代码转换为抽象语法树，抽象语法树中包含了源码的结构和行为信息，运行时性质则包含在具体的语句中；

2) 中间模型提取：源码解析的抽象语法树和安全编码规范作为输入，根据本文提出的转换规则，将规则所需要的结构、行为、运行时性质和安全编码规范信息从输入中提取到中间模型；

3) AADL模型生成：包含了源码结构、行为、运行时信息的中间模型作为输入，根据转换规则将中间模型的元素与AADL模型之间进行对应转换.

4)模型验证：在逆向构造之后，可以基于模型检测工具UPPAAL[21]和组合验证工具AGREE[22]对AADL模型进行形式化验证.

图2 C2AADL框架Fig.2 Framework of C2AADL

本文主要给出前3步从源代码的AADL模型的逆向构造工作.

3.1 源语言分析

本节将介绍基于抽象语法树提取的C程序的对象文档模型(Document Object Model，DOM)，在Eclipse C/C++开发工具(CDT)中DOM的思想被用来在CDT程序内部存储C/C++文档，使用CDT对C代码进行解析得到的抽象语法树，而MISRAC是一种安全编码的规范，其属性已包含在源码中，即也包含在抽象语法树中.图3给出了一个CDTDOM解析的例子，下面对抽象语法树3个层次进行说明，即程序组织结构、单文件结构和函数模块.

1)程序组织结构：抽象语法树中最顶层元素ICModel表示整个环境的workspace；ICModel包含ICContainer和ICProject，分别表示workspace中的工程和文件组；ICProject包含一个或多个ISourceRoot表示工程空间中的文件组织结构；每个ISourceRoot中可以包含一个或多个ITranslationUnit，表示单个C程序文件.ITranslationUnit是DOM模型中最重要的元素，每一个ITranslationUnit都包含源文件中的多种程序组成，如宏定义、声明、实现等；

2)单文件结构：在ITranslationUnit中包含一个或多个IASTDeclaration，IASTDeclaration可以是函数的头部声明，例如IInclude、IUsing和INamespace等，也可以是对程序文件内的函数、变量等的声明，例如IASTFunctionDefinition和IASTSimpleDeclaration等；

3)函数模块：函数声明IASTFunctionDefinition主要有4部分：IASTDeclSpecifier、IASTFunctionDeclarator和IASTCompoundStatement.IASTDeclSpecifier表示函数返回值类型；IASTFunctionDeclarator包含IASTName和IASTParameterDeclaration，分别表示函数名和函数参数；IASTCompoundStatement由一组IASTStatement组成表示函数的具体内容，IASTStatement可以是多种Statement的实现，例如IASTIfStatement、IASTForStatement、IASTSwitchStatement、IASTWhileStatement和IASTReturnStatement等.

图3 CDT DOM 解析Fig.3 CDT DOM parsing

3.2 转换规则

在源码分析的基础上，本节给出源代码到AADL模型转换的转换规则.转换规则为C到AADL的逆向构造提供了映射关系，而中间模型是C到AADL实现的桥梁.源码结构的转换规则包括：全局变量、局部变量、复合数据类型、线程和函数结构；源码行为的转换规则包括：赋值语句、分支语句、循环语句以及函数调用；源码运行时性质转换规则包括：多线程通信、多线程同步、多线程调度以及安全编码规范.

3.2.1 结构转换规则

结构方面的转换规则主要包括：基本数据类型和复合数据类型的变量到AADLData组件的转换、函数模块到AADLSubprogram组件的转换、任务模块到AADLThread组件的转换.

由于C语言中的变量和AADL中的数据组件对数据类型的描述相似，因此我们将变量映射到数据组件.为了使AADL的结构更清晰，我们将数据组件封装为两种类型的包：一个包表示名为Base_Types的基本数据类型，另一个包表示名为User_Define的扩展数据类型(复合数据类型).通常，对于基本数据类型，使用数据声明(Data)对应用程序数据建模就足够了，并且不必声明数据实现(Data Implementation).对于具有内部实现的扩展数据类型，扩展数据的元素映射到数据实现中声明的子组件.C语言的函数和任务模块分别映射到AADLsubprogram和thread组件.具体的转换规则如表2所示.

表2 结构转换规则Table 2 Transformation rules of structure

由于本文篇幅所限，表2中仅列出了一部分数据类型.例如，它不包括由unsigned和signed声明的数据类型.映射规则应考虑在标准C和Code Composer Studio(CCS)中定义的所有数据类型.如表2所示，对于没有内部元素的基本数据类型，相应的数据组件仅具有数据类型；对于具有内部元素的扩展数据类型，相应的数据组件具有数据声明以及数据实现.C语言定义了一种特殊的类型，称为“指针”.对于表2中所示的指针数据类型，我们将指针指向的数据类型视为数据组件类型.

在CCS中，多任务(TASK)代表执行的并发路径，而AADL中的线程组件是顺序执行的并发可调度单元.多个线程代表并发执行路径.可以将各种执行属性分配给线程，包括定时(例如，最坏情况下的执行时间)，调度协议(例如，周期性，非周期性等)，内存大小和处理器绑定.因此我们将任务(TASK)映射到AADLthread组件.除任务外，常规功能在CCS中使用函数定义.函数表示顺序执行，可以由多个任务调用，并且它们应该是可重用的.AADL中的subprogram组件表示顺序可执行的源文本，该组件是一个带有(不带有)参数的可调用组件，为调用它的组件提供服务功能.基于函数和子程序组件之间的相似语义，我们将函数映射到子程序组件.

3.2.2 行为转换规则

函数和线程执行行为主要由一系列语句(例如，顺序语句、分支语句、循环语句等)按照特定的顺序执行实现，关于行为的转换规则主要介绍顺序语句、if条件语句、switch分支语句、for循环语句、while循环语句，函数调用语句等到AADL行为附件的转换.

AADL行为附件对于行为的描述如图4上方所示，其中states表示执行过程所需的所有状态，transitions中si表示源状态，sj表示目的状态，guard表示状态转移的条件，action表示状态转移时执行的动作.为了更好的展示转换规则，我们将AADL行为附件的描述内容显示为状态机，状态转移线上表示守卫条件，线下表示执行动作.具体的转换规则如图4所示.

图4 行为转换规则Fig.4 Transformation rules of behavior

源语言中顺序语句一般由操作数和操作符组成.源语言操作数的名称对应于AADL行为附件动作中的数据名称；源语言操作符转换到AADL模型操作符号，例如：“=”转换为“：=”、“！”转换为“not”等.

源语言的If条件语句在转换到AADL模型时的关键信息是：If语句的判断条件和判断满足后的执行内容.其中If判断条件转换到AADL行为附件中状态迁移的守卫条件，执行内容转换到AADL状态转移守卫条件满足后的动作.

源语言Switch-Case语句的关键信息包括3部分：Switch中的控制表达式、Case中的表达式以及每个Case后的动作.Switch中的控制表达式和Case中的表达式使用等号连接成一个AADL状态转移的守卫条件，每个Case后的动作对应每个AADL状态迁移时的执行内容.源语言Switch-Case语句对应的所有AADL状态转移的起始状态相同，终止状态也相同.

源语言的for循环语句主要关注4个点：初始化表达式、循环条件、迭代表达式以及循环内容.其中源语言初始化表达式对应AADL行为附件循环前的一个状态转移的动作；循环条件对应AADL行为附件循环状态迁移的守卫条件；循环内容对应于AADL循环状态迁移的动作；迭代表达式对应行为附件执行动作最后的动作.

源语言的While循环关键信息是循环判断条件，While循环语句转换到AADL行为附件中的状态迁移，其中该状态迁移的起始状态和目的状态相同，状态迁移条件是While循环判断条件.

函数调用语句的关键信息分为3部分：函数名称，输入参数名称和接收返回值的变量名称.源语言的函数名称转换到AADL子程序名称，注意AADL子程序名称后需要加！，表示子程序调用；源语言的输入参数名称按顺序对应于AADL子程序调用的输入参数名称；源语言接收返回值的变量对应AADL子程序调用括号最后的参数.

3.2.3 运行时转换规则

运行时的转换规则主要考虑所使用平台的API和安全编码规范到AADL模型的转换，因此转换规则会展示一部分平台的API.运行时的转换规则主要包括：多线程通信、多线程调度、多线程同步以及安全编码规范.为了方便展示转换规则，图5顶部展示了在osate工具中AADL文本模型对应的可视化图形，具体转换规则如图5所示.

图5 运行时性质转换规则Fig.5 Transformation rules of runtime

线程间通信主要包含3种方式：共享数据、数据传输和事件(信号).共享数据是使用全局变量实现的，线程通过读取和写入全局变量进行通信；数据传输是通过邮箱队列实现，数据发送者可以将数据发送到队列，而数据接收者可以从队列中获取数据；事件通知通过发送信号量来实现，信号量是二进制数据.图5所示的3种通信方式转换规则：a)表示共享数据转换规则，源代码中进出队函数通过共享变量操作队列数据，其中队列数据为全局变量，对应生成的AADL模型在进程中包含这两个函数和全局变量，并通过Data Access将全局变量与两个函数进行连接；b)表示通知信号转换规则，源代码中两个线程通过发送和接收signal信号实现通信，对应生成的AADL模型在进程包含这两个线程，并通过端口连接将两个线程的信号收发端口连接，二进制信号对应AADL模型Event端口；c)表示数据传输转转换规则，源代码中消息发送线程通过邮箱机制将数据发送接受任务，生成的AADL模型中进程包含两个线程，并使用端口连接将发送端口与接收端口连接，该端口为Data端口.

在CCS SYS/BIOS中使用信号量和邮箱机制实现线程之间的调度，信号量转换规则如图5中(d)所示，源代码线程在等待信号量时，则线程挂起，收到信号量后恢复执行，在AADL中对应于On Dispatch从Complete状态(图中虚线椭圆状态)转移到执行状态.邮箱机制转换规则中源代码线程在等待邮箱数据时线程挂机，等待数据到来后，线程恢复执行，对应于AADL模型中On Dispatch从Complete状态到执行状态的转换，并在状态转移时读出端口数据.

表3 编码规范转换规则Table 3 Transformation rules of coding standards

安全编码规范通过AADL属性集表达，属于执行模型的一部分.表3中的安全编码规范与源码属性相关，指定函数/变量性质的规范转换为AADL属性集，并和相应的构件进行绑定.关于安全编码规范的转换规则与上述转换规则有所不同，首先给出MISRA C中规范的定义，然后给出该规范对应的AADL属性集，最后给出案例中使用到该规范的源码，并给出转换到AADL构件时的属性绑定.

4 原型工具

本节首先介绍便于C代码信息提取和AADL模型生成的中间模型，然后介绍原型工具C2AADL设计实现.

4.1 中间模型

在处理C程序的过程中，程序多种元素往往耦合紧密，为了能够在转换到AADL模型前将模型尽可能简化，屏蔽转换过程中不关心的组成成分，本小节基于C代码和AADL模型特征提出一个C到AADL转换的中间模型-CAInterM，如图6所示.中间模型的结构与C语言项目结构一致，一个C语言工程包含若干个源文件，每个源文件包含全局变量和函数，每个函数包含自己的局部变量和函数行为等.图6中CProjectModel存储了项目名称信息(Name)、项目文件结构信息(CModules)和项目用到的编码规范(properties)，其中CModules包含了全部的程序文件信息(SingleCModel).SingleCModel是单个文件的存储体，包含了一个相同文件名的.c和.h文件定义的全局变量(GlobalVars)、函数(Functions)、数据类型(Datas)和引用的文件(Includes).FunctionModel是对函数内容的记载，它包含函数名称(Name)、输入参数(Paras)、返回值(ReturnValue)、局部变量(LocalVars)、引用的变量(Data Access)和函数行为(StateList).DataModel是对定义的复合数据类型信息的存储，它包含定义的复合数据类型的名称(Name)、复合数据类型内部变量(Vars)和函数(Subs).考虑AADL模型特征设计中间模型的具体内容，Statement是对源码函数行为的记载，包括AADL行为附件中状态迁移所需的初始状态、目的状态、守卫条件和执行内容；VarModel是对源码局部变量和复合数据类型成员变量的记载，包括AADL数据构件所需的变量名称、变量类型、变量来源以及变量初始值；ConnectionModel记录源码线程/函数间使用全局变量或端口的通信，包括了AADL构件连接所需的源、目的和数据/端口名；MISRACModel记录了安全编码规范对应的属性名称，属性类型以及属性绑定的组件.

图6 中间模型：CAInterMFig.6 Intermediate model： CAInterM

设计该中间模型的意义在于：1)减少转换过程中需要考虑的信息量；2)将C程序模型保存成层次化结构，易于转换；3)保证了本文所提转转换方法的可扩展性.表4给出C语言抽象语法树到中间模型的映射关系.

表4 抽象语法树到中间模型映射Table 4 Mapping from AST to intermediate model

4.2 工具实现

C2AADL模型逆向构造工具是基于Java编程实现的.整个模型逆向构造工具框架如图7所示，工具采用模块化思想，包括源代码到中间模型抽取、安全编码规范到中间模型的抽取和AADL模型生成.本节主要介绍C2AADL模型逆向构造工具的实现.

图7 C2AADL工具框架Fig.7 Framework of C2AADL tool

模型逆向构造工具功能模块的主要步骤及其对应的Java代码数量统计见表5.

表5 C2AADL模型逆向构造工具主要步骤Table 5 Main steps of the model reverse construction tool

工具开发环境为基于Eclipse平台的Osate插件环境.将需要进行逆向转换的项目导入工具后，右击导入的项目启动逆向转换功能，可以在工具内对导入的项目文件内容进行修改调整，并查看生成的AADL模型.

5 案例研究

针对雷达信息处理子系统案例，首先使用本文实现的工具对该案例进行逆向模型构造，并对逆向结果进行分析，其次将本文实现的方法和相关MDRE方法进行分析比较得出结论，最后分析C2AADL方法的效性.

5.1 案例介绍

雷达信息处理子系统是指使用调制的波形和定向天线向空间中的特定空域发射电磁波，从接收的回波中提取制导信息的系统.雷达信息处理子系统功能分解，主要包括3层：DSP平台层、系统控制层和SAR(Synthetic Aperture Radar)实现层.DSP平台层主要采用多核DSP处理器，包括UART通信、1553B总线通信、以太网通信、AD采集、SRIO通信和核间通信模块；系统控制层主要是模式转换和任务调度，包括：前端分机控制、任务控制和参数装定模块；SAR实现层利用合成孔径原理实现高分辨的微波成像，包括：信号预处理模块、图像处理模块和匹配处理模块.

雷达信息处理子系统使用在机载SAR雷达中，该系统利用飞机平台的飞行路径，合成一个等效的“大天线”，并生成高分辨率的遥感影像.在每个发送/接收周期，对来自合成孔径元件上连续脉冲信号的幅度和相位进行处理，获取的数据存储在存储器中.在给定周期数后，将存储的数据重新组合，以创建正在飞越地形的高分辨率图像.

雷达信息处理子系统主要包括3层的主要功能如下：

·DSP平台层主要功能：不同DSP之间的板间通信和多核DSP中的核间通信、以太网和异步收发器与系统层之间的通信、串行多路数据总线通信和从AD芯片上采集需要量化的信号；

·系统实现层主要功能：根据指令选择SAR工作模型，控制各分机工作(任务控制功能)；各分机启动自检开始信号采集工作(前端分机控制)；将收集的数据重新组合装定完成量化处理(参数装定)；

·SAR实现层主要功能：处理从位置A到D时间段T内所有雷达所返回的信号(信号预处理)；合成预处理信号，从而延长天线长度，实现更高分辨率(图像处理)；当目标进入雷达波束，将目标与雷达图像相结合，完成目标匹配(匹配处理).

图8 任务控制功能分解Fig.8 Functional decomposition of task control

本文主要考虑系统控制层的任务控制功能里12个任务间相互调度和通信.具体任务的主要功能流程如图8所示：Task1接收到1553中断后解析1553消息，然后将控制指令发送给主控任务Task0；Task0根据控制指令后进行判断，将系统参数发送给Task4，启动前端分机自检，或者将子图分发给Task8～Task14，启动子图处理；Task8-14处理完毕后将子图发送给Task3，其中Task8同时兼有编排遥测数据，启动遥测数据传输任务的功能；Task3接收Task8-14发送的子图后进行拼接，并完成量化处理.

5.2 案例分析

本文的案例分析旨在回答以下两个研究问题：

1)RQ1.本文方法的有效性如何？RQ1旨在调查本文方法在应用到大型工业界案例时是否具有实际的价值，我们通过一个雷达信息处理子系统对此进行评估.

2)RQ2.与其他工具相比，本文所提出的工具有哪些优势？RQ2通过由现有其他逆向构造方法的转换进行比较，我们可以得出本文所提方法的优点.

本文从系统层面，单构件行为层面和多构件同步调度层面对生成的雷达AADL模型进行分析：

系统层：逆向构造的AADL模型中，整个任务控制功能对应一个顶层系统构件System.该功能中的其他内容对应相应的Subprogram，Process，Data，Thread等构件，其中一个比较特殊的函数是Main函数，它对应一个Process构件，程序的执行顺序通过函数调用和线程调度表达.如图9(a)所示是构造的任务控制功能的顶层框架：一个系统中的主进程；主进程中包含主控系统的所有线程、全局变量以及数据连接和端口连接.所生成的AADL模型框架架构与案例介绍时图11的框架一致.

图9 逆向生成的AADL模型Fig.9 Generated AADL models

单构件行为层：在结构和行为的分析中，以任务控制功能中通信时消息队列出队模块为例.图9(b)所示的代码中InterCoreDequeue函数转换到AADL模型对应Subprogram构件，其中函数输入参数转换成了Subprogram构件的In Parameter，安全编码的属性集也与Out Parameter进行了绑定，函数的执行内容构造在子程序的行为附件里，其中包含了共享数据访问、顺序表达式、If条件句和Return语句等.

多构件同步调度层：多线程的运行时重点在于线程的运行状态，线程在状态迁移时Complete状态用于表示线程挂起等待被调度.当线程等待的端口接收到信息后，转换到执行状态.由于有端口的存在，线程构件也有用于通信的端口连接.图9(c)所示任务控制功能中Task0检查为例，该任务初始状态为Complete状态等待信号Sync的到来，接收信号后调度执行，运行过程中会等待1553信号解析后的数据，并根据数据内容判断启动自检、设置时间、雷达扫描功能.

生成的AADL模型减少了相关研究人员理解项目所需的时间，可以补充因长时间开发所造成的文档缺失，并为进一步基于模型驱动的开发提供了源模型.

RQ1：通过完整的代码分析以及AADL模型逆向构造，我们可以看出，本方法对于复杂结构的工业级系统有良好的支持，模型构造过程自动化.

表6为雷达信息处理子系统的AADL模型数据统计，AADL模型元素分为3个部分：

表6 AADL模型统计Table 6 AADL model statistics

1)描述静态功能架构的模型元素，涉及整个系统中的System、Process、Thread、Subprogram和Data元素；

2)描述系统动态行为的元素，涉及线程函数中的Subprogram Implementation、Thread Implementation和BA；

3)描述非功能属性的元素，涉及源码编码规范的Property Set.

RQ2：我们将C2AADL与MDRE领域中的方法进行了比较，表7中利用4个参数进行此比较，即输入、输出、可以分析的类型(结构、行为、执行模型)和工具.

评估结果如表7所示.在MDRE方法[9，10，25，26，28]中，研究人员仅关注源代码的结构；在文献[23，24，27，29]中相比上述方法更关注了源码的行为信息.而C2AADL比较完整地支持处理遗留系统的结构、行为和运行时性质的逆向构造，并且在模型中绑定属性集表示编码规范使AADL模型更加精确.

表7 MDRE工具和方法评价Table 7 Evaluation of MDRE tools and methods

6 结束语

安全关键系统开发过程中，源代码中所包含的部分设计信息未能及时补充到设计模型，如何将源码信息自动构造到设计模型中是该领域的研究热点.本文提出了一种基于源代码的AADL模型自动逆向构造方法和工具.首先将C语言程序转换为抽象语法树，获取源码中的设计信息；然后将源码使用到的编码规范和抽象语法树作为输入，并按照转换规则所需的信息生成逆向转换的中间模型；最后将中间模型按照转换规则生成AADL基本构件、行为附件和属性集.通过对使用多任务的雷达信息控制子系统的逆向构造验证了本方法的有效性.

在未来的工作中，我们将进一步开展以下几个方面的研究工作：

1)源代码中无法显式表达软件系统的非功能属性(例如周期、执行时间、资源分配等).目前我们正在基于第三方工具(例如WCET分析工具)，测出软件执行时间和周期等信息，并将这些属性添加到相应的AADL模型中；

2)在软件开发过程中，Assertion是一种经典的调试和测试方法.在编程中是指对某种假设条件进行检测，如果条件成立就不进行任何操作，如果条件不成立就捕捉到这种错误，并打印出错误信息，终止程序执行.目前我们正在考虑将带Assertion的C语言转换到AADL Bless Annex[30]，目的是为了对行为附件进行验证；

3)模型转换的正确性是模型驱动开发方法成功的关键，目前我们正在基于模型检测工具UPPAAL和组合验证工具 AGREE对逆向构造的AADL模型进行形式化验证.