机载系统的功能研制保证等级验证方法

蒋 泉，朱春玲，王旭亮，尹小花

(1.南京航空航天大学 航空宇航学院，江苏 南京 210016；2.空军装备部 项目中心，北京 100089；3.南京航空航天大学 计算机科学与技术学院，江苏 南京 211100)

0 引 言

机载系统在飞机的整个飞行任务中起着至关重要的作用，其失效会造成不可估量的后果。因此，保障机载系统的安全性已成为安全攸关领域的研究热点[1,2]。民用飞机领域采用研制保证过程来保证机载系统的安全性，即为机载系统及其组件正确地分配研制保证等级(development assurance level，DAL)，使飞机的研制以一种足够规范化的方式进行，从而将飞机研制过程中引入的差错控制在可接受的范围内，保证机载系统的安全性。

在机载系统的研制初期，ARP 4754A[3]提出了研制保证等级在系统级的概念，即功能研制保证等级(function development assurance level，FDAL)，其用于度量系统的功能在研制过程中的严格程度，使功能需求研制过程中的错误限制到安全性可接受的水平。ARP 4761[4]指出：在机载系统架构设计阶段，需要根据系统功能失效状态的严重程度来人为的对系统进行FDAL的正确分配[5]，以实施研制保证过程。

然而，由于现代机载系统具有功能繁多、架构复杂的特点，且不同系统之间存在不同层次、类型的依赖关系[2]，为研制保证过程中的FDAL的人为分配带来了挑战，难以保证人为分配的功能研制等级是合理的。例如，当今的民用飞机普遍使用综合模块化航电系统，使得机载系统的架构复杂，飞机上出现了大量的不同飞机功能的实现依赖相同组件的情况，为该组件分配FDAL时极易出现差错，难以保证其正确性，因为分配过程中不仅需要考虑依赖该组件的许多功能，同时还要考虑该组件依赖的其它组件实现的功能。同时，现代机载系统为进一步保证安全性，通常会采用分区、冗余和安全性监控等不同的架构设计，这些架构设计也会影响FDAL的分配，例如冗余架构设计的组件可以降低单一版本组件的功能研制保证等级。若机载系统的FDAL分配不合理，可能会导致机载系统在后期阶段中存在致命的安全性问题。因此，机载系统必须在架构设计阶段检验FDAL分配的合理性，即是否符合相关安全标准中的安全认证目标，保证机载系统的安全性。然而，ARP 4754A标准并未明确提及功能研制保证等级与安全认证目标一致性验证的技术和方法。

验证安全等级与标准的一致性方面存在一些相关工作。文献[6]从危害分析的角度进行了研究，但未给出一套完整的一致性检验的解决方案。文献[7]采用表格形式对系统静态结构的软件构件安全依赖的合法性进行表述；文献[8] 采用模型驱动和形式化方法，验证机载软件构件之间的安全性依赖关系是否符合DO-178C标准当中的安全认证目标。但文献[8]中归纳出的安全认证目标存在局限性，并未考虑不同架构设计对功能研制保证等级分配的影响，不适用于工程实际。

综上，为保证系统研制过程中的FDAL分配是符合安全标准，有必要提出一套自动、有效且考虑架构设计的验证方法，对分配给系统的功能研制保证等级与安全标准的一致性问题进行研究，从而保证系统安全性。

1 基于SysML的机载系统静态结构安全性建模

1.1 机载系统特征与SysML块定义图描述

机载系统具有以下特征[2]：

(1)高集成性。机载系统包含的组成单元数量多且类型繁杂，包括环境、人员、硬件、软件等不同类型的组成单元；

(2)复杂性。机载系统的组成单元之间及单元内部存在关联耦合等复杂的关系。

(3)多架构设计。机载系统是高安全的系统，为保证其安全性，通常会采用分区、冗余和安全性监控等不同的架构设计来降低系统失效产生的后果。

