一个基于形式化方法的系统安全性建模分析实例研究

石梦烨，胡 军，陈 朔，唐红英，王立松

(南京航空航天大学 计算机科学与技术学院，南京 211106)(软件新技术与产业化协同创新中心，南京 211106)

1 引 言

近年来，随着各类安全关键系统[1，2]功能的不断增强和需求的日益增加，对传统的系统工程开发和安全性分析技术提出了很大的挑战.基于模型的安全性分析[3，4](Model Based Safety Analysis，MBSA)是近年出现的一类对复杂系统建模并基于系统模型实现自动或半自动化的安全分析及验证的技术方法.MBSA已成为系统建模和分析领域的一个热点研究问题.

MBSA方法是形式化方法在安全关键系统的应用，旨在系统复杂性上升的同时保持或提高其安全性水平.它用于支持系统设计层级的分析，包括三个关键要素[5]：

1)对整个系统进行形式化模型的构建，其中模型是组件的集合；

2)对模型进行定性和定量分析，将可能存在的安全问题设置成一系列故障模式；

3)对扩展模型进行形式化安全分析.

国际汽车工程师协会(Society of Automotive Engineers，SAE)架构分析与设计语言(Architecture Analysis and Design Language，AADL)[6，7]是一种形式化建模语言，通过可扩展的标记符、工具框架和精确的语法语义，用于设计和分析复杂系统的软件和硬件架构及其性能关键特性.

本文主要工作以AADL的子集SLIM为建模语言，基于xSAP(The eXtended Safety Assessment Platform)为安全性分析平台的形式化验证方法[8]，以AIR6110中的机轮刹车系统[9]为实例，对其进行安全性建模和分析.通过一个实例展现了面向SLIM模型进行安全性分析和形式化验证的过程.本文的结构安排如下：第二节，主要介绍了MBSA框架、形式化方法在MBSA的应用、建模语言SLIM，和验证工具NuSMV[10，11]；第三节，简要介绍了AIR6110标准和机轮刹车系统，并详细给出了用SLIM对其进行形式化建模的过程以及建模时遇到的问题，设计了多种类的故障模式并进行模型扩展；第四节对建立的机轮刹车模型进行分析并展现了验证结果；最后总结全文.

2 基于形式化方法的安全性分析方法架构

2.1 MBSA框架

MBSA方法学是一种系统设计工程师和安全工程师共享使用基于模型的开发过程创建的公共系统模型的方法[12].如图1所示，在设计阶段通过形式化语言描述复杂系统的行为架构，来构造一个通用的需求模型；在安全性分析阶段中基于所建立的系统模型来进行失效行为的语义扩展，并尽可能的自动化生成系统失效行为的最小割集故障树[13]和失效序列.

图1 MBSA方法框架Fig.1 MBSA method framework

总体上来看，MBSA的总目标是：1)提供一个可公用且严格定义的系统模型，确保随着系统架构的发展，安全分析结果是最新的；2)通过将传统的安全分析过程与基于模型的开发活动相结合，允许开发早期可以进行安全评估，降低因系统复杂度提高造成的成本增加并提高安全分析过程的质量；3)系统开发工程师和系统安全工程师可以通过公用的形式化模型进行沟通，便于对系统的理解.

2.2 MBSA中的形式化方法

形式化方法[5，14]是将数理和逻辑方法(如逻辑、自动机、图论)运用在计算机工程领域，通过借助形式化语言，去构建计算机系统的数学模型并进行模型推理和验证.它的应用领域是多方面的：首先使用形式化语言去描述符合语法语义规则的完整的系统模型；其次使用形式化分析技术和形式化工具分析系统模型；最后，形式化方法渗透在系统开发过程的各个阶段，包括需求分析、设计、实现.它可以用来引导安全关键系统的开发过程，尽早发现每个阶段的缺陷问题.

