系统架构描述语言AADL的功能行为建模扩展*

许金淼，杨志斌,2，黄志球,2+，谢 健,2，周 勇,2

1.南京航空航天大学 计算机科学与技术学院，南京210016

2.高安全系统的软件开发与验证技术工信部重点实验室，南京210016

+通讯作者E-mail:zqhuang@nuaa.edu.cn

1 引言

嵌入式系统广泛应用于航空、航天、核能等领域，这些系统具有资源受限、交互频繁等特点，对实时性、可靠性等性质有非常高的要求，因此也称为安全关键系统（safety-critical systems）。由于功能和非功能要求不断提高，系统的复杂度急剧增加。如何设计与实现高质量的安全关键嵌入式系统，并有效控制开发时间和成本，是学术界和工业界共同面临的难题。近年来，模型驱动开发方法（model-driven development，MDD）逐渐成为安全关键系统设计与开发的重要手段[1]。

MDD 作为一种软件系统开发的综合方法，它以UML（unified modeling language）及相关技术和实践为基础。MDD的中心概念之一是模型细分为平台无关模型（platform independent model，PIM）和平台相关模型（platform specific model，PSM）。现阶段，工业界常用的建模语言包括UML、SysML 和AADL（architecture analysis and design language）等。UML 是一种支持模型化和软件系统开发的图形语言。它可以通过类图对数据建模，通过状态图对行为建模，通过活动图、序列图对组件之间的交互建模。UML 支持软件的开发过程，可以建模平台无关模型（PIM）。但是，对于安全关键嵌入式系统，运行时间等非功能属性尤为重要。这些非功能属性依赖于执行平台信息，而UML是一种通用的建模语言，在表达安全关键嵌入式系统特有的某些非功能属性时不够精确[2]。SysML 是一种用于规范、分析、设计复杂系统（包括软硬件信息）的通用图形建模语言。SysML 是对UML2.0子集的重用和扩充，它的需求图支持结构化的需求建模且可以提高可追溯性，参数图可以捕捉物理系统的动态特征。但SysML 关注于系统层建模，不擅于表达计算机运行时环境（包括线程、进程，以及对处理器的分配）等特性[2]。另外，SysML 缺少精确的形式化语义描述，不利于后期的形式化验证。而AADL[3-4]是一种复杂嵌入式系统架构描述语言，它通过组件的概念描述嵌入式软硬件系统。AADL提供线程、线程组和进程来表示在受保护的地址空间（时间和空间分区）中执行的并发任务，通过端口、共享数据组件和服务调用来表示软件运行时体系结构。此外，AADL 标准为任务执行、通信时序以及模式转换提供了精确的执行语义，也称之为AADL执行模型[5]。

嵌入式系统的功能行为建模包括控制流建模与数据流建模。如图1所示，给出了AADL功能行为建模扩展的总体框架，包括基于行为附件对控制流功能行为建模以及基于同步语言SIGNAL[6]对数据流功能行为建模。

Fig.1 Global view of AADL functional modeling图1 AADL功能行为建模总体框架

为了支持组件内部的控制流建模，法国IRIT实验室于2006年提出了AADL行为附件（behavior annex）[7]。行为附件以变迁系统（transition system）的形式增强了AADL线程构件和子程序构件功能行为的详细描述能力[8]。行为附件与执行模型有密切的关系：执行模型定义行为附件何时执行，哪些数据被改变，而行为附件处于构件内部，对线程、子程序构件的执行给予更精确的描述[9]。

在对工业实际案例建模过程中，可能存在如下问题：（1）建模实际的工业项目是一个不断精化的过程，扁平化的状态机难以适应频繁的精化。（2）工业界的实际项目中有许多复杂的多层嵌套的层次状态机。如果这些嵌套状态机被展开，将会形成一个巨大且难以管理的状态机图。（3）扁平化模型难以管理大量的组件，并且扁平化模型会造成结构信息的丢失。因此，对于AADL行为附件来说，层次化地表达功能行为是一个非常重要的特征。

