支持SPIN验证的详细级SFMEA方法研究

刘　畅　李海峰　沈国华　顾　益　刘银陵

1(中国航空综合技术研究所　北京 100028)2(南京航空航天大学　江苏 南京 200016)



支持SPIN验证的详细级SFMEA方法研究

刘畅1李海峰1沈国华2顾益2刘银陵2

1(中国航空综合技术研究所北京 100028)2(南京航空航天大学江苏 南京 200016)

摘要随着软件系统的规模和复杂度不断增大，以软件为核心的安全关键系统的可靠性和安全性越来越难以保证。软件失效模式与影响分析SFMEA(Software Failure Modes and Effect Analysis)是军工业中常用的一种安全分析方法，其依赖人工分析、缺乏形式化语义、无法支持验证。针对SFMEA方法的不足，提出一种结合SPIN的详细级SFMEA方法，对软件失效模式进行形式化建模与分析，并结合模型检验工具SPIN进行自动化地模型检验和模拟仿真，从而提高软件系统的安全性和可靠性。该方法验证了“缓冲区数组下标越界”的这一失效模式，从而说明该方法的有效性。

关键词软件FMEA失效模式SPIN安全关键系统

0引言

当前嵌入式软件已经普遍运用于航空航天、交通运输、核电能源等安全关键领域。为了提供更为灵活和可靠的服务，嵌入式软件的规模和复杂性不断增加。用于安全关键领域的嵌入式软件一旦失效将有可能造成人员伤亡、财产损失等灾难性后果，因此，将这类嵌入式软件称为安全关键软件[1]。软件失效模式与影响分析[2]SFMEA方法提出于1979年，是工业界常用的软件安全性分析方法之一。SFMEA的基本思想是识别软件中的潜在失效模式；分析这些失效模式产生的原因并评估其对系统的影响；最后提出有效的改进措施以提高软件系统的安全性和可靠性。然而，传统的SFMEA方法仍然存在着一些问题和缺陷：传统方法采用自然语言描述失效信息，缺乏精确语义定义，容易产生二义性，制约了失效知识的存储和共享；另外，由于主要依靠人工分析，传统方法分析效率低、工作量大，结果易受分析人员主观经验影响，无法保证准确性。

针对上述问题，国内外学者们展开了一系列研究工作。文献[3]提出了一种基于灰色区间关联的SFMEA方法,通过计算各失效模式对象同理想评估对象的区间关联度,对水下机器人智能决策系统软件失效模式风险进行了定量评估。文献[4]在可信背景下，从软硬件FMEA对比和在软件分析和软件开发中的作用等方面详细分析了软件失效模式和影响分析技术。文献[5]对基于UML建模软件的SFMEA方法进行研究,建立了用例图和活动图与SFMEA分析要素之间的关系,并提出了一套分析方法。文献[6]提出了一种基于SFMEA的嵌入式软件质量控制方法，用以管理和分析实时嵌入式软件的多种失效模式。

基于上述研究，本文分析了传统的SFMEA方法，针对该方法的不足，结合模型检验工具SPIN，提出结合SPIN的SFMEA方法；关注了详细级的SFMEA安全性分析方法流程，用形式化的方法实现安全性模型验证；最后结合某型航空发动机数字控制系统的安全性实例分析，说明了该方法的实用性。

1结合SPIN的详细级SFMEA方法

1.1模型检验工具SPIN

SPIN是一个在有限状态系统中对于特定的安全属性进行正确性验证的工具。它擅长使用类似C语言语法的PROMELA建模语言对并发系统进行建模和分析。软件的失效模式可以转换为SPIN能识别的与PROMELA模型相容的验证属性。这些属性可以采用在模型中放置断言或使用LTL公式进行描述。SPIN工具提供了一个模型检验器和一个模拟器。模型检验器能通过自动检验程序的行为来判断一个PROMELA模型是否满足指定的验证属性；模拟器则可以通过模拟运行PROMELA模型代码，从而观察模型的可见行为[7]。如果某个安全属性没有被满足，那么模型检验器将返回一个供验证人员追踪查错的错误轨迹，即反例。模型检验在SFMEA中的意义：(1) 利用SPIN支持断言或LTL公式描述传统SFMEA方法采用自然语言描述失效信息，提高了语义定义的精确性，支持失效知识的存储和共享。(2) 利用SPIN中的PROMELA模型自动检验安全属性，解决了传统SFMEA方法中由于人工分析导致的分析效率低、工作量大，结果易受分析人员主观经验影响的缺陷。因此，本文采用结合SPIN的详细级SFMEA方法对软件失效模式进行形式化建模与分析，从而提高分析的准确性和充分性。