在系统的开发过程中，采用具有严格语法语义定义的形式化建模语言可以建立精确且公用的数学模型.在安全评估过程中，采用形式化分析技术可以对公用的系统模型的扩展形式进行分析和验证，来发现模型中可能存在的安全问题.采用形式化工具可以自动化验证过程，减少人工检查的高成本并减少错误.因此形式化方法在MBSA方法中极为重要[15，16].

MBSA的起点和重点是创建公用的需求模型.在本文工作中选用的是系统级集成建模语言(System-Level Integrated Modeling language，SLIM)对系统进行需求规约.SLIM是AADL的精化，一个完整的SLIM系统规范由三部分组成，即正常行为的描述、错误行为的描述以及描述错误行为如何影响正常行为的故障注入规范.NuSMV(New Symbolic Model Verifier)是一个符号模型检验工具，支持先进的模型检验技术[17]，基于BDD(Binary Decision Diagrams)和SAT(Satisfiability)针对CTL(Computation Tree Logic)[10]和LTL(Linear Temporal Logic)[18]时态逻辑进行验证，可用于对SLIM建立的需求模型进行分析.

3 AIR6110标准中的机轮刹车系统的实例建模研究

3.1 AIR6110标准和WBS概述

在本文的工作中，选择了在SAE的AIR6110标准中所给出的一个典型的安全关键系统实例展开研究，这是一个航空领域中的飞机机轮刹车系统的系统规范和安全性分析实例.AIR6110文件由SAE于2011年发布，SAE AIR6110的全称是“连续飞机/系统开发过程示例”，其中机轮刹车系统(WBS)的开发和安全性分析完全遵循工业标准ARP4754A—“民用飞机和系统发展指南”[19]和ARP47611—“进行民用机载系统和设备安全评估程序的指南和方法”[20]中的要求.ARP4754和ARP4761是目前航空电子领域的开发和安全评估过程的工业标准.

图2 机轮刹车系统模型概观Fig.2 Overview of the wheel brake system model

在AIR6110所给出的这个实例系统中，主要描述了WBS的系统框架结构和功能要求，其中，WBS由制动系统控制单元(Brake System Control System，BSCU)和液压调节系统组成.图2是机轮刹车系统的模型概观.

BSCU是系统中的数据处理组件，收集来自踏板、机轮速度等信息作为输入，使用内部的命令单元进行计算并向液压调节系统输出不同命令：传输到液压调节系统正常线路的控制命令，传输到液压调节系统备用线路的控制命令，对关闭阀和选择阀进行调控的开关命令.BSCU还包含监控单元，主要用于监控命令单元的状态.默认情况下，BSCU使用第一组命令和监控设备.当监控设备发出错误警报，则由选择设备自动切换成备用组.

液压调节系统用于对机轮进行供压，分为正常线路和备用线路.正常线路包括绿色液压泵、关闭阀、限量阀；备用线路包括蓝色液压泵、隔离阀、蓄压泵、防滑阀、人工刹车装置.正常线路由绿色液压泵供压，备用线路处于待机状态，由蓝色液压泵供压.当蓝色液压泵失效时，由用于驱动刹车制动器的蓄压泵支持.选择阀为两条线路共有，起线路切换功能.当正常线路失效，则转换至备用线路.若备用线路也失效，则由人工刹车装置额外提供液压.

3.2 WBS的形式化建模

上一节用自然语言概要描述了AIR6110标准中的WBS系统架构和功能，接下来在本节中将采用SLIM对WBS系统的功能进行形式化建模.本文将机轮刹车系统按表1所示分层结构建模.

表1 WBS分层模型整体框架图
Table 1 Overall framework of WBS hierarchical model

模型层级系统包含的子组件BSCU子系统第一层WBS液压调节系统监控器lru1、第二层BSCU子系统lru2、选择设备绿色液压泵、蓝色液压泵、第二层液压调节系统关闭阀、蓄压泵、隔离阀、选择阀、限量阀、防滑阀、人工刹车装置第三层LRU监控单元命令单元