为了解决扁平状态机的问题，Elattar等人扩展了UML 状态图Statecharts[10]。相应地，David 提出了层次时间状态机（hierarchical timed automata，HTA）[11]的概念，用于解决UPPAAL 中的层次化建模问题。另外，França 等人[12]通过对飞行控制软件的实际建模，评估了AADL 行为附件，提出了在AADL 行为附件中引入层次化概念的想法。然而，他们没有给出形式化的语法、语义定义以及层次化扩展的实现。

在本文中，根据层次化控制流建模思想，提出了AADL行为附件的层次扩展，命名为HBA（hierarchical behavior annex）。然后，给出了HBA 的形式语法和语义定义。为了实现HBA，给出了AADL 行为附件的元模型扩展。此外，完整的HBA 插件已被集成到AADL开源环境OSATE（open source AADL tool environment）中。为了便于形式化验证，给出了HBA到时间自动机TA（time automata）的转换规则，并利用UPPAAL工具对模型性质进行分析。最后，介绍一个使用HBA的实际工业案例。

本文的其余部分结构如下：第2章介绍了AADL和行为附件；第3 章给出了HBA 的语法定义；第4 章定义了HBA 的形式语义；第5 章介绍了AADL 行为附件层次化扩展的实现；第6 章给出了HBA 到TA（timed automata）的转换规则；第7章介绍了一个实际的工业案例研究；第8 章讨论相关工作；第9 章给出结论。

2 研究背景

2.1 AADL语言简介

AADL 是一种专为嵌入式系统建模而设计的架构描述语言。它支持高度可演化系统的开发，系统架构的早期分析，以及用于整个生命周期持续分析的架构模型的演变。

AADL采用半形式化的建模概念，描述了复杂嵌入式系统的软件、硬件架构和非功能属性，包括不同的组件及其交互。AADL 提供了一组预定义的组件类别[3-4]：

（1）线程、线程组、子程序、数据、进程。

（2）处理器、内存、总线、外设。

（3）用系统表示软件和执行平台的组合集。

例如，一个线程表示一个连续的执行流程，它是唯一可以被调度的AADL组件。一个子程序表示一段可以被线程或另一个子程序调用的代码。

组件之间的通信可以通过数据流、子程序调用或访问共享变量来实现。这些不同的通信方式在通信组件的接口中声明。根据所选择的通信方式实例，通信连接点可能是端口（port）、子程序（subprogram）或数据访问（data access）[8]。

系统行为不仅依赖于上述组件及其连接所定义的体系结构，还依赖于运行时环境[13]。AADL标准将执行模型指定为虚拟运行时环境（包含同步和异步模式），以支持组件的执行和管理。在执行模型中也定义了诸如截止日期、调度时间等时间属性，这些属性通过AADL属性声明。

此外，AADL 支持两种扩展方式：属性集和附件。属性集扩展允许用户引入新的属性集。例如，调度分析工具Cheddar，通过定义新的属性集增强了AADL支持更复杂调度算法的能力。现有的附件包括AADL错误模型附件[14]、AADL行为附件[7]、ARINC653附件、数据模型附件等。

2.2 AADL行为附件

行为附件是执行模型调度机制的扩展，用于更精确地描述模型行为，例如端口通信、子程序调用、时序、异步等。AADL执行模型指定行为附件何时执行，并指定哪些数据被执行。完整的AADL 模型应该包括执行模型和行为附件。现在行为附件可以附加到AADL 的任何组件中。它通过扩展的AADL 模式自动机[7]来描述组件行为，例如：“initial”指定自动机的初始状态，“complete”指定线程完成，转换可以包括条件和动作，条件和动作包括发送或接收事件，调用或执行子程序等。

行为附件主要包括三部分：变量、状态和转换。变量部分声明当前行为附件中使用的所有局部变量。局部变量可以用来保存当前行为附件范围内的中间结果。状态部分枚举状态机的所有状态及其属性（initial，complete，final 或它们的组合）。默认状态是一个执行状态。转换定义了从源状态到目标状态的转换，转换可以有条件和动作。

下面给出一个线程的行为附件的示例代码：

3 层次行为附件（HBA）语法

HBA扩展了AADL行为附件以增强行为附件的层次描述能力。HBA 保留AADL 行为附件的变量、状态和转换，添加层次映射函数和复合状态。

定义1（层次行为附件HBA）层次行为附件是一个六元组＜Var,S,S0,η,T,type＞，其中：

