基于NuSMV的AADL模型形式化验证技术

刘畅，蒋永平，马春燕,*，张涛

1.中国航空无线电电子研究所，上海 200233 2.西北工业大学 软件学院，西安 710072

为保障任务关键系统的高可靠性需求，在软件系统的设计阶段对任务关键属性进行形式化验证是有效的技术手段之一。

AADL(Architecture Analysis and Design Language)是一种描述嵌入式系统架构的建模语言，在航空航天领域广泛被应用。为在任务关键系统模型设计的早期阶段，对AADL模型的任务关键属性和系统行为的正确性进行验证，NuSMV(New Symbolic Model Verifier)形式化模型发挥着重要的作用，NuSMV使用有限状态机描述NuSMV模型，使用时态逻辑公式描述待验证属性，对相关属性进行验证。由于NuSMV工具的输入语言支持以模块化分层方式构建的复杂而庞大的系统，与AADL的层次化方式建立系统模型的思想一致。因此，可以通过将AADL模型转换为NuSMV形式化模型，完成AADL模型的形式化验证，如果验证失败，NuSMV会给出反例路径，方便模型验证人员快速定位问题来源，对模型进行优化。

目前已有多项研究将AADL模型转化为形式化语言描述的模型，如LNT、Event-B、BIP、Maude、TASM及CSP等，然后对AADL模型的相关建模属性进行正确性验证。然而，这些工作仅考虑一个小的AADL子集，未涵盖全部AADL软构件以及相关行为、配置相关的建模要素，而这些关键的建模元素在模型的正确性验证中较为常见。本文拟采用NuSMV对AADL模型的安全性和活性等属性进行验证。

1 相关工作

Mkaouar等介绍了一种AADL模型子集到LNT的转换方法，通过CADP工具对系统并发正确性进行验证。文献[6]使用Event-B对AADL模型架构进行形式化验证，但不包括行为模型的属性验证。本文研究团队丰富了AADL行为模型及可调度性等验证内容，采用Event-B对AADL模型进行形式化验证。

Yang等将AADL转换为抽象实时状态机TASM，并基于定理证明器(Coq)对转换的语义一致性进行验证。刘倩等基于UPPAAL工具，对AADL模型可调度性进行分析，但其时间自动机模型不提供对时钟的暂停及恢复，存在一定局限性。

Yang等使用可达自动机CSP构建AADL的形式化语义，并且使用FDR工具验证死锁和活锁。文献[13]使用HCSP构建AADL子集的形式化语义，并通过定理证明的方法验证AADL模型行为附件的正确性。Zhang等介绍了一种从AADL模型到CSP的映射规则，并使用PAT(Process Analysis Toolkit)验证AADL的安全性、活性等任务关键属性。

文献[15]将AADL转换为NPTA(Networks of Priced Timed Automata)并且基于UPPAAL-SMC提出系统性能定性评估的方法。文献[16]将AADL模型转换为SIGNAL模型，并提供多时钟约束的调度性分析。文献[17]提出了利用NuSMV对AADL模型进行验证的思想，但缺乏AADL模型到NuSMV模型的映射规则，以及采用NuSMV对AADL模型进行形式化验证的系统化方法，仅通过一个案例说明如何利用NuSMV对AADL模型进行验证。

对以上研究工作进行总结，可以发现前人方法存在以下3点不足。

1)部分研究工作考虑的AADL模型要素比较少，这样会导致无法描述比较复杂的系统。

2)大部分研究工作没有证明其方法的正确性，无法保证形式化模型与源模型语义一致。

3)模型系统待验证属性比较单一，局限性比较大。例如只支持LTL(Linear Temporal Logic)规范，这样无法描述包含全称和存在量词的属性。

为了弥补这些缺点，本文提出基于NuSMV的AADL模型验证方法。

2 AADL和NuSMV

AADL是系统架构分析和设计语言，提供了系统和软硬件构件以及构件之间交互关系的建模要素，AADL模型可以作为航空嵌入式系统的设计模型。AADL的软件构件包含系统、子系统、进程、线程、线程组、数据和子程序，每个软件构件都由类型和实现构成。AADL系统构件或软件构件的任务级模态是其所包含的构件、连接和属性值关联的显式配置，代表系统或软件构件可选的操作状态模态，模态配置也可以指定线程或子程序中要使用的不同调用序列，还可以表示在不同属性值下的软件构件(例如线程或子程序)的不同行为。系统或软件构件行为的描述通过AADL行为附件(Behavior Annex)进行建模，例如描述构件的子程序调用、异步和时序等行为。