1.2结合SPIN的详细级SFEMA方法流程

由于详细级SFMEA的对象是已经编码实现的模块或由伪代码描述的模块，因此详细级SFMEA的实施繁琐且工作量大，对系统中的每个模块都进行详细级SFMEA既是不必要的也是不现实的。因此分析人员应当挑选系统中安全关键、逻辑复杂、与其它模块关系紧密的软件模块进行分析。图1给出了基于SPIN的详细级SFMEA的具体实施过程。

图1　结合SPIN的详细级软件FMEA过程

1.2.1建立目标模块的PROMELA模型

步骤一选定分析模块

在详细级SFMEA过程中，应当首先确定待分析的软件模块，有针对性地对相关软件模块进行详细级SFMEA分析以限制模块的可能危害。通过阅读软件系统需求规格说明文档，软件概要设计文档，分析人员将软件系统分解为子系统和子功能并从中重点确定系统中比较重要、容易发生风险的部分来进行分析。

步骤二C语言程序的PROMELA建模

在详细级SFMEA过程中,对目标模块的建模对象多为软件实现代码或程序伪代码,它们和PROMELA语言之间往往存在着许多一一对应的关系，这为转化为PROMELA模型提供了便利。因此，针对某种特定的程序设计语言，能够设计一套从程序设计语言到PROMELA模型的转换方法。根据这套转换方法，模型分析人员就能够方便快捷地对程序模块进行PROMELA建模，以支持后面的分析验证工作。从C语言到PROMELA的建模包括：基本类型建模、结构体类型建模、枚举型建模、变量作用域建模、控制语句建模、函数建模建模。

PROMELA出于效率等方面的考虑，不支持指针类型的建模[8]。然而C语言代码中广泛使用指针，因此有时必须对指针设法建模。这里论述指针类型建模的不必要性。然而事实上，像PROMELA这样的模型检验器输入语言要支持指针从理论上就是不可行的。因为模型检验需要保证模型状态的有限性，而指针却支持模型状态的动态扩充，因此不可能在PROMELA模型中对指针进行很好地建模。尽管在SPIN4.0版本以后我们可以利用SPIN允许内嵌C语言代码的功能，使用c_decl、c_code、c_expr等原语缓解对指针进行处理的问题。但是对指针进行转化的问题从根本上还是需要模型分析人员根据实际情况对源代码进行人工的转换来解决。譬如当需要对某结构指针(p)进行建模时，可以用该结构类型的变量(_pt_p)进行建模，然后当需要通过该指针取得结构内容((*p)->x)时，直接通过变量获取(_pt_p.x)，通过这样的一系列等价转换来避开对指针的建模。然而必须指出的是，并非所有的指针类型相关的程序都可以等价转换为不用指针的版本，因此对某些指针相关的建模验证可能无法进行。

下面将对C语言的核心模块——基本类型建模、控制语句建模、函数建模进行简要介绍。

1) 基本类型建模

C语言中的基本数据类型PROMELA语言中很多都有对应的类型，但是浮点数类型在PROMELA中是不支持的，原因很简单，因为浮点数的状态过多，而且不能精确表示，因此不适合作为模型检验程序的数据类型。表1给出了一种C语言和PROMELA语言的基本类型对应表。从表中可以发现，最后两种难以处理的类型一般都被简化处理为int类型，这样的做法在很多时候是适当地，但是毕竟改变了原来变量的语义，因此有些时候可能不适用，必须由模型分析人员根据实际情况特殊处理。