Var是自动机中使用的局部变量的有限集合。S是一个非空有限的状态集合。S0⊆S是初始状态的有限集合。η:S→2S是层次函数，它将S映射到S的所有可达的子状态上。映射η将会产生一个根节点为root的树结构，其中root∈S。通过η来记录某状态S与其子状态的层次关系。type穷举了所有状态的类型。复合状态是AND 或者XOR 类型。非复合状态是基本状态（BASIC）、入口状态（ENTRY）、出口状态（EXIT）或历史状态（HISTORY）中的一种。

AND状态表示该复合状态的所有子状态是并发执行的，即当父状态被执行时，其内部各子状态同时从各自的初始状态开始执行。在后续的HBA 实现中，将AND 状态表示为“concurrent state”。XOR 表示该复合状态内的所有子状态是互斥执行，即同一时刻有且仅有一个子状态被执行。在后续的HBA实现中，将AND状态表示为“composite state”。ENTRY状态表示该非复合状态是其父状态的入口状态，即当进入其父状态时，默认进入该子状态。EXIT 状态表示该非复合状态为出口状态，即将要从其父状态转移到下一状态时，由该状态转移至下一状态。HISTORY 状态是一个伪状态，其目的是记住从组合状态中退出时所处的子状态，当再次进入组合状态时，可直接进入这个子状态，而不是再次从组合状态的ENTRY状态开始。

T⊆s×(Guard×Action)×s是转换函数。一个转换连接两个状态S和S′，转换有一个条件guard，或为布尔值。转换完成时可执行某一动作Action，Action可被省略。S被称为该转换的源状态，S′被称为该转换的目标状态。使用表示一个转换。当g缺省时，可以省略。当转换完成时，动作a将被执行。

图2显示了一个该语法的例子：图2（a）以图形的形式描述了一个状态图，图2（b）显示了它的树状表示。图2 下方显示了该状态图在对应的AADL 行为附件代码。可以看出状态A是一个AND类型的复合状态，并且ENTRY 类型的状态和EXIT 类型的状态不会在树状图中出现。

在给出状态约束之前，先给出符号约定。

用谓词符号TYPE(s)来表示。例如：AND(S)为真，表示TYPE(S)=AND。

由于HISTORY也是一种特殊的入口状态，因此定义HEntry(S)来表示一个状态的入口状态，当HISTORY状态存在时，HEntry(S)=Histroy(S)，否则HEntry(S)为S默认入口(ENTRY)状态。

定义函数η-1表示某一状态的父状态，即：

因此，定义函数η-2表示某一状态的祖父状态，即：

Fig.2 Syntax of HBA图2 HBA语法示例

下面，给出一些约束来确保HBA的一致性。

（l）只有复合状态才能包括其他状态：

（2）AND 类型的复合状态的所有子状态都不是basic类型：

（3）XOR 类型的复合状态的子状态只有一个初始状态：

（4）语法不支持直接地穿越层次边界的转换。当转换以复合状态作为源状态时，需将复合状态的出口状态作为默认的源状态，例如Exiting transitions。当转换以复合状态作为目标状态时，需将复合状态的入口状态作为默认目标状态，例如“Entering transi-tions”。合法的转换集合在表1中给出。图3中，黑色实心点表示入口或出口状态，白色空心点表示基本状态。规定转换不能直接从ENTRY类型状态到EXIT类型状态。

Table 1 Legal transition example表1 合法的转换类型

Fig.3 Legal transitions图3 合法转换示例图

4 层次行为附件操作语义

本章定义HBA的形式化操作语义。在HBA中，任一时刻系统的当前状态称之为一个系统状态。每一个系统状态显示了当前系统所包含的信息，即处于激活状态的位置的集合、当前时刻变量的赋值和历史状态。

定义2（系统状态）系统状态的形式为(ρ,μ,θ)，其中：

ρ:S→2S给出了处于激活状态的位置。ρ可以理解为η的一个部分的、动态的版本，它将每一个复合状态S，映射到S的当前被激活的子状态。如果一个复合状态S没有被激活，那么ρ(S)=∅。定义Active(S)=S∈ρ*(root),其中ρ*(S)是S的所有被激活子状态的集合，包括S本身。如果S≠root，那么Active(S)⇔S∈ρ(η-1(S))，其中η-1(S)是S的父状态。