SysML系统建模语言中的块定义图(block definition diagram，BDD)[9]从系统结构角度描述了系统的结构组成单元以及组成单元之间的各种关系。针对以上特征，BDD能够表达机载系统不同类型的组成单元，BDD中块之间的关系(依赖、泛化、关联、组合、聚合等关系)能够表达机载系统组成单元之间的各种关系，BDD中块的属性具备表达机载系统自身的安全和架构设计信息的能力。

1.2 机载系统的静态结构安全性建模

本文利用BDD构建系统的静态结构模型，为了在构建的模型中描述所需的安全和架构设计信息，在BDD中定义5种属性，分别为SafetyCritical、FDAL_Level、Atomic、Redundancy、IsPrimary，前2个属性描述系统安全信息，后3个属性描述架构设计信息，架构设计仅考虑安全性监控、分区和冗余3种设计。

(1)SafetyCritical属性

构成系统的组成单元根据其对整个系统安全性的影响程度分为安全关键和非安全关键。若该组成单元的失效导致整个系统产生致命的安全问题，则该组成单元为安全关键的，其SafetyCritical值为true；否则为非安全关键的，其SafetyCritical值为false。对于安全性监控的架构设计，由于监测系统监控被监测系统中影响系统安全的事件，因此监测系统为安全关键的，其SafetyCritical为true。

(2)FDAL_Level属性

对于BDD中SafetyCritical=true的安全关键模块，为其分配功能研制保证等级，用属性FDAL_Level进行表示，取值为{A，B，C，D，E，null}，前5个等级是ARP 4754A标准给出的功能研制保证等级的划分，null针对非安全关键模块。

(3)Atomic属性

Atomic属性定义BDD中的模块是否拥有子模块。“true”表示模块没有子模块，“false” 表示模块具有子模块，即该模块是聚合、组合或泛化关系中的父模块。

(4)Redundancy属性

BDD中的聚合、组合和泛化关系能够体现分区或冗余的架构设计。若子模块之间采用分区或冗余的架构设计，则这些子模块的Redundancy属性值为true，否则为false。结合Redundancy和Atomic属性能够判断是否对某个模块进行分区或冗余架构设计情况下的功能研制保证等级安全验证。对于BDD中的任意模块对 (S1,S2)，若满足S1.Atomic=false∧S2.Redundancy=true，则S1和S2之间是聚合、组合或泛化关系(S1为父模块，S2为子模块)，并且S2为分区或冗余架构设计，因此需要对模块对 (S1,S2) 进行分区/冗余架构设计下的功能研制保证等级的验证。Redundancy值为other表明该模块在BDD中不属于任何模块的子模块。

(5)IsPrimary属性

该属性定义模块失效对其相关联模块失效的贡献程度。对于BDD中的模块对 (S1,S2)： ①若S1和S2之间是聚合、组合或泛化关系，若子模块S2的失效严重性与父模块S1失效后果保持一致，则S2为主要模块，其IsPrimary属性值为true；否则为次要模块，其IsPrimary属性值为false。②若S1和S2之间是依赖或关联关系，若被依赖(被关联)模块S2的失效后果严重性导致其依赖(关联)模块S1出现最严重的后果，则被依赖(被关联)模块S2为主要模块，其IsPrimary属性值为true，否则为次要模块，其IsPrimary属性值为false。③除了①中聚合、组合或泛化关系中的子模块和②中依赖或关联关系中的被依赖(被关联)模块，其余模块的IsPrimary属性值为other。

在构建带有上述5种属性的BDD过程中，SafetyCritical和Redundancy属性值根据模块代表的系统是否是安全关键和是否采用分区或冗余设计进行确定，FDAL_Level和Atomic属性值可以直接根据所分配的功能研制保证等级和模块在BDD中是否拥有子模块而快速确定。而IsPrimary属性值的确定需要遵循ARP 4754A的相关要求。

