基于Z-AADL模型的形式化转换

高 正，曹子宁

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

基于Z-AADL模型的形式化转换

高 正，曹子宁

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

结构分析与设计语言(Architecture Analysis and Design Language,AADL)是针对嵌入式实时系统领域中的软件开发复杂度问题而提出的一种基于模型驱动开发的体系结构建模语言，可用于设计和分析一些安全关键嵌入式实时系统的软硬件体系结构。但是AADL严格来说只是一种半形式化的建模语言，虽然也描述了模型中构件的属性，但是对模型的非功能属性并没有明确的形式化描述，因此对AADL系统模型的非功能属性进行形式化验证，对于保证系统的正确性和可靠性具有重要意义。针对AADL模型中对非功能属性及数据性质等描述的不足之处，将其与形式规格说明语言Z语言相结合，提出了一种新的描述能力更加强大的形式规范语言—Z-AADL，并且定义了将Z-AADL模型转换为形式化模型—ZIA模型的转换规则，以实现Z-AADL模型到ZIA形式化模型的转换。并通过一个转换实例进行说明。

Z-AADL；ZIA；CT-ZIA；模型转换

0 引 言

嵌入式实时系统在航空航天、汽车控制、机器人等安全关键系统领域得到愈来愈广泛的应用。但由于计算精度、实时响应、资源限制等要求的提高，系统开始变得越来越复杂，因此采用更加严格和可靠的设计与实现规范可以实现具有高可靠性、高质量的复杂嵌入式实时系统[1-2]。针对这一越来越紧迫的问题，2004年，美国汽车工程师协会(SAE)提出了嵌入式实时系统体系结构分析与设计标准-AADL[3]。它以传统的建模语言MetaH、UML[4]为基础，能够更加精确地设计与分析嵌入式实时系统的软硬件体系结构及功能属性等。但是，AADL仍然存在一些问题，有待进一步的研究与完善。AADL采用自动机的形式对线程、进程等构件的执行状态和动作进行了语义描述，但这种语义并不是严格的形式化语义描述，而且对于状态及状态转换之间的数据约束关系也没有形式化语义描述，因此难以直接进行一致性检验。结合国内外对AADL建模语言多年的研究现状，现在对AADL形式语义的研究多采用形式化转换的方式，主要包括两种：

(1)用某种具有精确语义的形式化语言来定义AADL的语义，然后通过这种语义来进行形式化的转换；

(2)对目标系统进行AADL建模，然后将这种模型直接转换为另一种形式化模型。

Z语言是一种严格的形式化规范描述语言，可以对状态及状态转换之间的数据约束等进行严格的形式化描述。因此文中提出在AADL的基础上扩展Z，形成Z-AADL规范，从而可以在不考虑具体设计细节的情况下，从更高的抽象级别用Z-AADL刻画AADL模型。

1 AADL的Z扩充

1.1 AADL简介

AADL是一种功能十分强大的分析与设计语言，越来越广泛地应用于航空电子、飞行控制等航空航天领域的嵌入式实时系统的体系结构设计与分析中。它主要包括三大类组件，即：软件组件、执行平台组件、系统组件。并且，在系统的建模过程中，通过包来组织所定义的组件类型和组件实现等内容，这是一种类似于高级开发语言的组织形式。其中，软件组件主要包括进程组件、线程组件、线程组组件、数据组件、子程序组件、子程序组组件等。软件组件的主要功能是用来表示系统的进程、线程组、线程等应用程序所具有的任务架构，可用于表示模型所属的软件体系组成部分，例如数据组件中的数据类型、程序中的可执行代码等。执行平台组件主要包括处理器组件、存储器组件、总线组件、外设组件等，主要功能是对系统的软硬件体系结构分层次建模，通常表现为系统中相关线程的调度、接口与接口之间的通信、接口与外部系统的通信等。系统组件的主要功能是将所建模的系统中所拥有的所有组件组合起来，形成一种分层次的系统结构。AADL建模语言通过构件、连接等来刻画系统的软硬件体系结构；通过特征、属性等来刻画系统的性质；当系统需要在不同的工作模式之间切换时，它也可以通过模式转换来刻画系统的运行体系演变。体系结构、执行模型和行为描述构成一个完整的AADL模型,因此AADL语义也涉及这3个方面。文中主要是对AADL中的Behavior Annex[5-6]语义进行扩充的形式化描述。

