冯思喆,杨志斌,薛 垒
(1.南京航空航天大学计算机科学与技术学院,江苏 南京 211106;2.高安全系统的软件开发与验证技术工信部重点实验室,江苏 南京 211106; 3.上海航天电子技术研究所,上海 201109)
安全关键软件(Safety-Critical Software,SCS)[1]是指在发生系统失效时导致系统处于危险状态,会造成人的生命威胁、财产重大损失以及灾难性环境破坏的一类软件[2]。这类软件广泛应用于航空航天、医疗器械、轨道交通等领域的安全关键系统中[3]。安全关键系统往往具有严格的安全性和可靠性要求[4]。
为了降低这类系统设计与实现的复杂性,模型驱动(Model-Driven)开发方法[5]作为一种高效并且可靠有效的方法得到了工业界的认可并广泛使用。模型驱动方法主要采用抽象模型来对系统架构及其行为建模,并支持逐步迭代精化完善模型,使用验证工具对系统的功能性质进行验证,最后将模型自动转化为目标代码[6]。这个过程确保了生成的代码保留了在模型级别验证过的属性[7],提高了软件研发的可靠性与开发效率[8]。其中,复杂嵌入式体系结构分析和设计语言(Architecture Analysis and Design Language, AADL)[9]作为一种模型驱动开发语言备受关注,并逐渐成为了研究热点。AADL提供了标准并且全面化的方法对安全关键软件及硬件的体系结构、运行时环境、功能及非功能属性的表达[10]。
在AADL代码生成方面,法国巴黎电信学院Lasnier等人[11]提出了面向航空平台代码生成工具OCARINA,支持面向ARINC653的代码生成,平台相关代码是由代码生成器硬编码的方式实现;卡梅隆大学Julien等人[12]提出了面向商业平台的AADL代码生成方法,采用AADL架构和SCADE功能的混合建模,分别生成代码后手工集成到平台上,集成过程不仅繁琐且易出错。工业级的代码是运行在具有不同特性的目标平台上,目前平台相关的代码主要通过手工集成。
在模型驱动工程方面,支持我国航天工业代码自动生成的工作较少,特别是Ada代码的生成。Ada是一种面向安全高可信软件的高安全的多功能综合性语言,具有高安全性、较强的表达能力及高适应性[13]特点,且广泛应用于我国航天工业界。本文研究基于AADL模型的航天嵌入式软件Ada代码自动生成方法,主要内容如下:
1)针对工业界实际案例即卫星姿轨控系统,给出平台相关的AADL建模模型。
2)给出一种AADL到Ada代码自动生成方法,用于将AADL模型映射为平台相关的Ada代码。
3)基于AADL开源工具OSATE实现了面向航天嵌入式软件的AADL模型到Ada代码自动生成工具。对基于该工具所生成的代码进行了航天编码规范检查,并在仿真环境中运行,验证了本文所提方法的有效性。
本文是MACAerospace项目[14-16]中关于AADL模型到Ada代码生成的一部分工作。MACAerospace项目是一个基于AADL建模、分析验证与代码生成的模型驱动方法的研究。该研究提出了一种基于中文限定自然语言的需求建模方法[16],再将需求模型自动转化到AADL模型上[15],通过对AADL模型的精化得到平台相关模型;再通过形式化验证方法完成对平台相关模型的验证与分析;最后对验证后的模型自动生成目标C/Ada代码。MACAerospace项目的总体结构如图1所示。
图1 MACAerospace项目总体结构
AADL是由美国汽车工程师协会SAE在MetaH、UML等的基础上提出的嵌入式实时系统体系结构分析与设计语言,AADL将系统设计、分析、验证、自动代码生成等关键环节融合于统一框架之下[9]。
AADL主要用于描述嵌入式系统的软硬体系结构以及交互通信。通过软件构件、执行平台构件以及系统构件进行建模,其中软件构件(如数据、线程、进程、子程序)用于软件体系结构建模;执行平台构件(如处理器、内存、总线、设备)用于硬件体系结构建模;通过分发协议、调度策略、模式变换协议、通信协议以及分区机制来描述系统的运行时环境,其中模式可以表示线程或子程序内的调用序列或逻辑状态;通过连接(端口链接、参数链接、访问链接)来描述构件之间的交互行为,并引入流来描述系统中信息传输逻辑路径;通过属性来描述构件中的约束,如非功能属性约束、可调度性以及线程周期等约束;通过特征来描述构件功能的接口。当已有属性不能满足用户需求的时候,AADL还提供了扩展附件的能力。
为了支持对组件内部功能行为的描述,法国IRIT研究所提出了行为附件(Behavior Annex)[17]。行为附件通过状态、变迁的形式描述组件内部的行为,其中变迁可以定义触发条件以及变迁后的动作,而条件与动作主要由子程序调用、收发数据、延迟等待、执行时间、异步访问等组成[18]。行为附件增强了构件对实际功能行为的详细描述能力,以很好地支持功能行为验证与代码自动生成。
AOCS(Attitude and Orbit Control System)是一种安全关键的嵌入式系统,它通过控制卫星的飞行姿态以及轨道来保证卫星的飞行任务能按计划完成。该系统被划分为9个部分(如姿态确定、轨道计算、姿态控制、轨道控制等)和124个模块,以及21种模式。图2展示了AOCS系统的结构层次划分,前2层主要用于描述系统架构,最后一层描述系统的行为功能。
图2 AOCS系统架构
本文给出一个姿态轨道控制系统的AADL模型。首先,用AADL对图2中L1和L2系统架构层建模;其次,L3功能行为层中,同步控制流信息模块,基于行为附件BA进行建模;数据流计算模块,用AADL扩展机制将其与SIGNAL[19]同步语言进行异构建模;最后,通过属性集扩展和执行平台构件来描述平台相关方面。表1给出了AOCS系统的AADL建模统计图。
表1 AOCS模型规模图
图3 姿态轨道控制系统AADL模型
首先是平台无关模型,主要描述系统功能方面。图3是使用AADL对AOCS系统的软/硬件体系结构的建模。该系统有4个子系统,通过与硬件设备的交互以捕获数据和发送控制命令。在姿态和轨道的计算系统中,存在着大量的数据流计算用于数据的处理。而在姿态和轨道的控制系统中,通常采用模式来描述飞行状态,并通过模式变迁的方式来控制飞行器的状态。图4给出了AOCS中姿态控制子组件的AADL模型图。该子组件展示了模式及模式的转换,主要有消初偏、捕获地球、停控等待等模式和相应模式下的功能。其功能行为用AADL行为附件BA描述,其描述方式类似于状态机[20]。而功能中存在的数据流计算则使用同步语言SIGNAL建模。
图4 姿态控制子组件AADL模型
其次是平台相关模型M1,主要描述系统在特定平台中的执行方式。工业级代码运行在特定的平台上,功能相同的代码在不同的平台上有不同的表现形式。这些差异主要体现在调度机制(周期性)、任务通信和低级控制设施(设备控制)上[21],故需要将此类信息在AADL模型中捕获。图5展示了一组功能行为在平台上的执行模型;周期性任务轨道数据采集线程会定期采集设备2通过数据端口发送的数据;而非周期性线程设备自检线程则是通过设备1的事件端口来触发。不同的执行方式将造成生成的代码存在差异,这些差异则是在模型阶段中被AADL通过扩展属性集的方式捕获。
图5 平台相关执行模型
AADL2Ada是一种适用于航天工业界嵌入式软件的Ada代码生成方法,生成代码的风格严格遵循航天软件产品Ada编码规范。在系统功能方面,可直接将AADL构件映射到相应的Ada代码生成;在平台相关方面,Ada语言的内部提供了运行时的执行核,支持显式的并发、多任务、同步消息传递及处理低级设施,使得代码无需借助额外的操作系统平台即可直接运行在嵌入式应用上。
AADL2Ada规则主要针对系统架构及行为附件部分生成代码,SIGNAL部分在工作[22]中已完成。首先,给出AADL常用子集到Ada核心语法子集的映射规则:1)体系结构方面,包括系统构件、进程构件、线程构件等软件构件;2)执行模型方面,包括进程执行、模式变换、线程执行、端口通信等执行模型属性;3)扩展附件方面,主要包括行为附件BA。其次,将映射关系模块化[23],并进行模板式的代码生成,如图6所示。
图6 代码转换流程图
AADL模型中,进程构件用于描述软件的系统层及子系统层。系统构件的功能近似于进程构件,映射到代码时作为进程来被描述,故对系统构件与进程构件使用相同的转换规则。AADL进程构件映射为Ada程序中的过程,表2展示了进程构件的详细映射关系。进程构件中的特征描述进程的接口,可以是数据、事件或事件数据端口,故映射为Ada过程的形参。进程中的链接用于描述进程中2个线程之间的交互、线程和进程端口之间的通信以及线程和进程中数据对象之间的交互。
表2 AADL进程构件与Ada映射规则
一个进程中可能会包含若干个并发的线程,多个线程之间相互合作就需要对相应的任务进行同步。为此,Ada提供了会合机制(Rendezvous)。在此机制下,任务可以通过全局变量来通信,这种方式虽然效率高但缺乏安全性。保护类型提供了对数据读写访问的控制,故采用保护类型的方式将链接映射为Ada中的保护类型的对象。接下来给出一个保护类基类模板,在生成对象时,根据指定的属性来实例化保护类以达到适配的目的。基类模板定义如下:
1generictypeElement_Typeisprivate;2packagebase_protectis3protectedtypebase(count:Integer:=0)is4entrysecure;5procedurerelease;6proceduresend(message:Element_Type);7functionreceivereturnElement_Type;8private9current_count:Integer:=count;10values:Element_Type;11endbase;12endbase_protect;
其中,第9行的变量用于描述当前的保护状态,并由第4行和第5行的代码来控制。其中第4行的主动任务secure是一个同步控制入口(entry)类型,入口调用语句与接收(accept)语句用于响应会合请求。第10行的values是保护对象的变量,它的类型在第1行中通过Ada的generic机制声明为可重用类型,其类型根据端口类型进行实例化。
任务(task)是Ada提供支持并发程序的设施,功能与线程相同,故将AADL中的线程构件映射为Ada的任务。表3给出具体映射规则。
表3 AADL线程构件与Ada映射规则
一个进程中有多个并发执行的线程,线程的端口表示线程之间的交互,故不能简单地将端口映射为变量。线程的每一个端口都在进程的链接中有一个链接与之对应,故端口类型应对应为与之相连的保护类型的变量,作为线程类型的形参。
AADL中的线程构件则是通过在线程声明中的属性来指定线程的周期性(周期性、非周期性)。当AADL模型的属性中明确指定线程周期属性时,在生成的任务实现中通过Ada中的loop以及delay来实现,其对应的Ada代码模板如下:
1 taskbodyTask_Nameis2 --parameters3 begin4 loop5 --operation6 delayPeriod7 endloop8 endTask_Name
3.3.1 子程序构件映射规则
子程序构件用于描述进程之间的调用关系,在Ada中可以将其理解为过程的调用,映射关系如表4所示。
表4 AADL子程序构件与Ada映射规则
为了提高代码可重用性,Ada还提供了与其他语言混合编程的机制,通过调用Interface接口的方式实现。在代码实现层面这种方法类似于黑盒模式,与函数调用类似,故将其归纳为一种特殊的函数调用。为此,前面给出了对应的AADL模型扩展属性集的描述,接下来给出针对该扩展属性集的代码生成的算法:
1 defstaticdealSubCall(CallAction){2 Paths=dealCallPath(CallAction)3 Parameter=dealParm(CallAction)4 Switch(CallAction.type){5 subpgCall:{6 GenPgCall(CallAction,Parameter);}7 BlackBoxCall:{8 GenBLCall(sourceLanguage,CallAction,Name);}}}
如第4行~第8行所示,子过程调用被分为2种。第一种是常规调用,生成函数先对CallAction对象进行解析,获取到函数名和参数时便生成对应的代码。第二种子程序调用则是应用了Ada所提供的混合编程机制中的Interface方法。GenBLCall首先会对CallAction解析出需要的参数,再根据属性集中设定的目标语言等参数作为Interface的参数以生成对应的pragma Interface语句即可实现Ada与其他语言的混编。
3.3.2 行为附件映射规则
AADL行为附件BA主要用于支持组件内部的功能行为建模,通过将线程或进程的动作描述为同步自动机,以状态转移的方式来表达系统中的行为。状态转移将行为指定为当前状态从源状态到目标状态的变迁。条件决定了转换是否发生,当条件判定为真时,动作才会发生[20]。
行为附件主要包括3个部分:变量、状态和转换。变量部分声明当前行为附件中使用的局部变量,用于保存当前行为附件范围内的中间结果。状态部分枚举状态机的所有状态及属性,从初始态开始,到完成状态结束。转换描述了从源状态到目标状态的转换,其中包含警卫条件和动作。动作可以概括为:条件、赋值、循环、过程调用。表5展示了行为附件BA与Ada的对应关系。
表5 AADL行为附件与Ada映射规则
Ada语言具有严格的语法限制,行为附件中的变量需要在任务或过程的局部变量中声明。转换的算法如下:
1 defstaticdealA(BehaviorActionbehaviorAction)′′′2 ≪FORaction:behaviorAction.actions≫3 ≪switchaction{4 BehaviorActionSequence:′′′≪action.dealAE≫′′′5 PortSendAction:′′′≪action.dealPS≫′′′6 PortDequeueAction:′′′≪action.dealPD≫′′′7 AssignmentAction:′′′≪action.dealAs≫′′′8 SubprogramCallAction:′′′≪action.dealSC≫′′′9 CyclicStatementImpl:′′′≪action.dealCS≫′′′10 IfStatementImpl:′′′≪action.dealIS≫′′′11 default:′′′Exception′′′}≫12 ≪ENDFOR≫′′′
该算法将待转换对象进行解析,并根据AADL模型组件类型分类处理。第4行则是表示一个转换中存在着一组子转换对象,故调用算法自身以处理子转换对象。第5行~第7行负责处理赋值部分,赋值分为简单赋值以及端口数据读写操作。第8行是对于子过程调用处理的生成算法。第9行~第10行则为循环语句与条件语句的生成算法。
3.3.3 模式映射规则
AADL模式描述了系统的动态体系结构,在航天应用中模式被大量使用于航天器飞行状态的描述。模式被声明在系统构件、进程构件和线程构件中。每个构建中可以有多个模式,不同模式下构件的执行逻辑不同,且同一时刻有且仅有一种模式处于激活状态。模式包括模式和模式转换,模式转换的触发由构件的输入事件端口完成[9]。表6展示了模式的映射规则。
表6 AADL模式与Ada映射规则
3.3.4 数据组件映射规则
AADL数据组件表示一个基本数据类型(布尔型、字符型、枚举型、整型、字符串)时,映射到Ada的基础数据类型。类型的名称遵循标识符映射规则。类型则是来源于AADL组件的属性。
复杂的数据组件(数组、结构体、联合体)映射为Ada的相对应的结构类型,如表7所示。
表7 复杂数据组件映射规则
特别地,在AADL中可以使用Source_Language、Type_Source_Name、Source_Text属性来指定在目标语言中数据类型的定义。通过Ada的Interface机制直接引用该类型,无需进一步的改进。
3.3.5 设备构件映射规则
AADL设备构件用于描述硬件设备,在软件抽象时,设备一般被看做是系统对一串地址做操作。故将设备构件抽象为Ada中的记录体,并在Ada中指定记录体中变量的物理地址。代码如下所示,第5行~第8行中限定记录体内部成员在内存中允许分配的位置。第9行则展示了将对象指定到具体的存储地址上。
1 typeElementisrecord2 parameter1:Element_Type3 …4 endrecord5 forElementuserecord6 parameter1atxrangex..x7 …8 endElement9 E1:Element;forE1useatAddress;
本文实现了AADL2Ada代码生成原型工具,通过对第3章案例模型生成代码并对其仿真和分析以说明本文方法的有效性。
基于AADL开源环境OSATE,设计并实现了AADL2Ada代码自动生成工具,这是MACAerospace项目中的一个子工具。使用Xtend技术来开发代码生成插件,它是一种能和Java无缝连接的领域开发语言框架。Xtend提供了基于模板表达式的代码转换,这使得在模型转换代码时只需关注映射规则即可。在获取AADL模型信息时,使用了EMF(Eclipse Modeling Framework),它定义了AADL的元模型。图7展示了工具的工作流程,虚线部分是本文的工作。首先借助OSATE工具对AADL模型进行实例化;再将实例化的模型借助EMF转化为一个Java语言描述的中间模型;最后,对中间模型进行解析,并使用Xtend技术将其映射为Ada代码。表8展示了该原型工具代码规模。
图7 AADL2Ada工具工作流程
表8 AADL2Ada代码规模
4.2.1 生成代码分析
针对第3章给出的案例进行代码的自动生成并分析。主要针对该AADL模型架构及行为附件方面生成Ada代码,SIGNAL部分则是采用子程序调用的方式生成调用方面的代码。生成Ada代码的统计数据如表9所示。
表9 AOCS子系统代码生成统计数据
图8 部分自动生成的Ada代码
图8展示了部分姿态控制系统自动生成的代码。首先是平台无关方面,第1、7、11、20行展示了AADL模式部分生成的代码;第12行~第19行主要由行为附件BA部分生成。其次是平台相关方面,第2行~第9行展示了延迟等待时间更新信号的会合,通过第4行启用保护类来保护数据交互;第5行展示了过程调用以访问设备上的时间数据,并将其更新到形参中。
4.2.2 规则检查
TestBed是由英国LDRA提供的软件测试工具,适用于主机平台和嵌入式软件测试,其支持静态分析和动态分析。为了检查自动生成代码编码规范,根据航天软件产品Ada语言编码规范选出了67条检验标准,其中34条强制性标准以及33条可选标准。
自动生成的Ada代码并不是完整的项目,还缺乏数据流计算等部分,并且不支持模块测试,故将生成的代码替换到原工业级源码中以完成检测。在测试中,被检测的程序组件为624个,其中,因手工编码造成的不通过率低于20%,导致不通过的主要原因有:参数未使用、匿名子类型、同一变量名称在不同文件中重复、不能使用I/O等字符开头作为变量名称以及数据流异常等;在自动生成的代码中并未发现这些问题。图9中失败的部分原因是使用了字母i作为循环变量,以及在if语句完成时缺少结束语句。结果表明手工编程的代码容易出错,且编程风格不统一,而自动生成的代码更优于手工编写。
图9 TestBed编码规则检查部分结果
4.2.3 仿真执行
德国的iSYSTEM公司为嵌入式软件开发提供了一套解决方案,通过BlueBox技术及winIDEA集成环境为嵌入式开发提供了一个调试仿真以及分析的平台,其广泛应用于航天、医疗等领域的嵌入式软件开发中。
为了进一步说明生成代码的有效性、完整性和功能正确性,使用iSYSTEM提供的技术搭建了一个仿真平台;并将4.2.2节中检查后的代码部署在仿真环境中,通过对其发送仿真控制信号及传感器数据等,控制系统接收到数据后进行计算并发出指令调整飞行器的飞行姿态。图10为在仿真实验中航天器三轴姿态角度实时变化曲线图,其功能目标为修正姿态角角度,使得三轴角度逐渐向0收敛。如图,在初始阶段分别给三轴姿态角一个随机角度值,随后系统功能开始将其角度值逐渐修正。展示了生成代码的功能正确性,代码能满足系统设计需求。
图10 飞行姿态实时遥测数据
AADL作为模型驱动开发方法的一种标准化建模语言,逐渐应用于航空航天、医疗器械和轨道交通等领域。针对成果转化过程中代码通过人工集成到平台中带来的问题,首先提出了AADL2Ada代码自动生成方法并完成了原型工具;其次,对工业实际案例给出了相应的AADL模型,通过对其生成的代码进行仿真分析,说明了生成代码的有效性。然而,需求模型到平台相关模型之间还存在着差异,需求模型设计时不会考虑平台相关方面的信息。因此,将平台无关模型精化为平台相关模型是笔者下一步的工作。此外,复杂安全关键系统或信息物理系统CPS(Cyber-Physical Systems)包含复杂的架构信息[24]、同步/异步数据流信息、控制流信息等,如何将这些信息精化到模型中也是笔者未来的一个研究重点。