分析ARP 4754A中关于功能研制保证等级的要求，得出：①分区架构下，系统整体功能研制保证等级要与分区中系统部分最高功能研制保证等级相一致；②冗余架构下，可降低单一版本的功能研制保证等级，能够在保证系统整体安全性的同时，降低系统的研制成本；③安全性监控架构下，监测系统应与被监测系统的功能研制保证等级相一致。

以上要求使得IsPrimary属性值的确定需要遵循的原则为：①聚合、组合和泛化关系中，互为分区或冗余设计的所有子模块中至少存在一个主要模块，即至少存在一个IsPrimary为true的模块。②组合、聚合、泛化、关联和依赖关系中，对于采用安全性监控设计的架构，监测系统必为主要模块。

表1总结了SafetyCritical、Redundancy和IsPrimary属性值在不同架构下需遵循的约束。针对不同架构设计对FDAL_Level的约束，将在第2节中详细描述。对于系统之间的关系可以直接采用BDD块之间的关联、依赖、组合等关系进行表达。

表1 架构设计对属性值的约束

2 功能研制保证等级的安全认证目标

通过分析安全标准，并考虑不同架构设计会影响功能研制保证等级的分配，基于BDD中每个模块的SafetyCritical、Redundancy、IsPrimary属性值已满足表1约束的前提下，针对模块间不同的关系，给出功能研制保证等级的安全认证目标。

首先，BDD中的模块之间都必须满足一条总体的安全依赖约束：安全关键模块的功能实现不能依赖于非安全关键模块的功能，即为了确保安全关键模块功能的实现，在实现它的过程当中所依赖和使用的模块必须是安全关键的。具体而言，针对依赖(关联)关系，如果依赖方(关联方)S1是安全关键模块，则被依赖方(被关联方)S2也必须是安全关键模块；针对泛化、组合和聚合关系，如果父模块S1是安全关键模块，则子模块S2也必须是安全关键模块。该总体的安全依赖约束规约为规则R1：S1.SafetyCritical=true→S2.SafetyCritical=true。

对于非关键模块功能的实现依赖安全关键模块的情况，因该情况必然能保证非关键模块的安全性，因此不予考虑。下面给出的功能研制保证等级的安全认证目标仅针对两个模块都是安全关键的模块。

(1)模块之间的依赖(关联)关系

对BDD中的任意模块对 (S1,S2)，若满足S1.Atomic=true∨S2.Redundancy=other，则S1和S2之间是依赖或关联关系(其中S1为依赖/关联模块，S2为被依赖/被关联模块)。为保证依赖方(关联方)S1的安全性，被依赖方(被关联方)S2的功能研制保证等级必须大于或等于依赖方S1的功能研制保证等级，即满足规则R2：S1.SafetyCritical=true∧S2.SafetyCritical=true→S2.FDAL_Level≥S1.FDAL_Level。 由于BDD中的依赖或关联关系能够体现安全性监控的架构设计(分区设计的系统之间不存在直接的依赖或关联关系，冗余设计由聚合、组合和泛化关系体现)，所以该安全认证目标能保证作为关键模块的监测系统(被依赖方)的功能研制保证等级大于或等于被监测系统的功能研制保证等级，以确保监测系统正确实现监控功能。

(2)模块之间的聚合、组合、泛化关系

对BDD中的任意模块对 (S1,S2)，若满足S1.Atomic=false∧S2.Redundancy≠other，则S1和S2之间是聚合、组合或泛化关系(其中S1为父模块，S2为子模块)，该情况下存在的认证目标是：

1)若S2满足S2.IsPrimary=true，即S2是主要模块，其决定父模块整体的安全性，因此，子模块S2的功能研制保证等级必须大于或等于父模块S1的功能研制保证等级，即满足规则R3：S1.SafetyCritical=true∧S2.SafetyCritical=true∧S2.IsPrimary=true→S2.FDAL_Level≥S1.FDAL_Level。