1.2 Z语言简介

Z语言[7]是一种基于一阶谓词逻辑和集合论的形式规格说明语言，它采用了严格的数学理论，可以对系统的行为特征和状态值进行简明、精确、无歧义且可证明的形式化描述。Z模式是Z语言的核心，它有两种模式：状态模式和操作模式。状态模式定义目标软件系统某一部分的状态空间及其约束特征；操作模式描述了系统某一部分的行为特征，它通过描述操作前该部分的状态值和操作后该部分状态值之间的关系来定义系统该部分的一种操作特征。为了简单明确地描述状态与操作模式，Z规范中采用下述方式来表示变量：输入变量的最后一个字符后跟随一个“?”，输出变量的最后一个字符后跟随一个“!”。前状态变量就是通常的变量，对应的后状态变量是以撇号“’”作为右上标修饰的变量。

1.3 AADL的Z扩充规则

AADL的完整语义的形式化非常庞大，因此考虑一个AADL的子集，包括Thread,connection,behavior annex,系统执行模式等。文中主要对AADL中的behavior annex进行Z语言扩充。其中，behavior annex包括状态集合以及状态的转换集合。约定：R表示变量之间的约束关系，ψ表示状态转换时所要满足的约束性质，Computation表示状态转换时执行的操作。状态的Z模式描述如下：

Output|xi?∈Input∧yj!∈Output;xi,yj:xiRyj]

状态转换的Z模式描述如下：

Output;SrcState,DstState:STATE|SrcState.xi

SrcState.xi=DstState.yi;SrcState.xj=DstState

.yj;xi,xj∈Input;yi,yj∈Output;]

状态转换时的约束性质的Z模式描述如下：

Output|xi?∈Input∧yj!∈Output;φ∈ψ]

状态转换时所进行的操作模式描述如下：

yn!:Output|xi?∈Input∧yj!∈Output;φ∈ψ]

1.4 基于连续时间的ZIA(CT-ZIA)

1.4.1 CT-ZIA的定义

ZIA[8-9]可以刻画系统的行为和状态，但是它并不能刻画系统在实时方面的性质；时间自动机[10]是用来刻画实时系统的一种自动机模型。文中将连续时间ZIA与时间自动机相结合，形成一种针对嵌入式实时系统的能够同时刻画行为和状态的形式规范CT-ZIA[11]。

其中：

(1)SP是状态集合。

根据陪护在患者身边时发生跌倒坠床时的状态描述可以看出，搬运患者、陪护在身边睡觉、患者床边大小便后陪护未安置好患者等情况为主（见表3）。

(7)X为时钟变量的非负实数有限集合，C(X)为X上时钟约束的集合，其语法定义如下：Φ::=xc|cx|φ1∧φ2。其中，x∈X，∈{<,≤}，c为非负有理数。

(8)映射I：SP→C(X)为每个状态赋一时间约束，此约束称为节点不变量。

(9)TP是状态之间转换关系的集合，TP⊆SP×AP×C(X)×2X×SP。如果(s,a,φ,λ,s′)∈TP，那么表示在满足转换约束条件φ的前提下，通过动作a∈AP(s)，状态s可以迁移到新的状态s'，同时λ⊆X中的时钟被重置为0。

下面给出CT-ZIA所对应的一种时序逻辑及其语法和语义。

1.4.2RT-DCL时序逻辑

文献[12]通过在时序操作符上增加一个下标用于约束时间的范围，从而得到一种时序逻辑RT-DCL，用这种时序逻辑可以作为CT-ZIA规范所对应的时序逻辑。

RT-DCL的语法也就是逻辑合法公式，定义如下：

