基于特征配置的系统安全性建模和分析方法

摘要

伴随着计算机技术的发展，嵌入式系统在诸如航空航天、核应用、轨道交通和医疗等安全关键领域的应用更加广泛。如何保障系统的安全性，防止系统故障导致灾难性事故发生，成为当前安全工程和软件工程领域的研究热点。在业界开发的基于模型的安全性分析项目中，由欧洲宇航局开发的COMPASS项目，使用SLIM对诸如航天器系统这样的安全关键系统进行建模，不仅可以描述系统标定的软硬件行为，还可以描述系统的概率性故障、故障对系统的影响和系统恢复，使得SLIM语言逐渐成为欧洲航天局在系统建模方面的标准语言。然而，原始的SLIM建模方法，对真实系统在故障情况下的行为描述不够准确、针对SLIM的传统安全性分析过程中面临着故障空间过大的问题。
　　针对系统的安全性分析工作，本文从软件产品线的角度提出一种基于特征配置的系统安全性建模和分析方法。特征模型是软件产品线工程中描述软件产品家族共性和可变性特征以及特征之间关系的模型。利用基于软件产品线的模型检测工具 SNIP能够一次检测特征集内的所有产品是否违反了规定的属性。对于系统中故障组合空间巨大问题，软件产品线中的特征组合与系统中的故障组合契合，因此，将软件产品线特征配置思想应用到系统安全性分析中。
　　首先，基于软件产品线的特征配置思想、利用SLIM建立系统的扩展模型；结合软件产品线的特征配置思想对原始SLIM模型中的故障注入方法进行修改，为系统建立故障模型。通过故障模型，将标定模型和错误模型关联，形成系统的SLIM扩展模型。
　　然后，将SLIM扩展模型转换到软件产品线模型检测工具SNIP能够识别的fPromela+TVL模型；通过对SLIM和fPromela+TVL的语义进行分析，给出了SLIM扩展模型到fPromela+TVL模型的转换规则，并对转换的正确性作出证明；在得到fPromela+TVL模型基础上，为TVL中的故障添加约束关系。进一步，利用线性时序逻辑对安全性需求进行规约，结合转换后生成的fPromela+TVL模型，使用软件产品线模型检测工具SNIP对模型进行安全性验证工作，得出验证结果。
　　最后，针对本文提出的基于特征配置的系统安全性建模和分析方法，设计并实现了系统安全性建模和分析工具S2F。运用本论文提出的方法、结合实现的S2F工具，对空客A320液压系统进行实例分析。

目录

声明

缩略词

第一章 绪论

1.1 研究背景

1.2 当前研究现状和选题依据

1.3 论文研究内容

第二章 基于特征配置的系统安全性建模和分析方法

2.1 基于模型的安全性分析MBSA

2.2 软件产品线和基于软件产品线的安全性分析

2.3 基于特征配置思想的系统安全性建模和分析框架

2.4本章小结

第三章 基于特征配置的SLIM建模方法

3.1 系统层综合建模语言SLIM

3.2建立系统的扩展模型

3.3 本章小结

第四章 基于SNIP的SLIM扩展模型转换和安全性分析

4.1 SLIM和fPromela、TVL的语义

4.2 SLIM扩展模型到fPromela+TVL模型的转换

4.3 基于SNIP的SLIM扩展模型的安全性分析

4.4 本章小结

第五章 工具实现和实例分析

5.1 S2F原型工具

5.2 空客A320飞机液压系统实例分析

5.3 本章小结

第六章 总结与展望

6.1 论文总结

6.2 未来工作

参考文献

致谢

在学期间的研究成果及发表的学术论文