2)若S2满足S2.IsPrimary=false∧S2.Redundancy=true，即S2是互为分区或冗余的模块中的次要模块。虽然分区或冗余的架构设计允许降低单一版本系统的功能研制保证等级，即次要模块的功能研制保证等级无需与其父模块的功能研制保证等级相一致，但其必须满足最低允许值，分为2种情况：①若父模块S1的功能研制保证等级为A，则其次要模块S2的功能研制保证等级必须大于或等于C，即该情况下的安全认证目标为规则R4_1：S1.SafetyCritical=true∧S2.SafetyCritical=true∧S1.FDAL_Level=A∧S2.IsPrimary=false∧S2.Redundancy=true→S2.FDAL_Level≥C。 ②若父模块S1的功能研制保证等级为B，则其次要模块S2的功能研制保证等级必须大于或等于D，即该情况下的安全认证目标为规则R4_2：S1.SafetyCritical=true∧S2.SafetyCritical=true∧S1.FDAL_Level=B∧S2.IsPrimary=false∧S2.Redundancy=true→S2.FDAL_Level≥D。

综上所述，规则R1是总体的安全依赖约束，其排除安全关键模块和非安全关键模块之间的非法关系；规则R2排除安全关键模块之间的非法依赖和关联关系，验证的是安全性监控架构设计下的功能研制保证等级分配的合理性；规则R3、R4_1和R4_2排除安全关键模块之间的非法聚合、组合和泛化关系，验证的是安全性监控、分区和冗余架构设计下的功能研制保证等级分配的合理性。

3 功能研制保证等级一致性验证

为了能基于BDD做自动高效的一致性验证，需要将其转化为形式化模型[10,11]。本文采用块依赖图(block dependency graph，BDG)[12]作为BDD的形式化模型，并基于此模型给出一致性验证方法。

3.1 基于BDG的SysML块定义图的形式化描述

若M为一个BDD，其对应的块依赖图(BDG)M′为一个二元组，记为：M′=[NB,EB]，其中：

NB表示结点集合，集合中的每个结点代表BDD中的一个块，即M′中的每个结点代表M中的一个块。此外，每个结点带有标记L，是结点代表的块当中的属性构成的集合。结点上的属性SafetyCritical、FDAL_Level、Atomic、Redundancy和IsPrimary分别用p1、p2、p3、p4和p5表示，记v(p1)、v(p2)、v(p3)、v(p4)和v(p5) 为相应属性值；

EB是边集合，EB⊆NB×NB。 对于任意的 (x,y)∈EB，若x≠y，则有 (x,y)≠(y,x)，即块依赖图中的边均是有向的。 (x,y) 的含义是结点x与结点y存在关系，即 (x,y)∈R，R={依赖，关联，泛化，聚合，组合}。 例如： (x,y)={依赖}，则x为依赖模块，y为被依赖模块；(y,x)={依赖}，则y为依赖模块，x为被依赖模块。

对于块依赖图M′1=，如果有块依赖图M′2=，其中N′B⊆NB，E′B⊆EB，则称M′2是M′1的子图。

BDD转换成BDG时，首先将BDD中的每个块转化为BDG中相应的结点，块中的属性构成BDG中相应结点的标记L。其次将BDD中块之间的关系转化为BDG结点之间的有向边，即BDD中的依赖关系转化为BDG中依赖方到被依赖方的有向边；关联关系同依赖关系类似。组合关系转化为BDG中父模块的结点到子模块结点的有向边；泛化和聚合关系同泛化关系类似。

3.2 安全认证目标一致性验证方法

将BDD转换为BDG之后，需要基于BDG来验证是否满足认证目标。将BDG中不满足认证目标的模块之间的关系称为非法关系，具体存在两种情况：安全关键模块与非安全关键模块之间的非法关系、安全关键模块之间的非法关系。

