基于SPIN的系统级失效模式与影响分析方法研究

顾 益，黄志球

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

基于SPIN的系统级失效模式与影响分析方法研究

顾 益，黄志球

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

为保证关键软件系统的安全性和可靠性，对软件失效模式与影响分析方法在实际应用中存在的问题进行了分析研究，结合模型检验技术提出了一种基于SPIN的系统级失效模式与影响分析方法。该方法运用SPIN模型检验工具的验证和模拟功能，有效提高了失效模式分析的准确性和充分性。此外还结合某型航空发动机控制系统介绍了一个应用实例，证明了该方法在工程实践中的可行性。

模型检验;SFMEA;SPIN;PROMELA;失效模式

随着计算机软硬件系统的日益复杂，保证软件系统的安全性和可靠性已成为日益紧迫的问题。在软件设计的早期(如需求分析或概要设计阶段)，尽可能多地找到软件系统的潜在失效模式能极大地降低分析成本，从根本上保证软件系统的安全性和可靠性。

研究发现，传统的安全性分析方法——软件失效模式与影响分析(Software Failure Modes and Effect Analysis，SFMEA)［1］——在实际应用中存在着许多问题。首先，传统的SFMEA过分依赖分析人员的技能和经验，使得分析效率较低并且分析结果不够精确;其次，传统的SFMEA过程中的失效原因分析依靠分析人员人工完成，无法保证原因分析的正确性和完备性;最后，传统的SFMEA过程中的失效影响分析同样依靠分析人员人工完成，无法保证分析结果的充分性，而且工作量巨大。

SPIN［2］是一款由贝尔实验室研发的模型检验工具，它使用特定的解释语言PROMELA对软件系统进行建模，并在此基础上对模型的各种安全属性进行验证;此外，SPIN还支持对PROMELA模型的模拟运行，以观察软件设计模型的行为。SPIN的这些功能恰好能够弥补传统SFMEA方法由于人工分析导致的缺陷，从而提高分析的准确性和充分性。

因此，本文提出了一种基于SPIN的系统级SFMEA方法，利用SPIN模型检验工具的验证和模拟功能，在传统SFMEA过程的失效模式提取、失效原因分析、失效影响分析和改进措施的提出等多个步骤中帮助分析工作更加有效地进行。

1 基于SPIN的系统级SFMEA方法

本文针对传统SFMEA方法精确性低、客观性差、工作量大等问题，提出了基于SPIN的系统级SFMEA方法。该方法应用在软件开发的需求分析或概要设计阶段，目的是对软件体系结构和高级设计进行安全性评估和分析，在软件实现之前为改进软件设计提供依据，从而提高软件系统的安全性和可靠性。

基于SPIN的系统级SFMEA方法除了传统方法中所需的安全性分析人员以外，还需要模型分析人员的加入。安全性分析人员负责提取失效模式、分析失效原因、分析失效影响等工作;模型分析人员则负责系统建模、失效模式验证等工作。两类人员必须协同配合，才能成功完成整个安全性分析工作。基于SPIN的系统级SFMEA方法整体流程如图1所示。

步骤一，熟悉系统需求。

基于SPIN的系统级SFMEA过程的第一步是熟悉系统需求，确定所要分析的目标，并设法对其进行描述。分析人员可以通过阅读软件系统需求规格说明文档、软件概要设计文档等来了解待分析的软件对象，然后将软件系统分解为子系统和子功能，重点确定系统中比较重要、容易发生风险的部分来进行分析。

图1 基于SPIN的系统级SFMEA流程图

步骤二，建立系统的PROMELA模型。

软件需求建模方法是软件工程中长期研究讨论的问题，本文提出的安全性分析方法需要借助SPIN模型检验工具进行验证分析，因此采用PROMELA建模语言对需求进行建模。PROMELA语言本身就非常适合用于对并发控制系统进行建模，因此使用PROMELA建立的模型可以很好地描述软件系统需求，为模型分析人员的验证和分析工作提供基础。

软件系统的PROMELA建模当前仍然主要依靠人工手动完成，对于不同的软件系统，具体的建模方法也不尽相同。但是，对于一般的软件需求，模型分析人员可以从以下4个方面展开建模工作:建立系统各主要进程、建立环境进程、建立模块间调用关系、抽象未实现的功能模块。

步骤三，提取功能模块的失效模式。