表1　C语言和PROMELA语言的基本类型映射表

2) 控制语句

C语言的主要控制语句有if、switch、while、for等，它们分别提供分支判断和循环等功能。PROMELA语言同样提供了对应的语法以支持分支和循环的控制能力。建模人员可以使用PROMELA中的if…fi语法对C语言中的if、switch等进行转换，使用do…od语法对while、for等进行建模，如图2所示。

图2　C语言控制语句到PROMELA模型的转换

3) 函数建模

PROMELA中没有函数的概念，然而C语言程序中却充满了函数调用，因此必须有一种方式将函数建模到PROMELA模型之中。好在PROMELA中有替代函数的语法特征，我们一般可以采用inline过程或者进程调用的方式来建模C语言中的函数调用。例如，对于图3(a)中的C语言代码片段，我们可以采用图3(b)中的inline过程对其进行转换，也可以像图3(c)中那样使用进程来进行转换。

图3　C语言函数到PROMELA的转换

1.2.2通过SPIN验证模块的失效模式

步骤三确定软件模块的失效模式

变量失效模式表示的是某个变量的值发生错误、超出范围等。变量失效模式可能是由于算法错误所导致，也可能是由于外部的异常输入所导致。表2给出了一些典型的变量失效模式。

表2　典型的变量失效模式

步骤四验证模块失效模式

详细级软件FMEA过程中的失效模式验证方法与系统级软件FMEA相同，而且此时由于PROMELA模型与实际代码或详细设计的联系更为紧密，因此验证的过程也更为容易。模型分析人员能够很方便地将安全性分析人员所给的各种变量失效和算法失效等转化为PROMELA模型中的待验证属性，通过SPIN的自动验证功能判断某潜在失效模式是否确实可能发生等。

1.2.3结合SPIN分析失效原因和影响

步骤五分析失效原因和影响

SPIN模型检验工具在验证一个安全属性时，如果验证过程出现问题，会生成一个反例文件。该反例文件中会记录一个从系统初始状态到出现安全属性验证失败状态的路径，模型分析人员能够追踪该路径，分析出该安全属性在系统模型中被违反的原因。将其映射到实际系统需求中，就能得到某一模式发生失效的原因。将其映射到实际系统需求中，就能得到某一模式发生失效的原因。为保证保证失效原因分析充分性，仍需在屏蔽了该失效原因的基础上继续分析验证系统的PROMELA模型，观察除了该失效原因以外是否仍然存在其他原因会导致同一个软件失效。

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

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

步骤六提出改进措施并形成详细级软件FMEA工作表

根据上述详细级软件FMEA分析过程，分析人员已经找到了目标软件模块中的各种潜在失效模式及其对本模块、其他模块乃至整个系统的影响。根据结合SPIN的失效原因分析，分析人员已经定位了产生失效的根源，此时应该与设计开发人员一同提出改进措施并修改设计或实现。为了分析工作的完整性，为今后的工作提供依据，最后还应该分别完成详细级变量FMEA工作表等。

由于此时的改进措施已经非常详细，此时的改进措施由安全性分析人员来提出已经意义不大，因此详细级软件FMEA过程中的改进措施应该主要由软件开发人员来提出，辅以安全性分析人员的把关。

最后，在结束了与详细级软件FMEA的综合分析后，形成详细级软件FMEA工作表。

2发动机数字控制系统实例分析

某型发动机控制系统的数据接收子模块由两个部分组成：一个接收数据缓冲区和一个数据接收函数。接收数据缓冲区其实主要就是一个数组，它负责将各通道和上位机发来的数据缓存起来，等待数据接收函数的读取。数据接收函数则负责从缓冲区中一帧一帧地读取和解析校验数据，并把已读取的数据帧从缓冲区中移除。

模型分析人员根据软件程序代码，结合本文介绍的从C语言代码到PROMELA模型的转换方法，将这两个部分分别建模。为了能够对这些程序模块进行验证，模型分析人员还建立了一个环境进程，负责产生各种输入数据帧。其中数据接收函数的PROMELA模型伪代码如下：