一致性验证的方法是对BDG进行遍历，首先基于结点标记的属性值判断结点对 (Si,Sj) 之间存在何种关系，然后依据不同的关系对结点对 (Si,Sj) 进行相应关系下的认证目标的验证。若不满足相应关系下的认证目标，则结点Si和Sj之间存在非法关系。算法1给出了一个基于图的深度优先搜索的检验方法，算法的输入是块定义图M转化得到的块依赖图M′=，其中M的SafetyCritical、Redundancy和IsPrimary属性满足表1的约束，输出为非法关系集合Eillegal。主要算法思想如下：

(1)(7)行-(19)行判断BDG中是否存在安全关键结点到非安全关键结点的非法关系，即验证规则R1。通过遍历BDG中的结点，根据结点SafetyCritical属性的值为false(即第(9)行的Si.v(p1)=false)，识别所有的非安全关键结点并加入到集合unSafetyNode中；然后根据BDG中的有向边判断unSafetyNode集合中每个结点的前驱结点是否为安全关键结点，若是(即第(14)行的Sj.v(p1)=true)，则这两个结点之间存在非法关系，将其加入到集合Eillegal。

(2)(20)行-(42)行判断BDG中安全关键结点之间的非法关系。第(20)行在BDG中删除unSafetyNode集合中所有的非安全关键结点和以这些结点为起点和终点的所有边，剩余结点和有向边构成BDG的子图(subM’)；(21)行-(42)行对subM’中每一对结点对依据不同关系进行非法关系识别。首先获取subM’中的每一个结点的所有后继结点，然后依据当前结点及其每一个后继结点的属性标记值判断结点对之间的关系，从而依据不同关系进行相应认证目标的验证。具体判断情况如下：

1)(26)行-(35)行是组合、聚合或泛化关系下对认证目标R3，R4_1和R4_2的验证。对于任意结点对 (Si,Sj)，首先根据后继结点Sj的属性Redundancy的值不等于other以及当前结点Si的属性Atomic的值等于false确定Si与Sj为聚合/组合/泛化关系(即满足第(26)行的判断条件)。然后根据Sj的属性IsPrimary的值进行不同情况下认证目标的验证。若Sj为主要模块，则(28)行、(29)行进行规则R3的验证。若Sj的功能研制保证等级小于父模块Si的功能研制保证等级(即满足第(28)行的条件)，则为非法关系，不满足R3，将结点对之间的边加入到集合Eillegal中。同理，(31)行-(35)行针对Sj为次要模块的情况，(31)行、(32)行与(34)行、(35)行分别在Si的功能研制保证等级为A和B的情况下对次要模块Sj进行相应规则R4_1和R4_2的验证。若Si的功能研制保证等级为A，而次要模块Sj的功能研制保证等级小于C(即满足第(31)行的条件)，则为非法关系，不满足R4_1，将结点对之间的边加入到集合Eillegal中。若Si的功能研制保证等级为B，而次要模块Sj的功能研制保证等级小于D (即满足第(34)行的条件)，则为非法关系，不满足R4_2，将结点对之间的边加入到集合Eillegal中。

2)(37)行-(39)行是依赖或关联关系(即满足第(37)行的条件)下对认证目标R2的验证。若被依赖方(被关联方)Sj的功能研制保证等级小于依赖方(关联方)的功能研制保证等级(即满足第(38)行的条件)，则为非法关系，不满足R2，将结点对之间的边加入到集合Eillegal中。重复以上过程，直至subM’中的每个结点的所有后继结点都已经被遍历。

通过以上(1)、(2)的判断过程，可以得出BDG中所有模块之间的功能研制保证等级之间的非法关系。然后根据BDG中的结点与BDD中模块之间对应关系，将Eillegal中的非法关系映射到BDD中，得到功能研制保证等级分配不合理的系统组成单元，指导系统的安全设计模型的修改，确保系统安全。

算法1： 功能研制保证等级的非法关系判断

输入： BDDM转化得到的BDGM’

输出：M’中的非法关系集合Eillegal

(1)functionIllegalDependenceJudgment(NB,EB)