NuSMV是一套基于符号模型检测技术的形式化建模语言和工具，用于有限状态系统的形式化验证，可以用于分析计算树逻辑(CTL)和线性时序逻辑(LTL)表示的属性，例如，安全性属性和活性属性。NuSMV程序由模块(MODULE)构成，模块定义由形参(Paramenter)和主体(Body)组成。模块主体由描述状态集Variables、转移关系和对模型的一些约束Constraint、待验证的规范Specification组成。

3 AADL模型到NuSMV模型的转换方法

AADL模型到NuSMV模型的转换方法的研究分为2个阶段：确定需要转换的AADL子集；建立从AADL模型子集到NuSMV模型子集的映射规则。

3.1 需要转换的AADL子集

本文只考虑AADL模型的软件构件(数据、子程序、线程、进程)和系统构件5种构件类型(component_type)，如表1所示。

图1采用类图展示了需要转换的AADL模型建模要素及AADL构件的包含关系，系统构件可以包含系统构件、进程构件、子程序构件和数据构件，进程构件可以包含线程构件和数据构件，线程构件可以包含子程序构件和数据构件，子程序构件可以包含数据构件。表1中构件类型和构件子元素类型在图1中用类名表示，构件子元素类型的构成要素用类的属性表示。

表1 需要转换的AADL子集Table 1 Subsets of AADL to be transformed

图1 需要转换的AADL建模要素Fig.1 AADL modeling elements needed to be con-verted

3.2 AADL模型到NuSMV模型的映射规则

映射规则是基于AADL元模型和NuSMV元模型提出来的。为了保证映射规则的完整性、以及一致性，每条映射规则都满足从AADL元模型到NuSMV元模型节点的一对一映射，即每条映射规则都是同构映射。本节描述了AADL模型构件到NuSMV模块的7类映射规则，分别对应构件类型及构件包含的6类子元素到NuSMV模型的映射规则。

图2用UML类图表示映射得到的NuSMV模型。AADL中的system、process、thread、subprogram和data构件分别映射为NuSMV中MODULE_main、MODULE_process、MODULE_thread、MODULE_subprogram和MODULE_data等5种类型的模块(MODULE)，这些模块均继承MODULE_component，除了MODULE_data，其余4种模块属性一致，均包括多个MODULE_feature实例、多个MODULE_connection实例、一个枚举类型的modes变量、多个枚举类型的flow变量。NuSMV程序以main模块作为验证入口，main模块对应AADL模型中的系统根节点。AADL构件的模态(modes)、数据流(flows)可以用NuSMV中的基本数据类型表示。

对本文提出的7类映射规则进行详细阐释，并结合算法1中的AADL进程构件MissionLoadP及其映射的NuSMV模块为案例进行说明。

图2 映射得到的NuSMV模型Fig.2 NuSMV model obtained by mapping

3.2.1 映射规则Rule1

Rule1表示根据AADL构件A的类型，将构件映射为NuSMV模块A。如果构件A为系统构件，则映射为图2中的main模块(MODULE_main)；如果构件A为进程构件，则映射为MODULE_process，其他构件类型同理。图3中的MissionLoadP进程构件映射为MissionLoadP模块。

1) 进程模块中的布尔变量isActive标记其在系统模态下是否有效。

2) 线程模块中的布尔变量isBehavior标记线程组件在当前进程模态下是否执行其行为。

3) 进程模块isActive变量的值随着系统模块模态切换而变换。线程模块的isBehavior变量的值随着进程模块的模态切换而变换。

3.2.2 映射规则Rule2

构件A的features在表1中表示feature的集合。该集合中的每一个feature映射为一个feature MODULE实例，该实例会被connection模块实例引用。特征模块的定义如下：

MODULE feature(feaType,feaDirec)

DEFINE

Type:= feaType;

Direc:= feaDirec;

1) feaType 代表特征类型，AADL中定义的特征类型有抽象特征(Feature)、端口特征(Port)、参数特征(Parameter)、数据构件访问特征(Data Access)。在转换后的NuSMV模型中分别用1代表抽象特征(Feature)，2代表数据端口特征(Data Port)，3代表事件端口特征(Event Port)，4代表事件数据端口特征(Event Data Port)，5代表参数特征(Parameter)，6代表数据访问特征(Data Access)。