μ:Var→ℝ 将实数变量映射到它们对应的值。如果¬Active(S)，那么对于ν∈Var(S)，μ(ν)是未定义的，记作μ(v)=⊥。

θ:S→S表示历史状态。将历史状态视作状态的一种。如果退出时复合状态的当前子状态是一个基本（BASIC）状态时，θ(S)返回该子状态；否则，返回该复合子状态的入口（ENTRY）状态。

历史状态：使用谓词HasHistory(S)=∃b∈η(S).History(b)，如果HasHistory(S)存在，那么谓词HEntry(S)表示S唯一的历史状态。如果谓词HEntry(S)不存在，那么HEntry(S)表示复合状态S默认的入口状态。如果S是基本（BASIC）状态，那么HEntry(S)=S。如果上述情况都不是，那么HEntry(S)未定义。

定义3（内部转换）定义“internal_transition”表示源状态和目的状态位于同一复合状态内的转换。经过该转换，变量的值将会从V1更新到V2。

为了描述穿越复合状态边界的转换，定义了“进入转换（entering_transition）”和“退出转换（exiting_transition）”。

对于每个复合状态，都有一个默认入口状态和一个默认出口状态。当转换以外部状态作为源状态并以内部状态作为目标状态时，它需要使用进入转换。

如图3 中的Entering 所示，可以看到“进入转换”源状态的父状态（即η-1(S)）和目标状态的祖父状态（即η-2(S1)）是相同的状态。进入转换分为两个步骤：（1）从外部状态到复合状态的入口状态（即S1）的转换；（2）从入口状态到目的状态的转换。

当转换以内部状态作为源并将外部状态作为目标状态时，它需要使用退出转换。

退出转换与进入转换类似，但源状态的祖父状态（即η-2(S1)）和目标状态的父状态（即η-1(S′)）是相同的状态。退出转换分为两个步骤：（1）从源状态到复合状态的出口状态（即S1）的转换；（2）从出口状态到目的状态的转换。

定义4（层次转换）层次转换HT:S→g,aS′是从一个复合状态迁移到另一个复合状态的转换。层次转换包括三部分：（1）执行“退出转换”，退出复合状态S；（2）执行转换本身；（3）执行“进入转换”，进入复合状态S′。

经过层次转换可以得到新的系统状态(ρ1,μ1,θ1)，其中：

定义5（状态转换）定义状态转换Tst：

每个系统状态都由三部分组成：ρ、μ和θ。经过状态转换后，系统状态将被更新为ρ1、μ1和θ1。

5 图形化建模工具的实现

在实现方面，由于使用Graphiti进行图形化工具开发需要以EMF（eclipse modeling framework）模型为基础，因此在图形化工具开发之前首先需要对AADL-HBA 进行EMF 模型的建立。由于AADLHBA 是在AADL-BA 基础上扩展，因此本章以扩展AADL-BA元模型的方式得到HBA元模型。

5.1 扩展AADL行为附件元模型

AADL 行为附件与AADL 核心联系紧密，因此AADL行为附件元模型重用了AADL元模型的EMF框架，并在此基础上加以设计。这一方面有利于促进AADL-BA 在OSATE2 中的整合；另一方面，使用相同的形式来制定两个元模型可以简化对象依赖关系的表达，并简化二者之间的模型连接。

图4 显示了通过EMF 扩展（例如，Java 的继承机制）来表达两个元模型之间的依赖关系。可以看出，BehaviorAnnex扩展了AnnexSubclause，BAElement扩展了Element。后者简化了从AADL-BA模型到AADL模型的链接，可以轻松地检索相应的AADL对象。

为了扩展AADL 行为附件，首先扩展AADL 元模型，增加并发状态和复合状态的表达（见图5 中粗体部分）。

如图5所示，层次行为附件和AADL行为附件之间的主要区别在于添加了composite state 和concurrent state。另外，为了符合上述约束，相应地添加了诸如进入状态和退出状态的状态类型。

Fig.4 AADL-BA meta-model dependency图4 AADL-BA元模型依赖