定义2：RT-DCL的逻辑合法公式。

(2)若有φ1,φ2∈RT-DCL，则有φ1∨φ2∈RT-DCL。

(3)若有φ1,φ2∈RT-DCL，则有φ1∧φ2∈RT-DCL。

(6)若有φ1,φ2∈RT-DCL，则有Eφ1U～cφ2∈RT-DCL。其中，{<,≤,=,>,≥},c∈N。

(7)若有φ1,φ2∈RT-DCL，则有Aφ1U～cφ2∈RT-DCL。其中，{<,≤,=,>,≥},c∈N。

下面给出计算路径CT-ZIA上的定义。

定义4:RT-DCL的语义。

如果由Z-AADL模型转换后得到的CT-ZIA模型是带有数据约束的，刻画如下：

2 Z-AADL到CT-ZIA的转换

2.1 Z-AADL模型的刻画

下面将实时系统用Z-AADL规范刻画为一个七元组T=，其中：

(1)ST={si:i∈}表示系统中状态的集合，即1.3节中Behaviorannex中的状态States，即扩充了的Z状态模式的集合。

(2)NT表示系统中关于数据性质描述的集合。性质包括但不限于1.3节中的Guard等数据性质。

(3)PT表示系统中接口的集合，包括线程、进程等构件中的输入输出接口。