算法1 AADL进程构件及其映射的NuSMV模块

图3 元模型和模型实例之间的映射关系Fig.3 Mappings between metamodels and models

2) feaDirec 代表特征方向，AADL中定义的特征方向有输入(in)、输出(out)、输入输出(in out)、提供(provides)、请求(requires)。本文在转换之后的NuSMV模型中用-1代表输入(in)、1代表输出(out)、0代表输入输出(in out)、-2代表请求(requires)，2代表提供(provides)。

3) 如果构件的特征接口为事件端口特征(event port)或事件数据端口特征(event data port)，除了映射特征模块实例，还需要在映射后的模块中定义布尔类型变量，表示对应端口上的事件是否发生，该变量为TRUE代表事件到达，为FALSE代表事件未到达。该布尔类型变量可以作为模态转换或行为状态转换的条件。

算法1中MissionLoadP进程特征“reqDispandControl: in event port”映射为MODULE MissionLoadP中的“reqDispandControl：feature(3,-1)”。

3.2.3 映射规则Rule3

每个子构件映射为一个MODULE实例，所有子构件映射的MODULE实例均会被MODULE A引用。如果subcomponent_name是AADL构件A的某一个子构件的名字，component_type是子构件的类型，则映射的MODULE实例名为subcomponent_name，映射的MODULE实例的类型为component_type。

算法1中的MissionLoadP进程构件包含线程子构件getLocalPlaneAttributeInfo。线程子构件在模块MissionLoadP中表示为getInfo： getLocalPlaneAttributeInfo()。

3.2.4 映射规则Rule4

构件A的connections在表1中表示connection的集合，该集合中的每一条connection映射为connection MODULE实例。该实例会被模块A引用，连接模块的定义如下：

MODULE connection(src_feature,dst_feature,conn_type)

VAR

isWorking： boolean;

1) src_feature 对应连接的源特征，其类型为特征模块(即MODULE_feature)。

2) dst_feature 代表连接的目的特征，其类型为特征模块(即MODULE_feature)。

3) connType 代表连接类型，分为同级构件相连的连接类型、构件到子构件的连接类型及构件到父构件的连接类型，本文在NuSMV中分别用0、-1、1表示。

4) isWorking用以验证该连接在的模态下是否有效，其默认值为TRUE。

算法1中的“conn1:port getInfo.outport→returnPlaneInfo”映射为“conn1:connection(getInfo.outport,returnPlaneInfo,1)”，getInfo.outport为源特征，returnPlaneInfo为目的特征，1表示构件MissionLoadP的子构件端口到该构件端口的连接。

3.2.5 映射规则Rule5

构件A的modes在表1中表示modes子元素类型，其映射为枚举类型的modes变量，例如，该枚举变量表示为modes:{mode1, mode2, mode3}，其中，mode1、mode2、mode3对应表1中modes子元素类型的构成要素modes_set。算法1中的进程MissionLoadP的modes的转换，枚举值对应构件所有的操作状态，模态之间的转移关系用NuSMV中的next()表达式和case语句表示。

3.2.6 映射规则Rule6

构件A的behavior_annex在表1中表示behavior_annex子元素类型，映射为一个behavior MODULE实例，例如算法1中的线程getLocalPlaneAttributeInfo 行为附件的转换满足以下映射规则：

1)行为附件中的变量(variables)转换为NuSMV模块中的变量声明。

2)行为附件的状态集合(states)转换为NuSMV模块中枚举类型的变量声明。NuSMV模块中states变量的枚举值对应行为附件中定义的状态，包括initial状态、complete状态、final状态和execution状态。

3)行为附件中的复合状态被分解为多个原子状态。比如s0为initial和complete的一个复合状态，转换成s0_initial和s0_complete 2个状态。

4)行为附件的转移关系(transitions)映射为NuSMV的next(states)函数和case语句，描述AADL行为中行为状态的转移关系。

3.2.7 映射规则Rule7

构件A的flows在表1中表示flow的集合，该集合中的每一个flow映射为一个枚举类型变量，例如AADL中flow映射为NuSMV中枚举变量： flow: {feature,feature,…,feature}，其中，feature,feature,…,feature对应流s1经过的个特征集合。流的转移关系用NuSMV中的next()表达式和case语句表示，例如，算法1中从getLocalPlaneAttributeInfo线程的端口和进程MissionLoadP的端口形成的流s3到NuSMV模型的转换体现了该映射规则。