(2) unSafetyNode：=φ; Eillegal：=φ; PrecursorNodeSet:=φ;

//定义的集合分别为：非安全关键结点集合、非法关系集合、后继结点集合

(3) Precursor(Si):=Get precursor nodes ofSi; //获取结点的前驱结点

(4) Successor(Si):=Get successor nodes ofSi; //获取结点的后继结点

(5) GetEdge(Si,Sj):=Get edge betweenSiandSj; //获取结点对之间的边

(6)----验证安全关键与非安全关键结点是否满足规则R1----

(7) repeat

(8) nodeSi:=unvisited node ofM’;

(9) ifSi.v(p1)=false then //识别非安全关键结点

(10) unSafetyNode ← unSafetyNode∪{Si};

(11) PrecursorNodeSet ∶= Precursor(Si);

(12) repeat

(13) nodeSj∶=unvisited node of PrecursorNodeSet;

(14) ifSj.v(p1)=true then //识别安全关键结点

(15) Eillegal←Eillegal∪{GetEdge(Si,Sj)}; //不满足关系R1

(16) end if

(17) until all nodes in PrecursorNodeSet are visited

(18) end if

(19) until all nodes inM’ are visited

(20) Remove all nodes in unSafetyNode and related edges with deleted nodes fromM’, then construct the subgraph(subM’);

//获取子图subM’

(21) repeat

(22) nodeSi∶=unvisited node of subM’;

(23) repeat

(24) nodeSj∶=unvisited node in Successor(Si) //依据当前结点Si的属性与其后继结点Sj的属性判断两个结点之间的关系

(25)------------------聚合/组合/泛化关系下验证安全关键结点之间是否满足规则R3，R4_1和R4_2------------------

(26) ifSj.v(p4) !=other∧Si.v(p3) = false then // 首先判断Si和Sj是聚合/组合/泛化关系

(27)--------验证安全关键结点之间是否满足规则R3--------

(28) ifSj.v(p5)=true∧Sj.v(p2)

(29) Eillegal←Eillegal∪{GetEdge(Si,Sj)}; //不满足关系R3

(30)--------验证安全关键结点之间是否满足规则R4_1------

(31) else ifSj.v(p4)=true∧Sj.v(p5)=false∧Si.v(p2)=A∧Sj.v(p2)

(32) Eillegal←Eillegal∪{GetEdge(Si,Sj)}; //不满足关系R4_1

(33)--------验证安全关键结点之间是否满足规则R4_2--------

(34) elseSj.v(p4)=true∧Sj.v(p5) = false∧Si.v(p2)=B∧Sj.v(p2)

(35) Eillegal←Eillegal∪{GetEdge(Si,Sj)}; //不满足关系R4_2

(36)-----------依赖/关联关系下验证安全关键结点之间是否满足规则R2-----------

(37)ifSj.v(p4)=other ∧Si.v(p3)=true then //Si和Sj为依赖/关联关系

(38) ifSj.v(p2)

//被依赖模块(被关联方)Sj的功能研制保证等级小于依赖方(关联方)Si的功能研制保证等级

(39) Eillegal←Eillegal∪{GetEdge(Si,Sj)}; //不满足关系R2

(40) until all nodes in Successor(Si) are visited

(41)until all nodes of subM’ are visited

(42) return Eillegal

(43) end function

4 实例分析

飞机自动驾驶仪(autopilot system，AP)是典型的机载系统，在其体系架构设计阶段，验证其功能研制保证等级的分配是否与认证目标一致，有助于确保系统研制可以按照一种规范的方式完成，将研制过程中产生的错误，限制到安全性可接受的水平，从而提高系统的安全性。下面详细阐述本文方法的应用过程。

4.1 构建机载系统的静态结构安全性模型

