基于XSLT的可靠性模型的自动转换方法

李 蜜，庄 毅

(南京航空航天大学 计算机科学与技术学院，江苏 南京 211106)

0 引 言

随着集成模块化航电[1](IMA)概念的提出和广泛应用，使得嵌入式软件的应用日益普及，尤其是在航空航天等安全关键领域，不仅广泛应用了嵌入式软件，更要求在应用之前能够对嵌入式软件的可靠性进行严格的验证分析。AADL[2](architecture analysis and design language，体系结构分析与设计语言)是于2004年由美国汽车工程师协会(society of automotive engineers，SAE)提出，并发布了与之对应的SAE AS5506标准。自发布以来，AADL不断完善，分别于2009年和2012年发布了经过修订的AS5506A标准和AS5506B标准。由于AADL本身所具有的巨大优势，得到了航空航天领域的支持，多所大学与研究机构对AADL展开了深入研究与扩展[3-4]。这些研究涉及AADL标准扩展、建模工具、形式语义、可靠性分析等诸多方面，这些也是目前AADL的研究热点。

AADL的建模形式是基于组件进行的，它支持两种描述方式，分别是文本编辑和图形化编辑，图形化编辑方式可以建立直观的模型。AADL通过附件(Annex)机制来扩展它的模型描述能力，从而提升可扩展性。附件需要经过业界提议、发展以及核准才能成为AADL语言的一部分，已经核准的附件有Graphical AADL Notation Annex，Error Model Annex以及UML Profile Annex等。其中Error Model Annex[5](EMA，错误模型附件)主要用于嵌入式软件可靠性的建模[2,6-8],经历了两个版本更新，EMV1(EMA volume1)和EMV2[9](EMA volume2)。

但是，AADL仍属于一个半形式化的建模语言，也具有半形式化语言所固有的劣势，不能很好地支持对软件可靠性等非功能属性的严格分析评估。需要为AADL添加形式化语义[10-14]，将其转换为形式化模型，再对形式化模型进行严格验证分析。

而Z语言[15]是一种基于一阶逻辑谓词与集合论的形式化规约语言，具有精确、简洁、描述能力强等优点，所建立的模型具有很好的可扩展性[16-17]，并且能够采用现有的成熟工具对其进行类型检查与确认。

而AADL与Z语言描述形式存在较大的区别，直接的模型转换过程需要手动完善。为了实现AADL模型到Z语言模型的自动转换，需要一种可以通过现有工具完成转换的文档结构来描述AADL与Z语言[18]。XML(extensible markup language，扩展标记语言)是W3C的标准之一，提供了结构化数据和文档交换的通用格式。XMI(XML-based metadata interchange，基于XML的元模型转换)是OMG组织提出的基于XML语言的元模型交换标准。XML文档数据的转换与显示是通过添加文档样式信息来完成的，最常用的方法是基于XSLT来实现。XSL(extensible stylesheet language，扩展样式表语言)在1999年由W3C提出，主要用于将一个XML文档转换为具有任意结构的目标文档，以及定义目标文档的外观。XSLT[19](extensible stylesheet language transformations，扩展样式表转换语言)是XSL的重要组成部分，定义了XML文档的转换语言。

文中首先研究了AADL与Z语言模型的转换规则，然后通过AADL的建模工具OSATE(open source AADL tool environment)将AADL模型转换到XML格式文档，最后将基于XSLT的转换工具集成到OSATE平台上，完成AADL的XML格式文档到Z语言模型文档的自动转换。

1 AADL到Z的转换规则

1.1 AADL与Z

文中主要研究AADL可靠性模型到Z语言模型的转换规则。AADL可靠性模型包括结构模型与故障模型两个部分，将两者进行绑定可以描述软件的故障行为，从而定义软件的可靠性。图1为AADL可靠性模型框架。

图1 AADL可靠性模型框架

AADL组件分为三类：软件组件、执行平台组件和系统组件。软件组件包括线程(thread)，线程组(thread group)，进程(process)，数据(data)，子程序(subprogram group)；执行平台组件包括处理器(processer)，存储器(memory)，设备(device)，总线(bus)；系统组件包括系统(system)与抽象(abstract)。AADL组件是由组件类型和组件实现共同定义的，组件类型明确类组件类别，定义了外部接口，以及可从外部查测的特性；组件实现则是对组件的内部结构进行说明，包括内部隐含的属性、包含的子组件等等。