3.3 NuSMV模型的生成算法

基于上述7条规则的NuSMV模型生成算法如算法2所示。该算法以AADL模型构件为输入，以生成的NuSMV模块为输出，create表示生成NuSMV元素，VAR表示生成NuSMV变量，ASSIGN表示生成变量的转移关系，next(var)表示用NuSMV中的next语句描述var的转移关系。

算法2描述了AADL构件的NuSMV模型生成方法。该算法的输入为AADL语言表示的构件A，构件A的生成方法分为以下8步：

算法2 NuSMV模型生成算法

1) 首先根据构件A的构件类型生成对应的NuSMV模块，按照映射规则Rule1,如果是system，则创建MODULE_main，否则生成MODULE_component_name，如算法2的第1～5行所示。

2) 然后根据构件A包含的子元素类型，生成对应的NuSMV元素。如算法2的第6～50行所示。

3) 如果构件A包含features，按照映射规则Rule2生成每个feature对应的feature_MODULE实例，如算法2的第8～12行所示。

4) 如果构件A包含subcomponents，按照映射规则Rule3生成每个subcomponent对应的MODULE实例，如算法2的第13～23行所示。

5) 如果构件A包含connections，按照映射规则Rule4生成每个connection对应的connection MODULE实例，如算法2的第24～31行所示。

6) 如果构件A包含modes，按照映射规则Rule5生成modes变量，如算法2的第32～34行所示。

7) 如果构件A包含behavior_annex，按照映射规则Rule6生成behavior MODULE实例，如算法2的第35～42行所示。

8) 如果构件A包含flows，按照映射规则Rule7生成每个flow对应的枚举类型变量，如算法2的第43～49行所示。

4 AADL模型到NuSMV模型转换方法的正确性证明

模型转换的正确性表现为映射规则满足AADL语义保留、确定性以及有限性等性质。本采取图同构的方法对本文模型转换方法的正确性进行验证。

本文的转换方法是基于AADL元模型和NuSMV元模型提出的，AADL元模型中的节点要素到NuSMV元模型中的节点要素是一一对应的，满足图同构的定义。本文通过证明转换后的NuSMV模型实例与源AADL模型实例语义一致，说明AADL模型到NuSMV转换方法的正确性。证明思路如图3所示。

图3表示元模型和模型实例之间的映射关系，其中Ins(MMt)指目标语言的模型实例；表示源语言元模型到目标语言源模型的转换；表示源语言模型实例到目标语言模型实例之间的映射；、′分别表示源语言和目标语言元模型到模型实例之间的映射；表示源语言元模型到目标模型实例之间的映射关系；MMs表示AADL元模型；MMt表示NuSMV的元模型。映射函数和′为类型保留映射 (Type Prserve Mapping,TPM),TPM由OMG(Object Management Group)定义。

由3.1节可知，根据提出的AADL元模型和NuSMV元模型类图之间的同构映射，映射函数是图同构的。本节将证明AADL元模型与其模型实例Ins(MM)之间的类型保留映射函数是图同构的，同时证明(∘)是图同构的，在此基础上证明AADL模型实例到NuSMV模型实例的模型转换函数是图同构的。

定义一个图同构函数表示图从图到图的转换：=(:→,:→),其中，为图的节点集合；为图节点到图节点集合的映射函数;为图的节点集合;为图边缘节点集合到图边缘节点集合的映射函数；为图的边缘节点集合；为图的边缘节点集合。满足以下约束:

(1)

式中：、分别为同时作用于图的节点和边缘节点的转换函数。

元模型MM为一个UML(Unified Modeling Language)类图，Ins(MM)为一个UML对象图。TPM函数从MM映射为Ins(MM)，Ins(MM)中的每一个元素都是MM中类的映射。

如果元模型MM为UML类图，模型实例Ins(MM)为UML对象图。那么在元模型图及其实例图之间定义的TPM函数是图同构的。

根据命题1，在AADL元模型类图到NuSMV元模型类图的转换中，因为AADL元模型元素到其模型实例元素之间，以及NuSMV元模型元素到其模型实例之间的映射都是类型保留映射TPM，所以映射函数和′是图同构的。

如果映射函数是图同构的，并且映射函数是图同构的，那么和的组合∘也是图同构的。

根据命题2，因为函数、是图同构的，所以(∘)是图同构的。