proctype ReceiveData()

{

g_dRegRead = 0;

if

:: g_dRegLength < DATA_FRAME_LENGTH -> skip;

:: else ->

do

:: if

:: g_dRegister[g_dRegRead] == head_data ->

copy data to g_sRS422Receive[];

if

:: g_sRS422Receive checks right ->

variates = g_sRS422Receive[1…n];

:: else ->

g_dRegRead = g_dRegRead + DATA_FRAME_LENGTH;

fi;

g_dRegRead = g_dRegRead + DATA_FRAME_LENGTH;

if

:: g_dRegLength - g_dRegRead >= DATA_FRAME_LENGTH -> skip;

:: else ->

copy g_dRegister[g_dRegRead…g_dRegRead+n] to g_dRegister[0…n];

g_dRegLength=g_dRegLength-g_dRegRead;

break;

fi;

:: else ->

g_dRegRead++;

if

:: g_dRegLength - g_dRegRead >= DATA_FRAME_LENGTH -> skip;

:: else ->

copy g_dRegister[g_dRegRead…g_dRegRead+n] to g_dRegister[0…n];

g_dRegLength=g_dRegLength-g_dRegRead;

break;

fi;

在结合SPIN的发动机控制系统详细级FMEA过程中，我们需要对失效模式进行逐一验证。

本例针对失效模式—缓冲区数组下标越界引用进行验证。该失效模式不需要模型分析人员将其转化为PROMELA模型中的验证元素，因为SPIN会自动检测所有的数组越界引用问题。通过SPIN的模型检验，模型分析人员会发现该失效模式确实可能在该软件模块中发生，即这段代码确实可能产生缓冲区数组越界引用的失效，如下所示：

>spin -a controller.pml

>gcc -DSAFETY -DCOLLAPSE -o controller.exe pan.c

>controller.exe -m100000

pan:1: assertion violated - invalid array index (at depth 18378)

pan: wrote controller.pml.trail

通过SPIN分析失效原因和影响

结合SPIN的详细级SFMEA过程中，由于PROMELA模型与实际的C语言代码更为接近，因此模型分析人员能够更加方便高效地追踪反例，分析出失效原因。这个过程类似于固定执行路径的程序单步调式过程，分析人员可以在每一步中观察系统当前的所有变量的状态，从而分析出导致软件存在某个失效模式的原因。

如本例中的“缓冲区数组下标越界”这一失效模式，通过分析人员对反例的追踪分析，发现导致失效模式的原因是在数据帧校验失败的分支中多了一句数组下标向后移动的语句。

详细级分析过程中的失效影响分析可以借助SPIN的模拟运行方式加以辅助，以提高分析的效率和准确性。如本例中的失效影响，通过对PROMELA模型的模拟运行，模型分析人员可以发现该编码问题在本模块中除了会导致数据越界的问题以外，更多的是会导致数据帧丢失的问题，如下所示：

>spin -u2000 receive.pml

产生数据：1, 1, 11, 3, 5, 7, 21, 2/*不能通过校验的数据帧*/

产生数据：1, 1, 12, 15, 3, 4, 11, 3/*正确的数据帧*/

产生数据：1, 1, 3, 12, 14, 1, 5, 13/*正确的数据帧*/

…

校验不通过！

接收数据：1, 1, 3, 12, 14, 1, 5, 13/*丢失了第二条数据帧*/

…

spin: indexing g_dRegister[36] - size is 100

在结合SPIN的发动机控制系统详细级SFMEA过程的最后，安全性分析人员与软件开发人员一同对各个失效模式提出改进措施，进而修改程序代码，提高软件系统的质量[9]。并总结工作，完成各种详细级SFMEA工作表。部分详细级变量FMEA工作表如表3所示。

表3　发控系统部分详细级变量FMEA工作表

从该实例分析可以看出，结合SPIN的详细级SFMEA方法，利用SPIN工具的模型检验和模拟运行功能，辅助进行失效原因和失效影响分析工作，使分析方法在准确性、充分性和自动化程度等方面都比传统方法有很大提高。

3结语

本文研究分析了传统的SFMEA方法，针对该方法的不足，

结合模型检验工具SPIN，提出了结合SPIN的详细级SFMEA方法；重点关注详细级的SFMEA安全性分析方法流程，用形式化的方法实现安全性模型验证；最后结合实例分析，详细介绍了本文所提出的方法在实际工程项目中的使用过程，说明了该方法的实用性。

本文的主要工作总结如下：

(1) 在传统SFMEA方法的基础上，结合模型检验技术，提出了一种结合SPIN的SFMEA方法。该方法实现了自动化的验证了软件失效模式，解决了传统SFMEA依赖人工，缺乏形式化语义以及无法支持验证的问题。

(2) 本文详细介绍了结合SPIN的SFMEA流程，以及分析目标的形式化建模方法。给出了使用本文方法进行安全性分析的具体过程，并阐述了模型检验与软件失效模式与影响分析方法相结合的解决方案。

(3) 本文通过结合SPIN的SFMEA方法对某型航空发动机数字控制系统进行了安全性分析实例研究。通过实际工程项目详细介绍了使用本文方法进行实践分析的步骤和细节，说明了本文提出的安全性分析方法的实用性。

参考文献

[1] NASA-STD-8710.13B.Software Safety Standard [S].USA:National Aviation and Space Association,2004.

[2] Reifer J.Software Failure Modes and Effect Analysis[J].IEEE Transaction on Reliability,1979,28(3):247-249.

[3] 史长亭,张汝波.改进SFMEA的AUV风险评估方法[J].哈尔滨工程大学学报,2011,32(3):345-349.

[4] 刘俊丽.可信软件失效模式和影响分析技术研究[J].电子商务,2014(12):47-48.

[5] Shi H,Wang X.FMEA-Based Control Mechanism for Embedded Control Software[C]//Information Technology,Computer Engineering and Management Sciences(ICM),2011 International Conference on,IEEE.2011:110-112

[6] 王雁涛,王毅,杨钿.软件需求分析阶段基于UML的SFMEA方法研究[J].舰船电子工程,2013,33(8):119-122.

[7] Ben-Ari M.Principles of the Spin model checker[M].Springer,2008.

[8] 郑军,黄志球,徐丙凤.机载软件适航认证标准新进展及展望[J].计算机工程与设计,2012,33(1):204-208.

[9] Schröter C,Schwoon S.The model-checking kit[R].Applications and Theory of Petri Nets,2003:463-472.

ON DETAILED-LEVEL SFMEA METHOD SUPPORTING SPIN VERIFICATION

Liu Chang1Li Haifeng1Shen Guohua2Gu Yi2Liu Yinling2

1(ChineseAviationCompositeTechnologyResearchInstitute,Beijing100028,China)2(NanjingUniversityofAeronauticsandAstronautics,Nanjing200016,Jiangsu,China)

AbstractWith the increment in scale and complexity of software systems, the reliability and safety of the safety-critical system which taks software as the core are becoming increasingly difficult to guarantee. Software failure mode and effect analysis (SFMEA) is a common safety analysis method in military industries. However, it depends on manual analysis, lacks the formal semantics and does not support verification. In light of the deficiencies of SFMEA, we propose a detailed-level SFMEA method which combines SPIN to carry out formalised modelling and analysis on software failure mode. Moreover, in combination with model verification tool SPIN it makes automatic model verification and simulation so as to improve the security and reliability of software system. The method validates the failure mode of “out of bound of array subscripts in buffer zone”, therefore explains the effectiveness of the method.

KeywordsSoftware FMEAFailure modeSimple Promela Interpreter (SPIN)Safety-critical system

收稿日期：2014-12-08。国家自然科学基金项目(61272083)。刘畅，高工，主研领域：软件安全性工程，软件工程，需求验证。李海峰，高工。沈国华，副教授。顾益，硕士。刘银陵，硕士。

中图分类号TP311

文献标识码A

DOI:10.3969/j.issn.1000-386x.2016.05.070