Fig.5 Extended AADL behavior annex HBA meta-model(part)图5 扩展后的AADL行为附件HBA元模型（部分）

5.2 使用ANTLR和Xtext技术生成Java代码

ANTLR（another tool for language recognition）是一个解析器生成器，用于读取、处理、执行或翻译结构化文本或二进制文件。它广泛用于构建语言、工具和框架。从语法上看，ANTLR 生成一个可以构建并解析抽象语法树的解析器。

Xtext 是开发编程语言和领域特定语言的框架。可以通过Xtext 语法来定义语言，并据此获得完整的基础架构，包括解析器、链接器、类型检查器以及编译器。

使用AADL-HBA builder factory来指定如何构建AADL-HBA 抽象语法树（abstract syntax tree，AST）。它确保AST 符合AADL-HBA 元模型。使用ANTLR框架从定义的AADL-HBA语法中生成词法分析器和解析器的Java类。

OSATE 是一个开源环境，为基于AADL 的复杂嵌入式系统开发架构模型提供支持，包括对AADL的建模和分析。AADL 行为附件插件基于Xtext 技术，可以在互联网上下载AADL 行为附件的元模型（Xtext的输入）。因此，利用EBNF（extended Backus-Naur form）扩展了BA的元模型。

6 HBA到TA的转换

本章介绍层次行为附件（HBA）到时间自动机（TA）的转换规则。

虽然David等人提出了层次时间状态机的概念，并给出了形式化的语法、语义定义，但并没有进一步实现，也没有相应的集成工具支持。因此，为了使模型能够被现有工具集分析，给出了一套扁平化算法，用于将HBA 翻译成现有工具UPPAAL 的输入——TA，并利用UPPAAL验证模型属性。

6.1 扁平化算法

在本文的工作中，使用UPPAAL 进行形式化验证。正如前面所提到的，需要在验证之前将层次结构扁平化。在UPPAAL 中，每一个时间自动机被称作“模板”，节点被称作“位置”。扁平化算法共有8步：

（1）对于层次行为附件M中的每一个自动机F，如果F不是顶层自动机，那么该自动机增加一个新的位置，命名为ReadyState。

（2）对于每一个转换t，如果它的目的状态是复合状态S（composite或concurrent状态），那么增加一个从ReadyState状态到S的入口状态的转换，并且转换的警卫条件与转换t的警卫条件一致。

（3）为了同步多个相关自动机的执行，对于所有目的状态是复合状态的转换t，为其增加一个发送同步信号，记为发送（！）。

（4）对于每个XOR类型的复合状态S（composite状态），为其对应的子状态机，增加的从ReadyState状态到S的入口状态的转换，为该转换增加接收同步信号，记作接收（？），同步信号与（3）中相同。

（5）对于AND 类型的复合状态S（concurrent 状态），为其每个子状态机，增加的从ReadyState状态到S的入口状态的转换，为该转换增加接收同步信号，记作接收（？），同步信号与（3）中相同。

（6）同理，对于所有源状态是复合状态的转换t，为其增加一个接收同步信号，记为接收（?）。

（7）对于每个XOR类型的复合状态S（composite状态），为其对应的子状态机，增加的从S的出口状态到ReadyState状态的转换，并为该转换增加发送同步信号，记作接收（！），同步信号与（6）中相同。

（8）对于AND 类型的复合状态S（concurrent 状态），为其每个子状态机，增加的从出口状态到ReadyState 状态的转换，为该转换增加发送同步信号，记作发送（！），同步信号与（6）中相同。

6.2 转换规则

首先简单介绍时间自动机TA 的语法定义。一个时间自动机A是一个六元组。其中，L是一个有穷的位置集合；L0⊆L是初始位置的集合；Σ是一个有穷符号集合；X是一个有穷时钟的集合；I是一个映射，它给L中的每个位置s指定Φ(x)中的一个时钟约束；E⊆L×Σ×2X×Φ(X)×L是一个转换集合。表示输入符号a时，从位置s到s′的转换。φ是X上的一个时钟约束，它在转变发生时被满足；λ⊆X是在该转换发生时复位零值的时钟集合。

由于扁平化后的HBA 与TA 有着相同的自动机形式，因此可以通过简单的映射规则完成HBA到TA的映射。

7 案例分析