已知在元模型MM和MM′之间存在同构映射，元模型MM和它的实例Ins(MM)之间存在类型保留映射函数，元模型MM′和它的实例Ins(MM′)之间存在类型保留映射函数′，则Ins(MM)和Ins(MM′)之间的映射函数是图同构的。

如图3所示，上文已经证明函数、、′、都是图同构的，分别用式(2)～式(5)表示

(MM)=MM’′是图同构

(2)

(MM)=Ins(MM)是图同构

(3)

(MM)=Ins(MM′)是图同构

(4)

(MM)=′((MM))=Ins(MM′)是图同构的

(5)

根据定义1和式(2)，可得

(6)

根据定义1和式(5)，可得

(7)

假设如图3所示，=∘，将式(7)中的替换成∘，可得

(8)

根据式(8)，因为是图同构的，结合定义1的约束，据此推断映射函数也是图同构的。

本转换方法是基于源模型和目标模型的语法结构以及源模型语义角度提出的。基于源模型和目标模型的语法结构采用上下文无关文法描述，是精确无二义性的，所以模型转换为一对一映射，是确定的。同时AADL模型的构成要素是有限的，因此转换方法是有限的。

综上，证明了本文从AADL模型至NuSMV模型转换方法的正确性。

5 基于NuSMV模型的验证方法

5.1 安全属性的验证

本文验证的安全属性(Safety)包括状态、模态的可达性和转换的确定性。

5.1.1 可达性验证

在状态迁移系统中，如果事件或者消息到达指定端口，将会切换为另一个状态。状态的可达性验证指在所有可能的状态转换序列中，是否存在目标状态不可达的情况。

1) 模态可达性验证

模态的可达性指当事件数据端口上有事件到达时，一个模态能够转换为另一个模态的能力。例如，图4(a)展示了一个由于模态3没有传出转换导致的非可达性示例，图4(b)展示了一个满足模态可达性的示例。对于图4，在NuSMV中，表示是否存在从mode1到mode3的模态转换序列，模态可达性的CTL描述为

AG(modes=mode1→AF(modes=mode3))

(9)

2) 行为附件状态可达性验证

行为附件状态的可达性指卫式(Guard)满足时，从一个行为状态切换到另一个行为状态的能力，卫式是指状态转换时满足的约束条件。例如，图5(a)表示由于s1和s2没有传出转换，所以从s2到s1，或从s1到s2都是不可达的；图5(b) 表示了一个状态可达的案例。在NuSMV中，表示是否存在从s1到s2的行为状态转换序列，行为附件状态的可达性CTL描述为

AG((states=s1) →AF(states=s2))

(10)

图4 模态可达性示例Fig.4 Example of mode reachability

图5 行为状态可达性Fig.5 Example of state reachability

5.1.2 确定性验证

状态转换分为确定性和非确定性。在一个状态上，对于同一个转换条件，有且只有一条转换，则称该转换是确定性的，否则为非确定性的。AADL模型中的模态和行为状态转换必须是确定性的。例如，图6(a)所示为当port1上的事件到达时，模态会从mode1向mode2转换，或向mode3转换，这属于非确定性的模态转换；图6(b) 所示为确定性的模态转换案例，对每一个源模态，每一个转换条件只存在唯一的传出转换。NuSMV表示到mode2模态的转换是否是确定性的，对应的CTL规范描述为

AF modes = mode2

(11)

图6 模态转换的确定性Fig.6 Example of deterministic mode transition

5.2 活性属性的验证

活性属性指“计划的事情最终一定会发生”。活性属性验证包括进度属性的验证。进度属性指“如果满足某些条件，某些事情最终一定会发生”。AADL模态切换、行为附件中行为状态的切换皆定义了进度属性。NuSMV中，如果模态切换的条件(Event)满足，模态将会按照计划切换为mode2，模态进度属性的CTL规范描述为：AG(event →AF(modes=mode2))；如果行为状态转换的条件满足，行为状态将会按照计划变成S0状态，行为附件中行为状态的进度属性对应的CTL规范描述为

AG(event → AF(states=S0))

(12)

5.3 模态配置的合法性验证

AADL模型中，构件对其所包含的子构件、连接等元素与模态的关联性进行配置，表示不同操作状态下的构件行为。本文对模态配置的合法性验证包括连接元素模态配置的合法性验证、子构件模态配置的合法性验证、流元素模态配置的合法性验证及系统构件下线程行为嵌套配置的合法性验证4部分。

1) 连接元素模态配置的合法性验证