AP是一种能够代替驾驶员控制飞机运动状态的自动控制装置。在构建AP系统的静态结构安全性模型的过程中，SafetyCritical和Redundancy属性值的确定可以根据BDD模块代表的系统是否是安全关键和是否采用分区或冗余设计进行确定，FDAL_Level和Atomic属性的值可以直接根据所分配的功能研制保证等级和模块是否拥有子模块而快速确定，IsPrimary属性值根据表1确定。图1给出了飞机自动驾驶仪系统带有安全信息和架构设计信息的SysML BDD图，相关子系统各属性值的确定过程如下：

(1)确定FDAL_Level、Redundancy和IsPrimary属性值

AP系统和自动油门(AT system)是自动飞行系统的核心部分，其设计需求的功能研制保证等级要求较高，AP系统为B级，AT为C级。为确保安全，对AP系统采用安全性监控设计，提供监测子系统(AP monitor)对AP运行状态进行监测，其等级为C。由于AP monitor是监测系统，因此其IsPrimary值为true。完成自动飞行任务需要导航系统(navigation system)引导飞行，由于导航系统需要同时为多用户提供关键信息，因此其采用功能冗余的架构设计，通过惯性导航系统(INS)和航姿参考系统(AHRS)为飞机收集姿态等信息，等级分别为B和C，其Redundancy值均为ture。由于大多数组合导航系统以INS为主，因此INS系统的IsPrimary值为true，AHRS的IsPrimary值为false。导航系统根据INS和AHRS提供的信息进行转发和判断，其等级为B，IsPrimary值为true。为保证系统安全交互，AP系统通过公共接口(Interface)接收导航系统处理的信息，其等级为B。监控器(Interface Monitor)监控接口中影响系统安全的事件，其等级为B，由于其也是监测系统，因此其IsPrimary值为true。Interface Monitor一旦监控到不安全的事件，事件处理子系统(EventHandler)将会采取安全措施降低或消除产生的危害。功能控制增稳系统(CAS)既能提高飞机稳定性又能改善飞机操纵系统，其等级为A。紧急断开系统(ForceExit)为飞行员提供紧急情况下快速断开AP工作的功能，其等级为C，由于其失效将导致AP系统出现严重的后果，因此其IsPrimary为true。AP1和AP2是AP下互为备份的控制器，等级均为B，Redundancy值均为true，IsPrimary值也为true。AP控制器由计算功能模块(compute function)嵌入到飞行控制计算机(control computer)构成，通过计算飞机当前飞行状态参数并控制执行元件执行驾驶员的命令，其等级分别为B和C，IsPrimary值均为true。

(2)确定SafetyCritical属性值

除EventHandler子系统外[8]，其余系统均为安全关键系统，因此BDD中对应模块的SafetyCritical值为true。

(3)确定Atomic属性值

Navigation system、AP system和AP2系统均有子模块，因而其Atomic值为false，其余模块的Atomic值为true。

图1 自动驾驶仪系统及其辅助系统的BDD

4.2 构建块依赖图

根据3.1节的BDD到BDG的转换方法，得出如图2所示的BDG，结点上的标记信息如图2中右边列表所示。具体转换过程如下：

(1)将BDD中的每个块转换为对应的BDG中的结点，模块具有的属性转换为BDG中结点的标记L，即模块属性SafetyCritical、FDAL_Level、Atomic、Redundancy和IsPrimary分别转换为标记L中的v(p1)、v(p2)、v(p3)、v(p4) 和v(p5)。

(2)其次将BDD中块之间的关系转换为BDG中相应结点之间的有向边，即BDD中的依赖/关联关系转化为BDG中依赖方到被依赖方的有向边，例如AP system与ForceExit之间的依赖关系转换为图2中结点S5到结点S7的有向边；组合/聚合/泛化关系转化为BDG中父模块的结点到子模块结点的有向边，例如Navigation system与子模块INS和AHRS之间的聚合关系转换为图2中结点S3到结点S1和结点S2的有向边。

图2 块依赖图的构建

4.3 安全认证目标一致性验证

依据3.2节中给出的算法1，以图2中的块依赖图为输入，功能研制保证等级的认证目标一致性验证过程如下：