在实际工程中，对导航、制导与控制系统（guidance,navigation and control system），即GNC系统建模并生成初始模型。由于文章空间的限制，只在本文中介绍GNC 系统中的姿态控制线程的精化，作为本文的演示。

7.1 姿态控制线程

7.1.1 需求描述

姿态控制线程有4 个状态：姿态控制状态、稳定状态、遥测状态、系统监测状态。姿态控制线程的功能行为如图6所示。假设此时卫星已正常运行，处于稳定状态（实际案例中当星箭分离后，卫星需要先通过姿态控制和轨道控制调整自身位置后，再进入稳定状态）。其中稳定状态为初始状态。当卫星处于稳定状态时，若接收到姿态调整指令，则进入姿态控制状态；若接收到遥测指令，则进入遥测状态；若接收到系统监测指令，则进入系统监测状态。当姿态调整完成后，卫星将发送姿态调整完成信号，并返回稳定状态。当遥测状态结束时，卫星将发送遥测结束信号，并返回稳定状态。当卫星处于系统监测状态时，若接收到监测终止指令，卫星将返回稳定状态。

Fig.6 Attitude control thread functional behavior图6 姿态控制线程的功能行为

上述需求是架构设计师设计的，他们可能不会考虑每个模块的内部处理细节。内部细节将在精化阶段由设计人员补充。

7.1.2 使用行为附件建模

此处，行为附件用来建模第一次的精化行为。AADL代码如下所示：

上述案例对应的图形化效果如图7所示。

7.2 精化

7.2.1 需求精化

以姿态控制模块为例，介绍各模块的精化。姿态控制包括滚动姿态机动状态、姿态偏置飞行状态、滚动姿态返回状态三个正常状态以及陀螺仪安全、飞轮安全状态两个异常状态。姿态控制模块的功能行为如图8所示。

当接收到姿态调整指令后，系统进入姿态机动状态。检查三轴（X、Y、Z轴）飞轮角动量值与陀螺仪状态，若三轴同时满足角动量不大于4 Nms，并且陀螺仪可用，则进入姿态偏置飞行状态；否则，若角动量不满足上述条件，则进入角动量调整状态；若陀螺仪不可用，则进入陀螺仪安全状态。

Fig.8 Control state functional behavior图8 控制状态内部的功能行为

当卫星处于偏置飞行状态时，若控制姿态角大于或等于13°，则进入飞轮安全状态；否则，偏置飞行结束后，进入姿态返回状态。

姿态返回状态发送姿态调整信号后，退出姿态控制状态。

7.2.2 使用层次行为附件建模

使用层次行为附件对姿态控制模块建模。首先将姿态控制状态设置为复合状态（composite state），然后为姿态控制状态添加子状态描述，HBA 代码如下所示：

当双击图7中的ControlState后，可以看到图9所示的自动机。

7.3 形式化验证

根据第6 章提出的转换规则，将上述HBA 转换为UPPAAL 的输入——时间自动机网络，如图10 所示。本章中详细描述的顶层模块和姿态控制模块对应的时间自动机如图11和图12所示。

在此基础上，可以对死锁、安全性、活性等性质进行验证，例如：

（1）系统不存在死锁，A[]!deadlock。

（2）安全性，如“当系统处于姿态控制状态时，机动状态一定会被激活”，A[](ac.ControlState)imply(atcm.Maneuver)。

（3）活性，如“系统终究会进入稳定模式”，E＜＞(ac.StableState)。

通过将上述待验证性质输入到UPPAAL 的验证器中后，得到如图13 所示结果。从结果图中可以看出，系统不满足“系统无死锁”性质。

Fig.9 Control state graphical display图9 控制状态内部的图形化展示

Fig.10 TA network of attitude control thread图10 姿态控制线程的时间自动机网络

Fig.11 TA representation of attitude control thread图11 姿态控制线程的时间自动机表示

Fig.12 TA representation of attitude control state图12 姿态控制状态内部的时间自动机表示

Fig.13 Verification result of attitude control thread图13 姿态控制线程验证结果