AADL模型中连接表示不同构件之间的数据交互，连接元素模态配置的合法性指构件间的数据交互是否符合模态配置的要求。NuSMV中，conn1只在模态mode1下有效的性质对应的CTL规范描述为

A[!conn1.is Working U modes=mode1]

(13)

2) 子构件模态配置的合法性验证

AADL模型中，不同的模态指定了构件不同的操作状态。子构件模态配置的合法性指子构件的有效性是否符合构件模态配置的要求。映射规则Rule1中提到，进程模块的isActive属性标识进程模块是否在系统模块的模态配置下有效；线程模块的isBehavior属性标识线程模块是否在进程模块的模态配置下有效。NuSMV中，表示进程模块p在系统模态mode1下是否有效的CTL规范描述为

AF(modes=mode1 & p.is Active)

(14)

3) 流元素模态配置的合法性验证

AADL模型中，因为流元素的合法性与连接的合法性及子构件的合法性有关。所以流的可达性与模态配置具有一定的关联关系。

NuSMV中，表示在模态mode1下，流flow是否可以达到指定的特征接口，流元素模态配置的合法性属性对应的CTL规范描述为

AG(modes=mode1)→AF(flow=feature))

(15)

4) 系统构件下线程行为模态嵌套的合法性验证

AADL模型中，系统构件的模态配置影响进程构件的有效性，进程构件的模态配置影响线程子构件的行为执行。所以系统构件的模态配置，会间接对具体线程的行为执行产生影响。

系统构件下线程行为配置的合法性验证就是判断线程行为的有效性是否符合系统定义的模态配置。NuSMV中，表示在系统模态mode2下，进程构件p中的线程构件t是否能够正常执行，该性质对应的CTL规范描述为

AF(modes=mode2 & p.t.is Behavior)

(16)

6 实验验证

以包含人机交互子系统、备份子系统和自动飞行子系统的飞行控制系统为例，详细阐释了基于NuSMV的AADL模型形式化验证方法。

6.1 实验案例

人机交互子系统负责处理飞行员对飞机的操作指令，并且负责显示飞机的各项飞行参数。该子系统包含了显示控制进程和飞行员输入进程。显示进程将飞机的飞行参数展示给飞行员，并且根据飞行员的操作控制驾驶杆、油门杆和周边键等设备。飞行员输入进程包含3个分别处于不同计算机上的飞行员输入线程，当1个输入线程发生异常时，会由其他飞行员输入线程完成对飞行员输入信息的处理。

备份子系统的主要功能为备份重要的数据信息，当飞行控制系统发生异常状况时，能够根据备份信息恢复正常，备份子系统运行在PowerPC_G4处理器上。

自动飞行子系统主要功能为读取GPS(Global Positioning System)数据，发送控制信号至控制平台实现飞机的自动飞行，该子系统包括GPS读取线程以及自动导航线程。GPS读取线程仅在初始状态从GPS读取飞机位置信息，当开启自动驾驶后，自动导航线程开始运行，飞机进入自动驾驶状态。

6.2 实验案例——飞行控制系统的AADL模型

使用OSATE工具为飞行控制系统建模。该AADL模型包括人机交互子系统S_HCI、自动飞行子系统S_NAP和备份子系统S_BUP。

S_HCI包含1个飞行员输入进程构件P_Pinput和1个显示控制进程构件P_DIS，表示驾驶杆、油门杆和周边键的设备构件以及表示线程运行平台的处理器构件。P_Pinput包含3个绑定到不同处理器的飞行员输入线程T_Pilot_Input1、T_Pilot_Input2、T_Pilot_Input3。同时P_Pinput包含3个输入线程的模态配置，表示不同情况下不同线程的执行情况。飞行员输入线程为后台线程，当飞行员输入命令的时候会启动。P_DIS包括2个线程构件显示线程T_Screen_Disp和设备控制线程T_Control_Dev。显示线程每50 ms会刷新界面显示，设备控制线程根据飞行员输入信息控制驾驶杆、油门杆和周边键3个设备。

S_NAP中有2个模态：加载(load)和执行(run)。当自动飞行子系统接收到自动驾驶打开的事件，模态会由load变为run。导航控制进程P_Nav_Con只在run模态下正常执行。P_Nav_Con包含GPS读取线程T_GPS_Reader和自动导航计算线程T_AP_Compute，该进程构件有3种工作模态，即:GPS打开及自动导航关闭模态GPS_UP_AP_DOWN、GPS打开及自动导航打开模态GPS_UP_AP_UP、GPS关闭模态GPS_DOWN。如果GPS出现故障时，飞行控制系统不能自动飞行。

