Improving System Reliability via Model Checking: The FSAP/NuSMV-SA Safety Analysis Platform
Improving System Reliability via Model Checking: The FSAP/NuSMV-SA Safety Analysis Platform
复制标题
通过模型检查提高系统可靠性：FSAP/NuSMV-SA 安全分析平台
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Adolfo Villafiorita
中科院分区：
文献类型：
--
作者：
M. Bozzano;Adolfo Villafiorita
安全关键系统正变得越来越复杂，无论是它们提供的功能类型，还是它们与环境交互的方式。这种日益增长的复杂性要求安全工程师充分提高评估系统安全性的能力，包括分析系统在退化情况下的行为。形式化验证技术，如符号模型检查，具有处理这种复杂性的潜力，并且在系统设计期间更经常使用。在本文中，我们提出了基于NuSMV2模型检查器的FSAP/NuSMV-SA平台，该平台实现了已知的和新颖的技术，以帮助安全工程师进行安全分析。FSAP/ nusv - sa的主要功能包括：基于故障模式库的故障模式定义、故障注入、单调和非单调系统的自动故障树构建、故障排序分析。目标是提供一个环境，设计工程师可以使用它来正式验证系统，安全工程师可以使用它来自动化安全评估的某些阶段。该平台是在ESACS项目（复杂系统增强安全分析）中开发的，ESACS项目是欧盟赞助的航空电子部门项目，其目标是定义一种方法来改进复杂系统开发的安全分析实践。
Safety critical systems are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with their environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the bahaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are more often being used during system design. In this paper we present the FSAP/NuSMV-SA platform, based on the NuSMV2 model checker, that implements known and novel techniques to help safety engineers perform safety analysis. The main functionalities of FSAP/NuSMV-SA include: failure mode definition based on a library of failure modes, fault injection, automatic fault tree construction for monotonic and non-monotonic systems, failure ordering analysis. The goal is to provide an environment that can be used both by design engineers to formally verify a system and by safety engineers to automate certain phases of safety assessment. The platform is being developed within the ESACS project (Enhanced Safety Analysis for Complex Systems), an European-Union-sponsored project in the avionics sector, whose goal is to define a methodology to improve the safety analysis practice for complex systems development.