在EMV1中故障模型与基本组件描述方法类似，由类型和实现两部分组成。但在EMV2[9]中，故障模型则由故障类型、故障传播、故障行为的方式分开说明。

Z语言的关键元素是类型系统与构造单元。类型系统包括基本类型、幂集类型和枚举类型等。构造单元包括公理定义、模式(Schema)和通用式定义等。Schema是Z语言的基本结构，包含声明(Declaration)与谓词(Predicate)两部分，其中声明部分用于声明状态空间或局部变量，而谓词部分用于定义变量之间的约束。模式S通常采用如下的表示形式：

其中，v1,v2,…,vm为变量名，T1,T2,…,Tm分别为v1,v2,…,vm的类型，P1,P2,…,Pm为关于v1,v2,…,vm的约束。

1.2 转换规则

AADL可靠性模型的转换包括两个部分：单个组件的转换与组件间故障传播的转换。

AADL可靠性模型中每个故障模型与每个组件进行绑定，单个组件的转换就是将组件的结构、故障状态、发生的故障行为等映射至Z语言模型对应元素。其中故障行为可以通过故障事件以及事件引起的状态转移表示。

故障传播则是指某组件发生故障时会影响与之有交互的组件。这种情况是模型转换中的难点之一。

1.2.1 单个组件的转换

以下是单个组件的转换规则，因篇幅原因，部分模式仅以文字说明，未给出公式形式表达。

规则1：组件结构转换成Z语言的模式，模式声明部分描述组件的端口、参数等结构，谓词部分可以给出结构的约束，例如端口输入或者输出、参数的大小等等。

规则2：组件的故障类型通过Z语言的枚举类型表示：[ErrorType]，ErrorType={ReplicationError, ServiceError,ValueRelatedError,TimingRelatedError…}。

规则3：组件的故障状态通过Z语言的自定义类型表示：[ErrorState]，每个组件的故障状态不一定相同，因此不同组件故障状态映射的ErrorType会有所不同。

规则4：组件的故障事件(ErrorEvent，Ee)转换成Z语言的模式，模式声明部分描述故障事件发生的概率分布，谓词部分则是给出概率分布的相关约束。其中概率的分布类型通过枚举类型表示：[DistributionType]，DistributionType={Fixed,Poisson,Normal,Gauss,Weibull…}。模式的垂直形式如下：

在该模式中，<>中的元素为可替换项，Occurrence表示概率，Distribution表示概率的分布类型，R表示实数，0..1表示处于0至1之间(包含边界)。

规则5：组件的状态转移转换成Z语言的模式，模式声明部分描述导致状态转移的转移动作，以及转移的前后状态，谓词部分给出状态转移需要满足的必要条件。模式垂直形式如下：

1.2.2 故障传播的转换

AADL可靠性模型中的故障传播包括故障传播点(ErrorPropagationPoint，Epp)、故障传播的路径。故障传播点包括传入故障点incoming、传出故障点outgoing。而故障传播路径在AADL中用流(Flow)表示，流定义了组件从输入到输出的逻辑流，可以描述组件之间数据流、控制流或者故障流。

以下为故障传播的转换规则。

规则1：故障传播点转换成Z语言的模式，声明部分描述故障传播点的类型。而故障传播点的类型通过枚举类型表示：[EppType]，EppType={incoming,outgoing}。

规则2：故障传播路径转换成Z语言的模式，模式声明部分描述故障传播经过的传播点，用以表示传播路径，谓词部分给出相关约束。模式的垂直形式如下：

在该模式中，Epp即规则1所转换得到的模式。

2 基于XSLT的自动模型转换

OSATE是由卡耐基梅隆大学开发的一款开源AADL建模环境。OSATE以eclipse插件形式提供了AADL的建模、验证与分析工具。建模工具支持AADL文本、图形和XML三种视图的同步建立、更新与转换。

在完成AADL可靠性模型的建模与对应XML源文档的生成后，需要根据转换规则设计XSLT样式表。根据第1节提出的转换规则，描述一个完整的AADL可靠性模型需要以下元素：组件结构模式、故障事件模式、状态转移模式、故障传播点模式、故障传播路径模式和一些数据类型。所以在转换过程中要分阶段对源文档进行递归处理。另外，在设计过程中会用到Z模式中一些特有的标识符，所以在设计之前需要在实验环境中增加相应的Z语言字符集。