安全性分析人员在确定分析目标并且构建系统层次及依赖关系模型之后，就可以开始着手提取软件系统的失效模式，确定目标模块的各种失效，以形成软件模块的失效模式列表。

提取软件失效模式的方式有很多，安全性分析人员一般可以从以下3个方面进行失效模式的提取工作:从通用失效模式集中提取、从特定软件失效模式库中提取、针对特定软件模块分析提取。

步骤四，通过SPIN验证系统的失效模式。

模型分析人员不能够直接针对失效模式进行验证，因为模型检验工具只能识别形式化的验证属性，因此当模型分析人员得到了安全性分析人员提供的软件模块失效模式列表以后，首先必须着手将这些软件失效逐一转化为SPIN能够识别的与系统PROMELA模型相容的验证属性，如断言(assertion)、LTL(Linear Temporal Logic)公式［3］等。然后利用SPIN的模型检验功能，自动地对各失效模式进行验证，判断其是否有可能在系统模型中发生。更重要的是，如果证明可能发生失效，SPIN会自动生成一个反例文件，以记录原因。

步骤五，通过SPIN反例分析失效原因。

SPIN模型检验工具在验证一个安全属性时，如果验证过程出现问题，会生成一个反例文件。该反例文件中会记录一个从系统初始状态到出现安全属性验证失败状态的路径，模型分析人员能够追踪该路径，分析出该安全属性在系统模型中被违反的原因，将其映射到实际系统需求中，就能得到某一模式发生失效的原因。

然而，当模型分析人员找到了导致某个软件失效的原因之后，仍不能结束失效原因的分析工作，而应该设法在屏蔽了该失效原因的基础上继续分析验证系统的PROMELA模型，观察除了该失效原因以外是否仍然存在其他原因会导致同一个软件失效，这是保证失效原因分析充分性的必要工作。

步骤六，通过SPIN模拟分析失效影响。

对于每个提取出的软件失效模式，在查找出了失效原因的基础上，应当进一步分析其失效影响。

基于SPIN的SFMEA分析过程中，对失效影响的分析仍然借助于SPIN工具。SPIN除了可以进行模型检验以外，还能够对PROMELA模型进行模拟运行。因此，可以利用SPIN的模拟运行能力，对存在失效模式的PROMELA模型进行模拟运行，其运行结果会体现模型在这种情况下的表现。将这些表现映射到实际的软件系统之中，就成为了该失效模式的失效影响。

步骤七，提出改进措施并完成系统级SFMEA工作表。

为了有效地控制软件失效，分析人员应当根据每个软件失效模式发生的原因、产生的影响以及严酷度等级，综合地提出有针对性的改进措施。然后将改进措施同样建模到系统的PROMELA模型之中，再次进行验证，以判断改进措施的有效性。

最后，分析人员还需要填写系统级SFMEA工作表，以完整地记录分析的过程和取得的成果。

2 实例分析

某型航空发动机数字控制系统负责对某型航空发动机的燃油供油量、风扇导叶角度、矢量喷管位移等进行控制。该型航空发动机数字控制软件主要包括系统初始化、信号采集、信号处理、故障诊断与处理、控制逻辑处理、控制算法处理、信号输出、通讯等功能。本文以某型航空发动机数字控制系统为例，通过基于SPIN的系统级SFMEA方法对其进行安全性分析，说明该方法在工程实践中的可行性。

首先，分析人员通过阅读需求说明文档，了解了该型发动机控制系统(以下简称发控系统)的设计需求，然后针对发控系统的各个模块进行PROMELA建模，并合并化简为一个统一的PROMELA模型。接着对各个模块及其子模块展开分析，提取出每个模块中的失效模式，将这些失效模式转化为系统PROMELA模型中的验证属性，并进行验证。根据对SPIN产生的反例进行追踪分析，寻找导致失效的原因，再通过SPIN的模拟来分析失效影响。最后综合上述分析，对每条失效模式提出相应的改进措施，并整理完成系统级SFMEA工作表［4］。

本文仅在此对发控系统中控制逻辑处理模块做一个详细的举例分析。

首先，分析人员认真理解控制逻辑处理模块的需求规约，如其中“假开车控制”过程的需求如下所示:

进入条件:油门杆角度位于慢车域，“假开车信号”和“起动按钮信号”有效，“起落架放下信号”有效，且“起落架收起信号”无效。

控制过程:

(1)0s开始，输出“起动机控制信号”，持续60s后进入停车控制;