(4)CT表示系统中时钟变量的非负实数集合，状态转换时所要满足的时钟约束；TB为CT上的时钟基，时钟基是时钟变量的有序可数集合：TB={[ci,cj]|ci

(5)AT表示系统中动作的集合，即1.3节Transition中扩充了的操作模式Computation等。

(6)TRT表示系统中状态转换的集合，即1.3节中Behaviorannex中的状态转换Transitions，即扩充了的状态转换模式Transition的集合。

2.2 Z-AADL到CT-ZIA的转换规则

从Z-AADL到基于连续时间CT-ZIA模型的转化规则如下:

(1)SP={si:sTi∈ST,i∈}，其中si∈SP是CT-ZIA模型P中的状态，sTi∈ST是Z-AADL模型T中的状态。

(2)AP={ai:aj∈AT,aj→ai,i,j∈}，其中aj∈AT是Z-AADL模型T中的动作，aj→ai表示将模型T中的每一个动作aj，映射为模型CT-ZIA中的一个动作ai，根据动作执行者的不同，将它们分别归入内部动作、输入动作和输出动作集合中。

(3)VP={vi:pi∈PT,pi→vi,i∈}，pi→vi表示将Z-AADL模型T中的接口用到的变量vi根据变量的拥有者分别把它们归入到输入变量、输出变量和中间变量的集合中。

(6)X={xi:ci∈CT,i∈},C(X)={cx:[ci,cj]∈TB，i,j∈，[ci,cj]→xi,xi∈X,i∈}。其中ci∈CT是Z-AADL模型T中的一个时钟变量，映射为CT-ZIA模型P中的一个时钟变量xi∈X，[ci,cj]∈TB是Z-AADL模型T中的一个时钟基，[ci,cj]→xi表示将时钟基[ci,cj]∈TB映射为CT-ZIA模型P中对于xi的时钟约束。

(7)I={si|→[ci,cj]:si→xi,[ci,cj]→xi,si∈S,[ci,cj]∈TB}，其中si→xi表示将Z-AADL模型T中的时钟基TB中的时钟对[ci,cj]转换为CT-ZIA模型P中状态si上的时钟约束。

在系统内部状态变迁过程中，CT-ZIA中的状态转换是严格按照所要转换的扩充了Z语言的AADL系统中的状态转换映射过来的，这样也就保证了在转换过程中，系统内部行为的一致性；而关于对时钟的刻画[13]，通过把实时系统中的时钟变量提取出来，CT-ZIA中的时钟变量是根据实时系统中的时钟变量以及时间事件来进行时钟不变量的描述，这就确保了实时性的一致性描述；对于数据的约束能力，因为实时系统中非功能属性可以映射到Z语言模型，而CT-ZIA就是把数据用Z模式来进行约束，这样在数据约束能力方面它们采用的是一样的Z模式，所以从实时系统转换到CT-ZIA之后，它的行为和性质与转换之前保持了一致性。文献[13]对模型转换的正确性进行了归纳证明，文中的证明与此类似。

3 模型转换实例

锅炉装置在发电厂、船舶等领域应用广泛，文献[14]中对一个蒸汽锅炉控制系统进行了自动机建模,文中参考此模型，建立了一个简化的蒸汽锅炉模型，它包括温度控制器、供热系统以及压力控制器，如图1所示。其中，温度是由温度控制器控制，压力由阀门自动控制，供热系统会向压力控制器发送压力值。

图1 锅炉系统

图2展示了系统中温度和压力的状态转换关系，用变量x和y分别表示温度和压力。x?表示供热系统从温度控制器接收一个输入变量,y!表示供热系统向压力控制器发送一个输出变量。假设初始温度和压力分别为20 °C和100Kpa，初始状态为l0。当压力大于等于700时状态会跳转到l1，并将压力置为700，压力导数置为30，此后的状态跳转与此类似。

图2 状态转换关系

锅炉系统中的压力会随着温度自动变化，因此下面只给出温度控制器的AADL建模描述：

Threadimplementationtemp.impl

Features

x:indataporttemperature;

y:outdataportpressure;

Properties

Dispatch_Protocol=>Periodic;

Period=>50ms;

Compute_Execution_Time=>15ms..15ms;

Deadline=>50ms;

annexbehavior_specification**

states

l0:initialcompletestate;

transitions

l0-[]→l1{a0(30ms);x':=20,y':=y'+10};

l1-[]→l2{a1(15ms);x':=dx'+10,y':=y'};

l2-[]→l3{a2(15ms);x':=x',y':=y'-10};

l3-[]→l0{a3(15ms);x':=x'-10,y':=y'};

** ;

endtemp.impl;

根据1.3节中的Z扩充规则，对AADL模型中的状态、操作以及状态变迁等进行Z模式的扩充。以l0，a0以及通过a0所做的状态变迁为例，分别给出Z模式描述如下，后面的情形与此类似。

l0[x?:N;y!:N|x?<1 000;y!≥20];

其中，x?表示状态l0时的温度，y!表示状态l0时的压力。

transition[x?:N;y!:N;l0;l1|x?<1 000∧y'!≤940;x?=20∧y'!≤1 000];

其中，l0；l1表示状态变迁时的前状态与后状态。

a0[x?:N;y!:N|x?=700;x'?=30];

根据上述状态转换关系，可以刻画锅炉系统的Z-AADL模型，即2.1节中的七元组模型T=。

(1)ST={l0,l1,l2,l3}表示系统中状态的集合；

(2)NT={?(y!≥700),(x?≥660∧y!≥820),(x?≥960∧y!≥1 000),(x?≥900∧y!≥900)}；

(4)CT=[0,75],TB为CT上的时钟基， TB={[0,30]，[30,45]，[45,60]，[60,75]}；

(6)TRT={(l0,a0,l1),(l1,a1,l2),(l2,a2,l3),(l3,a3,l0)}表示系统中的状态转换的集合。

根据2.2节的模型转换规则，可将上述的Z-AADL模型转换为CT-ZIA模型：

(1)SP={l0,l1,l2,l3};

(3)AP={a0,a1,a2,a3};

(4)VP={x?;y!};

(7)TP={(l0,a0,l1),(l1,a1,l2),(l2,a2,l3),(l3，a3,l0)}。

4 结束语

文中对AADL建模语言进行了Z语言扩充，形成了新的规范Z-AADL，从而使其不仅保留了原来的描述能力，而且具备了形式化的描述状态及状态转换之间的数据约束方面的能力，为转换为CT-ZIA形式化模型打下了基础；然后研究了Z-AADL模型与CT-ZIA模型之间的转换，使得转换后的模型可以采用形式化方法进行分析与验证等。

在AADL的扩展和形式化模型转换方面取得了一定的成果，但是转换后的模型是基于连续时间的无穷状态模型，因此需要将其转换为有限的域自动机模型来验证。未来的主要工作是研究基于连续时间的CT-ZIA如何转换为有限的域自动机模型，从而实现模型检测。

[1] 杨志斌，皮 磊,胡 凯,等.复杂嵌入式实时系统体系结构设计与分析语言:AADL[J].软件学报，2010，21(5)：899-915.

[2] 禚百田，付秀敏，郑永果，等.基于UML的嵌入式实时系统开发方法[J].信息技术与信息化,2010(1):56-59.

[3]SAEAerospace.SAEAS5506:ArchitectureAnalysisandDesignLanguage(AADL)[EB/OL].2004.http://www.aadl.info/aadl/currentsite/.

[4] 王立杰,刘昌禄,俞烈彬.基于MDA的MARTE模型形式化转换[J].指挥控制与仿真,2012,34(6):128-133.

[5]SAEAerospace.SAEAS5506annex:behavior_specificationV1.6.[EB/OL].2006.http://www.aadl.info/aadl/documents/Behaviour_Annex1.6.pdf.

[6] 李振松，顾 斌.基于UPPAAL的AADL行为模型验证方法研究[J].计算机科学,2012,39(2):159-161.

[7] 倪水妹.面向混成系统的ZIA形式化模型及其自动验证方法研究[D].南京:南京航空航天大学，2014.

[8] 李广元，唐稚松．带有时钟变量的线性时序逻辑与实时系统验证[J]．软件学报，2002，13(1):33-41．

[9] 狄杨思，曹子宁，王 辉．一种基于形式规范ZIA的自动验证方法[C]//火力控制技术/航空电子系统综合技术2011年学术年会.出版地不详：出版者不详，2011：113-120．

[10] 孙全勇.时间自动机及其应用研究[D].哈尔滨：哈尔滨工程大学，2007.

[11] 倪水妹，曹子宁，李心磊.带数据约束实时系统的模型检测[J].计算机科学,2014,41(5):254-262.

[12]LinHuiming,ZhangWenhui.Modelchecking:theories,techniquesandapplications[J].ActaElectronicaSinica,2002,30(S1):1907-1912.

[13] 钱俊彦,赵岭忠,古天龙.一种基于时间自动机的时钟等价性优化方法[J].计算机工程，2005，31(18)：71-73.

[14]HenzingerTA,Wong-ToiH.UsingHyTechtosynthesizecontrolparametersforasteamboiler[M].Berlin:Springer,1996.

Formal Transformation Basedon Z-AADL Model

GAO Zheng，CAO Zi-ning

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

Architecture Analysis and Design Language (AADL) is a kind of system structure modeling language based on model driven development in view of the problem of software development complexity in the field of embedded real-time system,which can be used to design and analyze the software and hardware architecture of some security critical embedded systems.But AADL is a semi-formal modeling language seriously.Although it also describes the properties of the components,the non-functional properties of the model are not clearly defined.Therefore,the formal verification of the non-functional properties of the AADL system model is of great significance to guarantee the correctness and reliability of the system.Aiming at the shortage of non-functional and data property of AADL model,combining the AADL specification with the Z language,a new specification—Z-AADL is put forward.Then the transformation rules between Z-AADL and ZIA is given,which define that how the Z-AADL model can be transformed to the ZIA model.An example is given to illustrate the transformation.

Z-AADL;ZIA;CT-ZIA;model transformation

2015-12-03

2016-03-17

时间：2017-01-04

国家“973”重点基础研究发展计划项目(2014CB744900)

高 正(1991-)，男，硕士研究生，研究方向为形式化方法；曹子宁，博导，研究方向为形式化方法、人工智能。

http://www.cnki.net/kcms/detail/61.1450.TP.20170104.1023.030.html

TP31

A

1673-629X(2017)03-0023-06

10.3969/j.issn.1673-629X.2017.03.005