经分析查验发现，在需求描述中，针对顶层姿态控制线程有如下时间属性描述：姿态控制线程周期性调度，调度周期为360 ms。在稳定模块中，有如下属性描述：在稳定模块中，当系统处于数据采集（dataCol）阶段，若在一个线程周期内未收到数据信息，则使用上一周期数据进行检测；若连续三次未收到数据信息，则报告数据采集异常。当收到数据信息后，经过600 ms 延迟，确认无新数据到达时，进入数据校验（check）阶段。

通过查看反例和仿真，发现系统上述需求会导致系统停留在稳定模块中的数据采集阶段，当一个线程周期（60 ms）结束后，未达到600 ms 延迟的要求，因此系统无法继续迁移。针对上述问题，将系统延迟时间缩小后更新模型，发现系统无死锁。

8 相关工作

在层次扩展方面，Harel[15]通过扩展UML 状态机图提出了层次自动机的概念，解决了复杂系统状态机规模大、层次嵌套深的问题，但嵌入式安全关键软件的实时性描述仍然缺乏。为了解决时间自动机无法描述层次模型的问题，David[11]提出了层次时间自动机（HTA）的概念，并通过扩展时间自动机来解决复杂的层次系统建模和验证问题。HTA可以建模分层系统并验证它们的时间属性，但它需要将模型手动转换为自动机形式，这增加了工作的复杂性。

在形式化语法和语义方面，David[11]给出了层次化扩展的HTA 的形式化语法和操作语义，并给出了一个简化的HTA模型。Yang等人[8]通过时间抽象状态机（time abstract state machine，TASM）定义了AADL行为附件的形式语义，并提出了一个实时行为建模和验证原型。Zhou等人[16]给出了UML状态机图的基本语义和MARTE（modeling and analysis of real time and embedded systems）的时间依赖建模元素，并提出了基于扩展层次结构的操作语义的形式化时间自动机。Ölveczky 等人[17]为AADL 的行为子集提供了一个形式化的实时重写逻辑语义，其中包括其行为附件的基本方面。为了在AADL架构下支持明确的推理、形式化验证以及高保真仿真，Besnard等人[18]定义了AADL 行为附件的形式语义。Larson 等人[19]提出了嵌入式系统软件的行为语言（behavioral language of embedded system software，BLESS），它是AADL 的行为接口规范语言和证明环境。BLESS为AADL行为描述和自动生成验证条件提供了形式语义。Ahmad等人[20]提出了AADL模型的同步子集的形式语义。通过使用他们开发的定理证明器——HHL（hybrid hoare logic）prover 可以验证AADL 模型的正确性。Johnsen等人[21]对AADL核心的一个子集进行了形式化，并将其转换为UPPAAL 的输入语言TA。他们通过语义锚定的方法将AADL 子集映射到时间自动机，给出了AADL子集的形式化语义定义。França等人[12]分别通过实际工程项目评估了AADL-BA 的实用性，分析了AADL-BA 的约束条件，提出了行为附件层次化扩展的思想，但没有给出形式化定义和实现。

在混合建模方面，Ma 等人[22]使用高级建模语言AADL 进行系统架构设计；使用基于同步语言SIGNAL的形式化框架Polychrony进行分析和验证。Yu等人[23]通过利用AADL 对嵌入式系统架构建模和利用Simulink对嵌入式系统功能建模，并通过形式化的多时钟模型分析和验证了系统的时间属性。

9 总结与展望

本文通过扩展AADL 行为附件元模型的方式，对AADL功能行为描述能力进行了层次化扩展。通过提出层次行为附件（HBA）的方法，解决了建模过程中难以管理大量状态以及结构层次丢失的问题。本文给出了层次行为附件的形式化语法约束以及形式化语义定义，通过对AADL 行为附件元模型的扩展，基于Xtext以及Xtend技术，在AADL开源开发环境OSATE上实现了对应的工具插件。为了便于形式化验证，本文给出了HBA到时间自动机TA的转换规则。最后，通过案例分析，验证了方法的有效性。

AADL行为附件自身支持timeout、dispatch、computation 等时间相关描述，本文所提层次行为附件扩展主要关注组件功能行为的描述，对原有时间属性没有扩展。因此，扩展后的层次行为附件仍然支持原AADL行为附件支持的时间描述。对于层次化扩展而引入的时间相关属性的计算与判别问题，是下一步研究工作的重点。