给出液压调节系统的选择阀的SLIM描述如图3所示，其他部件可以通过类似方法得到其对应的SLIM代码模块，在此不再赘述.

首先设置端口，选择阀的输入端口有来自蓄压泵的液压accumulator_input，来自正常线路的液压green_input，来自备用线路的液压blue_input，来自monitor的事件switch，以及来自BSCU的select_alternate.输出端口有green_out，blue_out.其中，accumulator_input、green_input和blue_input的数据类型是intRange，范围是[0…10]，初始值为5，select_alternate是布尔型端口，初始值为false.

共设置四种模式：select_green、select_blue、select_accu、fail，初始模式是select_green.图3设置了7种转换.

第1个转换说明，如果收到的数据端口绿色液压值大于等于5，则说明使用正常线路，那么令液压值等于输入的绿色液压值.

图3 选择阀建模代码
Fig.3 Selector modeling

第2、3、4这三个转换说明如果收到的绿色液压值green_input小于5，则选择备用线路；收到switch事件，则系统从select_green转变为select_blue，即选择备用线路；当选择阀收到来自BSCU的select_alterate值为true，即表示当前正常线路出现了问题，则使用备用线路，令选择阀的输出液压值为蓝色液压值.

第5、6、7这三个转换说明，如果收到的来自蓝色液压泵的液压值≥5，则使用备用线路，并令选择阀的输出液压值为蓝色液压值；若收到的蓝色液压值<5，而蓄压泵的液压值≥5，则使用蓄压泵的液压值；当蓄压泵的液压值也小于5，说明蓄压泵也出现问题，则失败.

在面对AIR6110标准建模的过程中，我们发现了一些在AIR6110标准文档中尚未清楚阐述的地方，如：在标准的文字描述中给出“正常线路的液压值会作为反馈传输到BSCU中.当该反馈值小于指定的值时，就类似于一个指示信号，指示正常线路失效.这种情况下，BSCU会产生一个命令，将关闭阀关闭.”并未说明BSCU的命令如何传到该阀？此外，AIR6110标准中的Arch4架构显示，监控单元有一根连着关闭阀的线，它是否可以用来控制阀门?

由此可见，自然语言存在无法阐述清楚系统需求或者存在二义性问题.而形式化方法是基于形式化语言的，具有非常精确的语义，因此可以明确地解释系统出现的问题.在进行形式化建模的时候，新的系统除去了由液压调节系统指向BSCU的液压反馈值.建模时，在BSCU系统中单独建了一个select系统，它接受来自于监控单元的数据，用于判断是否使用备用液压，它的输出select_alternate会传到关闭阀中.如果select_alternate为true，则说明当前正常线路出现了问题，那么则关闭关闭阀.

另外，在标准文字表达中出现：“防滑阀也能对液压进行调整”，实际系统中如何体现对液压的修改？

由于标准中记载的防滑阀和限量阀的功能是：“防滑阀遵循BSCU传出的命令去控制制动器的液压，它用于限制制动器的液压管路压力以防止机轮锁定.”以及“当飞行员或自动刹车系统测量到压力超过滑行轮胎所需的压力时，通过降低制动压力来优化制动.限量阀根据BSCU传来的控制命令，对液压调节系统的液压值进行调节，并把调节后的值传输到机轮.”也就是说，防滑阀和限量阀的主要功能是降低制动压力.所以，在使用SLIM进行建模的时候，设置它们的压力变化为不变和下降.相应的，BSCU产生的命令为down和nochange.

3.3 用xSAP对WBS模型故障扩展

由于上一节中建立的模型是假设系统在理想情况下运行.而实际情况下，安全分析需要考虑到可能发生的不同故障以及系统组件可能出现故障的各种方式，因此必须使用系统的故障行为来增强基于模型的开发中捕获的正常系统行为.xSAP支持基于库的故障模式定义，可以对正常的系统功能行为进行模型扩展，扩展后的模型通过安全性分析来评估存在故障的系统行为.