XSLT样式表部分内容如图2所示。

图2 XSLT样式表实例

图2中样式表的┌与└符号表示输出模式的标识符，会直接输出。其次，用元素输出模式的模式名，命名格式为“[name]+Event”，name与XML源文档中对应元素相同，Event可以不加。样式表中的“|”则对应Z语言模式中的分隔线，将声明与谓词部分分隔。

以上是以故障事件为例简单说明了XSLT的设计过程，由于XSLT语言的模块化特性，可通过添加模式表模板来匹配更多AADL元素，从而实现AADL模型的自动转换。

总结基于XSLT的转换过程如下：在OSATE平台上建立AADL的可靠性模型，并转换为XML格式的源文档。根据建立的AADL到Z的转换规则设计XSLT样式表，将AADL可靠性模型进行转换，最后输出目标文档，得到Z语言模型。图3展示了AADL到Z的转换流程。

图3 AADL到Z的转换流程

3 实例研究

文献[2]中以一个飞行控制系统作为示例描述了AADL可靠性的建模过程。文中对该系统的自动驾驶子系统的功能需求进行细化，以此作为示例对文中模型转换方法进行应用说明。

3.1 实例描述

图4是自动驾驶子系统的AADL架构，包含4个作动器(Aileron、Elevator、Rudder与Engine)与1个GPS传感器。作动器用来控制飞行器的飞行状态，GPS用来获取当前定位信息。还包括了计算线程(AP_Computer)、读取GPS数据线程(GPS_Reader)、参数设置线程(AP_Params)等四个线程组件。该子系统的功能是通过4个作动器和GPS传感器的交互来控制飞行控制系统状态。文中以设备GPS与线程GPS_Reader为例说明模型转换方法。

图4 自动驾驶子系统AADL架构

3.2 自动转换过程

GPS的AADL可靠性模型如图5所示，主要包含两个部分：故障行为与GPS组件的类型及实现。故障行为中描述了一个故障事件CatchFail、两个故障状态Error_Free和Failed、一个状态转移BadValue Transition，并在属性中给出了故障事件的概率分布，概率为0.003，分布类型为定值Fixed。在GPS组件的类型中描述了两个端口send1与send2，send1为输出数据端口，send2为输出事件端口。GPS组件类型中还包含了一个annex EMV2，在其中描述了组件采用的故障模型库、故障行为、故障传播点(用send1、send2表示)与故障传播流(GtoR)。

图5 GPS的AADL可靠性模型

GPS_Reader的AADL可靠性模型与GPS类似。

图6是GPS的AADL可靠性模型对应的XML源文档。从图中可以看到GPS的故障行为CFT被转换为XML文档中的树状结构。

图6 GPS的AADL可靠性模型XML源文档

转换规则对应的XSLT样式表设计过程按第2节所述方法进行。最后通过基于XSLT样式表转换得到的目标Z语言模型文档(部分)如图7所示。其中GtoR表示故障传播流，send1是GPS组件的故障传出点、recv是GPS_Reader的故障传入点，在谓词约束中对传入传出类型进行约束。

图7 Z语言模型文档

将图7所示的部分转换结果与图5所示的部分AADL进行对比，可以看出，图7的Z模型中描述的CatchFail、send1和GtoR均在图5的AADL中有定义，并且在转换过程中，这些组件的可靠性约束完整、无丢失。比如，send1在AADL先被定义为out data port类型，即为数据输出接口，后在定义flows类型的GtoR时又被定义为故障源接口，即为故障输传出点；在图7的send1模式中，将send1直接定义为了故障传出点，符合转换要求。这验证了文中转换方法的正确性和有效性。

4 结束语

针对AADL难以严格验证评估软件可靠性的问题，在对AADL与Z语言语法语义研究的基础上，提出AADL到Z的转换规则，分别研究了单个组件以及组件间故障传播的转换规则。并基于XSLT实现了AADL到Z的自动转换方法，从实例研究中可以看到，该方法可以将AADL中的相关元素都转换到Z语言模型中。基于文中的研究工作，可以在软件开发的设计阶段建立直观的AADL可靠性模型，而通过AADL到Z的转换有助于后续的可靠性评估工作。