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

《基于SPIN的系统级失效模式与影响分析方法研究.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、2013年5月机械设计与制造工程Malv．2013第42卷第5期MachineDesignandManufacturingEngineeringV01．42No．5DOI：10．3969／j。issn．2095—509X．2013．05．014基于SPIN的系统级失效模式与影响分析方法研究顾益，黄志球(南京航空航天大学计算机科学与技术学院，江苏南京210016)摘要：为保证关键软件系统的安全性和可靠性，对软件失效模式与影响分析方法在实际应用中存在的问题进行了分析研究，结合模型检验技术提出了一种基于SPIN的系统级失效模式与影响分析

2、方法。该方法运用SPIN模型检验工具的验证和模拟功能，有效提高了失效模式分析的准确性和充分性。此外还结合某型航空发动机控制系统介绍了一个应用实例，证明了该方法在工程实践中的可行性。关键词：模型检验；SFMEA；SPIN；PROMELA；失效模式中图分类号：TP31l文献标识码：A文章编号：2095—509X(2013)05—0055—04随着计算机软硬件系统的Et益复杂，保证软件拟功能，在传统SFMEA过程的失效模式提取、失系统的安全性和可靠性已成为日益紧迫的问题。效原因分析、失效影响分析和改进措施的提出等多在软件设计的早期(如需

3、求分析或概要设计阶个步骤中帮助分析工作更加有效地进行。段)，尽可能多地找到软件系统的潜在失效模式能极大地降低分析成本，从根本上保证软件系统的安1基于SPIN的系统级SFMEA方法全性和可靠性。本文针对传统SFMEA方法精确性低、客观性研究发现，传统的安全性分析方法——软件失差、工作量大等问题，提出了基于SPIN的系统级效模式与影响分析(SoftwareFailureModesandSFMEA方法。该方法应用在软件开发的需求分析EfectAnalysis，SFMEA)⋯——在实际应用中存在或概要设计阶段，目的是对软件体系结构和高级设

4、着许多问题。首先，传统的SFMEA过分依赖分析计进行安全性评估和分析，在软件实现之前为改进人员的技能和经验，使得分析效率较低并且分析结软件设计提供依据，从而提高软件系统的安全性和果不够精确；其次，传统的SFMEA过程中的失效可靠性。原因分析依靠分析人员人工完成，无法保证原因分基于SPIN的系统级SFMEA方法除了传统方析的正确性和完备性；最后，传统的SFMEA过程法中所需的安全性分析人员以外，还需要模型分析中的失效影响分析同样依靠分析人员人工完成，无人员的加入。安全性分析人员负责提取失效模式、法保证分析结果的充分性，而且工作量巨大

5、。分析失效原因、分析失效影响等工作；模型分析人SPIN是一款由贝尔实验室研发的模型检验员则负责系统建模、失效模式验证等工作。两类人工具，它使用特定的解释语言PROMELA对软件系员必须协同配合，才能成功完成整个安全性分析工统进行建模，并在此基础上对模型的各种安全属性作。基于SPIN的系统级SFMEA方法整体流程如进行验证；此外，SPIN还支持对PROMELA模型的图1所示。模拟运行，以观察软件设计模型的行为。SPIN的步骤一，熟悉系统需求。这些功能恰好能够弥补传统SFMEA方法由于人基于SPIN的系统级SFMEA过程的第一步是工分

6、析导致的缺陷，从而提高分析的准确性和充分熟悉系统需求，确定所要分析的目标，并设法对其性。进行描述。分析人员可以通过阅读软件系统需求因此，本文提出了一种基于SPIN的系统级规格说明文档、软件概要设计文档等来了解待分析SFMEA方法，利用SPIN模型检验工具的验证和模的软件对象，然后将软件系统分解为子系统和子功收稿日期：2013一O1—14作者简介：顾益(1987一)，男，江苏太仓人，南京航空航天大学硕士研究生，主要研究方向为模型检验、软件安全性分析、软件形式化方法等。·55·2013年第42卷机械设计与制造工程能，重点确定系统中比较

7、重要、容易发生风险的部性，因此当模型分析人员得到了安全性分析人员提分来进行分析。供的软件模块失效模式列表以后，首先必须着手将这些软件失效逐一转化为SPIN能够识别的与系统安全性分析人员模型分析人员I熟悉系统需求lPROMELA模型相容的验证属性，如断言(asser—+l确定分析目标l⋯_．tion)、LTL(LinearTemporalLogic)公式等。然后～～～～鬯鲠墨l提取系统的失效模式l～利用SPIN的模型检验功能，自动地对各失效模式～～一一一∑2鲻．进行验证，判断其是否有可能在系统模型中发生。更重要的是，如果证明可能发生

8、失效，SPIN会自动，世中曲生成一个反例文件，以记录原因。J分析失效原因·一步骤五，通过SPIN反例分析失效原因。1分析失效影响卜

9、一●SPIN模型检验工具在验证一个安全属性时，l。确定失效模式严酷度I●。改进措如果验证过程出现问题，会生成一个反例