3.3.1 故障设置

在此以液压调节系统中的阀类为例设计故障.对关闭阀设置了三种不同的状态：OK，Dead，Stuck_at_zero.OK表示初始状态，Dead是失效状态，失效的原因来自于内部软件错误事件internal_error.Stuck_at_zero是卡死状态，当出现错误事件stuck_at_zero时，pump会从OK变成Stuck_at_zero.这种情况下，无论输入的液压值是多少，输出的液压值都为0.

具体实现中，设置两个故障事件，internal_error和stuck_at_zero.internal_error是液压错误事件，stuck_at_zero是卡死故障，表示卡死在液压值0.接下来定义转换，分别定义了以下转换：

1)OK-[Internal_error]->Dead；

2)OK-[stuck_at_zero]->Stuck_at_zero.

系统初始时处于OK状态，当遇到故障事件internal_error，会从OK转为Dead.当遇到卡死事件stuck_at_zero，会从OK转为Stuck_at_zero.

3.3.2 故障扩展

上一节中所设计的系统故障行为是从安全性分析的视角来进行设计的，还需要进一步将这些可能的故障信息与正常的系统功能行为合并在同一个模型中进行完整的系统分析.这种合并是通过在模型层的故障注入方式来实现的.

故障注入描述了错误发生对系统正常行为的影响.更具体地说，它指定当关联的错误模型进入特定错误状态时组件实现中的数据元素经历的值更新.

在本实例的研究中使用xSAP对模型进行扩展，选择三个故障注入，分别是:1)电源2发生故障；2)主模式BSCU系统中的监控单元出现错误；3)液压调节系统中的绿色液压泵发生错误.

4 机轮刹车模型的安全性分析

形式化分析工具可以用来对建立的模型进行安全性分析.以xSAP为核心的COMPASS(Correctness，Modeling，and Performance of Aerospace Systems)分析[21，22]包括对系统进行形式化建模，即建立SLIM模型；对系统进行定性分析并设计安全属性；考虑系统可能存在的失效行为并进行语义扩展和分析.COMPASS的输入为根据系统架构建立的正常模型和设置的故障模式，以及一组表示系统规约的属性.输出为反例路径、故障树、FMEA表[5，23]、FDIR[24]等可视化界面.

4.1 模型的动态仿真

模型模拟主要用于检查系统功能的正确性.图4是模型的部分运行图形，在此选择运行的步长为20.轨迹由一个表格组成，其中第一列提供了模型元素的名称，在其他列中显示了该元素在每个步骤的值.布尔条纹显示为具有两个值的波形，其中high为true，low为false.

图4 对扩展的WBS系统进行动态仿真Fig.4 Dynamic simulation of extended WBS systems

通过图4中的模拟结果可以发现，由于主模式的监控单元发生了invalidReport错误，导致判断监控单元是否有效的输出valid的值为false，该故障作为故障传播进入BSCU中的select_Alternate.监控器收到来自BSCU中监控器的错误，引发switch事件，switchBSCU和alarmBSCU变为true，switch事件传入BSCU，导致BSCU系统从Primary转为Backup.

4.2 模型检测

模型检测用于根据一个或多个属性检查SLIM模型.通过将指定的属性描述为时态逻辑公式并使用特定的符号算法进行状态空间的智能搜索来确定属性是真是假.若属性为假，则生成反例轨迹以显示违反该属性的模型的执行轨迹来进行深入的进一步分析.否则，显示属性正确.共设计并验证了15条属性，其中6条正确，9条错误，耗时8.36秒.

图5 模型检查得到错误属性的反例Fig.5 Model check gets a counterexample of the wrong attribute