(1)对块依赖图进行深度优先遍历，根据属性SafetyCritical的值为false，识别所有非安全关键结点并加入集合unSafetyNode，在该实例中，只有S15为非安全关键结点，满足算法1中伪代码第(9)行，因此unSafetyNode={S15}。

(2)对unSafetyNode中每个非安全关键结点Si进行规则R1的验证。首先获取Si结点的所有前驱结点Sj，若Sj的SafetyCritical的属性值为true，即存在一条非法关系，将该非法关系加入集合Eillegal。该实例中，由于结点S15不存在前驱结点，不满足算法1中伪代码第(14)行，因此不存在安全关键结点到非安全关键结点的非法关系。

(3)在BDG中删除unSafetyNode中所有的非安全关键结点以及与该类结点关联的所有边，剩余结点和有向边构成子图(该子图与图2相比，仅不存在S15结点)。

(4)对子图中的每一个结点，获取其所有的后继结点，然后依据当前结点及其每一个后继结点的属性标记值判断结点对之间的关系，从而依据不同关系进行相应认证目标的验证，即检验安全关键结点之间是否存在非法关系。例如，对于结点S3，其所有后继结点集合为 {S1,S2}，需要对结点对 (S3,S1) 和 (S3,S2) 进行相应规则的验证，此处以 (S3,S1) 为例。根据结点属性，满足算法1中伪代码第(26)行，判定 (S3,S1) 之间为聚合/组合/泛化关系，因此依次验证规则R3、R4_1和R4_2。又如结点对 (S5,S7) 满足算法1中伪代码第(37)行，判定 (S5,S7) 之间为依赖/关联关系，因此需要验证规则R2。在子图中，所有具有聚合、组合和泛化关系的结点对的集合是 {(S3,S1),(S3,S2),(S5,S8),(S5,S9),(S9,S11),(S9,S12)}，对集合中的每对元素进行规则R3，R4_1和R4_2的验证；所有具有依赖和关联关系的结点对的集合是 {(S4,S3),(S13,S4),(S5,S4),(S14,S4),(S5,S6),(S5,S7),(S5,S10)}，对集合中的每对元素进行规则R2的验证。最后，得到非法关系集合Eillegal={(S9,S11),(S5,S7),(S5,S10)}。

4.4 一致性验证结果分析

将Eillegal中非法关系映射成BDD中相应关系。对于非法关系(S5,S7)，在BDD中分别为AP system和ForceExit。由于AP system依赖ForceExit，为保证AP system的安全性，要求ForceExit的FDAL大于或等于AP system的FDAL。但在该设计中，ForceExit的FDAL低于后者，因此不满足规则R2。解决方案是提高ForceExit的FDAL。在实际的项目开发中，AP设计早期阶段没有重视ForceExit，后期在试飞过程中，发现强制退出功能经常出现故障，严重影响飞机的安全性。

对于非法关系(S5,S10)，在BDD中分别为AP system和AP monitor。AP system采用安全性监控，该依赖边不满足规则R2，可见AP monitor的FDAL分配不合理。

对于非法关系(S9,S11)，在BDD中分别为AP2和control computer，由于S11所代表的块是S9的主要模块，所以其FDAL应该大于或等于S9的FDAL，不满足规则R3，因此S9所代表的系统的安全性无法得到保障，因而该系统的FDAL分配不合理。

5 结束语

本文从系统静态结构的角度，通过分析相关安全标准和不同架构设计得出功能研制保证等级之间的安全认证目标，提出了一种系统功能研制保证等级的验证方法。利用SysML构建系统静态结构安全性设计模型，并通过将其转换为形式化模型块依赖图实现FDAL分配是否符合相关安全标准中的认证目标的自动验证。通过对案例的分析，得出结论：该方法通过验证系统功能研制保证等级与安全认证目标的一致性，能够分析出FDAL分配不合理的模块，提高系统安全性。