S_BUP包含1个备份进程构件P_BUP和PowerPC_G4处理器构件，P_BUP包含1个数据库访问线程构件T_DB_Operation，主要负责访问数据库中的备份信息，该线程构件与PowerPC_G4处理器构件的关系通过S_BUP子系统构件的Actual_Processor_Binding属性表示。

当导航控制进程处在GPS_UP_AP_DOWN模态时，如果飞行员将飞机驾驶状态调整为自动驾驶，则模态会变成GPS_UP_AP_UP模态，如果GPS发生故障，模态将会变成GPS_DOWN模态。T_GPS_Reader线程在GPS_UP_AP_DOWN和GPS_UP_AP_UP模态下都可以正常工作。该线程每隔20 ms从GPS获取一次数据。T_AP_Compute线程仅在GPS_UP_AP_UP模态下正常工作，该线程每隔50 ms会输出一次飞机的俯仰角、偏航角、滚动角信息给制动器，以实现飞机自动导航。

6.3 生成的实验案例——飞行控制系统的NuSMV模型

基于AADL模型到NuSMV模型的映射规则和转换算法，构建飞行控制系统的NuSMV模型。NuSMV模型包括：1个main模块，S_HCI、S_NAP和S_BUP 3个子系统模块,P_Pinput、P_DIS、P_BUP和P_Nav_Con 4个进程模块,T_Pilot_Input1、T_Pilot_In put 2、T_Polot_Input 3、T_Screen_Disp、T_Control_Dev、T_DB_Operation、T_GPS_Reader和T_AP_Compute 8个线程模块以及表示线程模块行为的行为附件模块；3个数据模块。例如，生成的P_Nav_Con进程模块(导航控制进程)如算法3所示，其中modes变量的转移关系如算法4所示，T_GPS_Reader线程模块及其行为附件模块如算法5所示。

算法3 导航控制进程模块

算法4 modes变量的转换关系

算法5 线程模块及其行为附件模块Algorithm 5 Thread module and behavior_annex module

6.4 实验案例——飞行控制系统的形式化验证

基于飞行控制系统NuSMV形式化模型，对其安全属性、活性属性以及模态配置的合法性进行验证，如果相应属性的验证结果为TRUE，则表示验证属性符合要求;否则NuSMV会给出一条反例路径，说明验证失败的原因，模型验证人员可以根据反例路径去完善建模方案。

6.4.1 安全属性的验证

安全属性验证包括可达性及确定性的验证。

1)可达性验证

①Nav_Control_Process模块modes的可达性验证

如果当前模态为GPS_UP_AP_DOWN，验证GPS_UP_AP_UP是否可达，该属性对应的CTL规范为

AG(modes=GPS_UP_AP_DOWN→

AF(modes=GPS_UP_AP_UP))

(17)

验证结果为TRUE表示Nav_Control_Process进程的GPS_UP_AP_UP模态满足从GPS_UP_AP_DOWN模态开始的可达性，否则模型存在故障。

② T_GPS_Reader行为状态的可达性验证

T_GPS_Reader的行为附件的reader1状态表示该线程调度完成，验证reader1行为状态是否可达。该属性对应的CTL规范为

AG(states=reader0→EF(states=reader1))

(18)

验证结果为TRUE表示T_GPS_Reader可以被正常调度，否则存在故障。

2)确定性验证。

对Nav_Control_Process的GPS_DOWN模态进行确定性方面的验证，模态的确定性保证了构件不同的操作行为都可以正常执行。该属性对应的CTL规范为

AF modes=GPS_DOWN

(19)

验证结果为FALSE，对NuSMV工具给出的反例路径进行查看，发现如果GPS_error事件一直未发生，进程模态就不会变成GPS_DOWN。在实际情况中，GPS错误事件有一定概率发生，这是由于未添加公平性约束导致的验证结果与预期不符。对GPS_error变量添加公平性约束并重新验证，模型满足该条属性。

6.4.2 活性属性的验证

1) Nav_Control_Process的GPS_UP_AP_UP模态的活性验证

GPS_UP_AP_UP表示GPS打开及自动导航打开模态，当人机交互子系统设置飞机为自动驾驶状态时，导航控制进程会接收到自动导航指令，工作模态也会变成GPS_UP_AP_UP。该属性对应的CTL规范为