在此选取其中两个进行说明.首先对属性“AG(valid=false and bscu.mode=mode：Backup-> AF alarmBSCU)has been found false.”进行验证，该属性的含义为：无论何时原子命题“valid=false and bscu.mode=mode：Backup”成立，它最终一定会被响应alarmBSCU.如图5所示，结果显示该CTL属性错误并给出反例路径.

接下来对CTL属性“AG(bscu.mode=mode：Backup and bscu.valid=false-> EF alarmBSCU)has been found true”进行检查，它的含义是当BSCU当前的模式是Backup，并且valid值为false，则表明BSCU系统已经是失效，可能会响应警报alarmBSCU.在模型中，该CTL属性成立.

4.3 形式化模型的安全性分析

经典的系统安全性分析方法有故障树分析(Fault Tree Analysis，FTA)和故障模式和影响分析(Fault Mode and Effect Analysis，FMEA).FTA是一种自顶向下的方法，它通过考虑所分析系统的意外行为，自上而下分析追踪直到找出所有故障模式.FMEA则是一种自底向上的方法，它通过考虑给定的危害的起因，分析其可能的安全后果.

4.3.1 故障树分析

在此选择属性“bscu fail twice”作为顶层故障事件(Top Level Event，TLE)进行故障树分析的说明，它的不定式是“bscu.valid=false and bscu.mode=Backup”，含义是当前BSCU子系统处于备用模式且输出端口valid的值为false，即两个监控命令单元都失效.这种情况下，说明整个BSCU子系统已经失效.使用COMPASS中生成故障树的功能，生成对应的故障树.故障树显示如何达到与TLE相对应的状态，即通过AND和OR门连接可能导致TLE的基本事件序列(故障).

通过运行故障树，顶层事件“bscu fail twice”得到两个文件：wbs_000001.flt_events和wbs_000001.flt_gates.其中wbs_000001.flt_events包含三个基本事件，分别是：

1)E2：bscu.lru1.mon._errorSubcomponent.#invalidReport

它表示BSCU子系统的lru1子系统的监控单元发生了invalidReport故障.

2)E5：power._errorSubcomponent.#close

它表示电源组件发生了close故障.

3)E6：power._errorSubcomponent.#depleted

它表示电源组件发生了deplted故障.

图6 “bscu fail twice”的故障树Fig.6 Fault tree of “bscu fail twice”

图6是导致顶层事件“bscu fail twice”发生的故障树.如图所示，在这个故障树中有两个分支引起故障：一个分支是E2和E5，它们通过与门连接，一起导致事件fault_cfg_1的发生；另一个分支是E2和E6，也通过与门连接，导致事件fault_cfg_2的发生.该故障树的逻辑公式表示为：(E2∧E5)∨(E2∧E6).

故障树的最小割集(Minimum cutset，MCS)[25]是导致TLE发生的组件故障的最小组合，它代表对TLE的更简单的解释.TLE是MCS的析取，每个割集则是相应基本故障事件的合取.“bscu fail twice”的MCS共两个，为E2∧E5和E2∧E6.

4.3.2 故障模式和影响分析

FMEA以表格的形式显示了可能导致一个或多个故障状态的所有可能的事件组合.本次生成FMEA表依据的属性为：“bscu.mode=mode：Backup”.此属性表示的含义是：BSCU主模式失效.结果表明为了引发事件“bscu.mode=mode：Backup”，故障事件组合有以下几种情况.

1)基数为1的1个组合：

即“bscu.lru1.mon._errorSubcomponent.# invalidReport=True”.它代表BSCU子系统中的lru1的监控单元发生故障invalidReport.

2)基数为2的4种组合：