(2)0s开始，输出“起动电磁阀信号”，持续5s;

(3)整个过程中按“起动供油规律”输出主燃油起动供油流量，且“主燃烧室点火信号”无效。

此时，分析人员便能将发控系统的控制逻辑处理模块用PROMELA语言进行建模。其中“假开车控制”功能的PROMELA模型如图2所示。

图2 假开车控制功能的PROMELA模型

然后，针对该模块内的各个软件部件展开失效模式分析，列出失效模式列表，见表1。

表1 初步分析所得失效模式列表

接着，将表中的失效模式转化为系统模型中的验证属性，代入系统PROMELA模型进行验证。如第5条“冷运转控制异常被假开车控制打断”可以用LTL公式“＜＞((g_status==s_cool_run)U(g_status!=s_init)U(g_status==s_dummy_start))＆＆ ＜＞(g_status==s_cool_run)”来表示，其中g_status是当前系统的控制状态，s_cool_run、s_init、s_dummy_start分别表示冷运转状态、系统初始状态和假开车状态，这个LTL公式的直接意义是“存在一种情况，使得g_status先为s_cool_run，然后不经过g_status为s_init的情况再直接满足g_status为s_dummy_start的情况”。通过这个LTL公式，SPIN可以验证其是否可能在系统运行中发生，反映到实际的软件系统中也就是冷运转控制是否可能被假开车控制异常打断。

将这一系列的验证属性逐一用SPIN进行验证，发现第1条“从起动状态进入未知状态”这种失效模式不可能发生，因此可以将其从表格中删除，而第5条失效模式“冷运转控制异常被假开车控制打断”却可能发生。

接下来针对那些可能发生的失效模式进行失效原因的分析。譬如第5条“冷运转控制异常被假开车控制打断”，分析人员根据SPIN产生的反例文件进行追踪分析，发现导致该失效的原因是“冷运转过程中，油门杆被推到了慢车域，并且按下了假开车按钮，此时系统虽然没有完成冷运转控制功能，却一下子进入了假开车控制了”，这是发动机控制系统需求所不允许的情况。通过SPIN的模拟运行，分析人员发现该失效模式可能导致整个系统的状态迁移异常，使得“冷运转控制”功能始终无法完成。最后，通过对该失效模式失效原因和失效影响的分析，得出第5条失效模式的改进措施为“在假开车控制的进入条件中增加额外限制，还要求在初始条件下才能进入假开车控制”。总结的部分系统级SFMEA工作表见表2。

表2 发动机控制系统SFMEA工作表

3 结束语

基于SPIN的SFMEA方法能够弥补传统方法对分析人员过分依赖、精确性低、自动化程度差等问题，然而需要安全性分析人员与模型分析人员协同合作才能达到最好的效果，因此可以基于本文方法，开发一个原型系统以规范整个方法的实施，保证最好的分析效果。

［1］Goddard P L.Software FMEA techniques［C］//Reliability and Maintainability Symposium.［S.l.］:IEEE，2000:138 －144.

［2］Ben－Ari M.Principles of the Spin model checker［M］.［S.l.］:Springer，2008:45 －50.

［3］Vardi M.Branching vs linear time:Final showdown［J］.Tools and Algorithms for the Construction and Analysis of Systems，2001(1):1－22.

［4］郑军，胡军，柯昌博，等.综合模块化航电软件系统测试方法研究综述［J］.计算机应用与软件，2012，29(5):163－168.

The System Level SFMEA Methodology Based on SPIN

GU Yi，HUANG Zhiqiu
(Nanjing University of Aeronautics and Astronautics，Jiangsu Nanjing，210016，China)

In order to increase the complexity of software systems，it is important to ensure the correctness and reliability of critical software.The traditional software failure modes and effect analysis methodology is lack of accuracy and completeness because of the restrict of the artificial work.Therefore，it presents SPIN based system level SFMEA methodology，which can provide more accuracy and more completeness analysis for the system.It also describes a case study of one aero engine using this mothedology to prove the feasibility of the mothedology.

Model Checking;SFMEA;SPIN;PROMELA;Failure Mode

TP311

A

2095－509X(2013)05－0055－04

10.3969/j.issn.2095 －509X.2013.05.014

2013－01－14

顾益(1987—)，男，江苏太仓人，南京航空航天大学硕士研究生，主要研究方向为模型检验、软件安全性分析、软件形式化方法等。