AG(AP_Toggle_event→AF(modes=

GPS_UP_AP_UP))

(20)

验证结果为TRUE表示一旦飞行员设置飞机飞行状态为自动驾驶，Nav_Control_Process进程会在GPS打开及自动导航打开(GPS_UP_AP_UP)模态下执行。

2) T_GPS_Reader行为状态的活性属性验证

当T_GPS_Reader接收到改变驾驶状态的消息时，T_GPS_Reader会自动获取飞机位置信息。该属性对应的CTL规范为

AG(AP_Position_Input_event→AF(behavior_

specification.states=reader1))

(21)

验证结果为TRUE表示T_GPS_Reader线程只要接收到改变驾驶状态的消息时，总会成功执行其行为；否则模型存在故障。

6.4.3 模态配置的合法性验证

1) 连接元素模态配置的合法性验证

当Nav_Control_Process以GPS_UP_AP_UP模态工作时，与自动导航计算线程T_AP_Compute线程有关的连接应该是有效的。该属性对应的CTL规范为

A[!conn1.is Working U modes=

GPS_UP_AP_UP]

(22)

验证结果为TRUE表示在模态为GPS_UP_AP_UP时，连接conn1总是有效的，否则存在故障。

2) 子构件模态配置的合法性验证

T_AP_Compute仅在GPS_UP_AP_UP模态下才正常执行。该属性对应的CTL规范为

AF(modes=GPS_UP_AP_UP &

T_AP_Compute.is Behavior)

(23)

验证结果为TRUE表示T_AP_Compute符合Nav_Control_Process的模态配置定义，仅在GPS_UP_AP_UP模态下执行，否则存在故障。

3) 流元素模态配置的合法性验证

AADL模型中定义的数据流data，只有在模态GPS_UP_AP_UP下，才可以到达滚动角输出接口(Delta_Roll_Output)。该属性对应的CTL规范为

AG(modes=GPS_UP_AP_UP→AF(data=

Delta_Roll_Output))

(24)

验证结果为TRUE表示在GPS_UP_AP_UP模态下，流data总能达到滚动角输出接口，即流的有效性符合Nav_Control_Process的模态配置定义，否则存在故障。

4) 系统构件下线程行为配置的合法性验证Nav_Control_Process进程仅在自动飞行子系统模态为run时，才会正常执行。而Nav_Control_Process内的T_AP_Compute线程仅在进程模态为GPS_UP_AP_UP时，才会执行。验证系统模态为run模态时，T_AP_Compute线程是否会正常执行。该属性对应的CTL规范为

AF (modes=run & Nav_Control_Process.

T_AP_Compute.is Behavior)

(25)

验证结果为TRUE表示T_AP_Compute的行为符合系统模态的配置定义，否则存在故障。

6.5 验证结果分析

通过在AADL模型中插入10种故障类型，形成不同的AADL故障设计模型，并对其进行验证，均可以发现相应的故障，证明了本文方法的有效性。通过对飞行控制系统的验证结果进行分析，实验结果统计信息(包括故障说明、验证故障数目、验证故障总数、验证消耗时间和空间)如表2 所示。

表3展示了本文提出的基于NuSMV的AADL模型形式化验证方法与其他方法的对比结果，通过对比，本文方法主要具有以下3个方面的优势:

1) 考虑的AADL子集更丰富，包括构件、特征、连接、模态、数据流及行为附件等建模元素。

2) 采用图同构的方法保留AADL模型语义，以保证AADL模型到NuSMV模型转换的正确性、有效性和有限性。

3) 对AADL模型中的安全性、活性、模态配置的正确性进行验证，其中模态配置验证包括连接子元素、子构件及流元素的模态配置，以及系统层次化建模导致的模态嵌套正确性的验证。

7 结 论

本文覆盖了全部AADL软构件、系统和构件行为、模态配置和模态嵌套相关的建模要素，提出了一种基于NuSMV的AADL模型形式化验证方法，以验证AADL模型中安全性、活性和任务属性配置模态的正确性。由于NuSMV自身的缺陷，部分属性无法验证，比如模型精化属性、可调度性。所以本文与团队之前发表的文献[7]分别使用2种形式化方法对AADL模型进行验证，两种方法的侧重点不同，具有互补性。

表2 实验结果统计信息Table 2 Statistics of experimental results

表3 相关工作比较Table 3 Comparison of related works

续表3