即“(hydr.green_pump._errorSubcomponent.# hydraulicError=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表液压调节系统的绿色液压泵出现故障hydraulicError并且BSCU子系统中的lru1的监控单元发生故障invalidReport.

以及“(hydr.green_pump._errorSubcomponent.# stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表液压调节系统的绿色液压泵出现故障stuck_at_zero并且BSCU子系统中的lru1的监控单元发生故障invalidReport.

以及“(power._errorSubcomponent.# close=True &bscu.lru1.mon._errorSubcomponent.#invalidReport=True)”.它代表电源组件出现故障close，并且BSCU子系统中的lru1的监控单元发生故障invalidReport.

以及“(power._errorSubcomponent.# depleted=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True)”.它代表电源组件出现depleted的故障，并且BSCU子系统中的lru1的监控单元发生故障invalidReport.

3)基数为3的4种组合：

即“(power._errorSubcomponent.# close=True &(bscu.lru1.mon._errorSubcomponent.#invalidReport=True &hydr.green_pump._errorSubcomponent.#hydraulicError=True))”.它代表电源组件出现故障close，BSCU子系统中的lru1的监控单元发生故障invalidReport，以及液压调节系统的绿色液压泵出现故障hydraulicError.

以及“(power._errorSubcomponent.#depleted=True &(bscu.lru1.mon._errorSubcomponent.#invalidReport=True &hydr.green_pump._errorSubcomponent.# hydraulicError=True))”.它代表电源组件出现故障depleted，BSCU子系统中的lru1的监控单元发生故障invalidReport，并且液压调节系统的绿色液压泵出现故障hydraulicError.

以及“(power._errorSubcomponent.#depleted=True &(hydr.green_pump._errorSubcomponent.# stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.# invalidReport=True))”.它代表电源组件出现故障depleted，液压调节系统的绿色液压泵出现故障stuck_at_zero并且BSCU子系统中的lru1的监控单元发生故障invalidReport.

以及“(power._errorSubcomponent.#close=True &(hydr.green_pump._errorSubcomponent.#stuck_at_zero=True &bscu.lru1.mon._errorSubcomponent.#invalidReport=True))”.它代表电源组件出现故障close，BSCU子系统中的lru1的监控单元发生故障invalidReport并且液压调节系统的绿色液压泵出现故障stuck_at_zero.

5 相关工作与小结

为了提高安全关键性系统的安全性，使用基于模型的安全评估技术对复杂系统进行形式化建模和安全性分析受到了学术界和工业界的关注.文献[7]提供了AADL的语法，介绍了它的接口和具体实现，并通过示例的讲解为AADL对大型系统的建模提供了思路.文献[9]详细介绍了AIR6110标准中的机轮刹车系统(WBS)，描述了它的架构以及功能需求，本文选择了它的最新架构图进行建模和分析.

与已有工作相比，本研究主要工作为：将WBS分为整体层、子系统层及设备层，采用AADL的子集SLIM对其进行系统级建模，充分考虑了组件之间的交互；针对文献[9]未说明BSCU的命令如何传到关闭阀从而对关闭阀进行控制，形式化建模时，在BSCU系统中单独建了一个select系统，它接受来自于监控单元的数据，用于判断是否使用备用液压，它的输出select_alternate会传到关闭阀从而对关闭阀进行控制；考虑WBS可能发生的故障并设计一系列故障模式，选择指定故障与系统正常功能行为合并为扩展模型，从而进行安全性分析.

尽管本文的研究结果论证了基于模型的安全分析方法对于提高安全关键性系统的安全性是有效的，但仍存在不足之处.未来的工作主要分为以下三部分：

1)本文建立的WBS的SLIM模型尚有改进空间，在建模时对于液压调节系统的所有子组件，只考虑了液压的输入和输出，而没考虑子组件造成液压的损耗.因此，下一步将完善机轮刹车系统的形式化模型；

2)对于模型的安全性分析，目前只考虑了定性属性，接下来会在模型中增加概率性属性[26]，进一步对WBS进行性能分析；

3)本文研究是从系统的架构层出发，未来将考虑系统的需求层面，证明WBS需求的一致性和完备性.