基于AltaRica的模型转换与安全性验证方法研究

摘要

随着航空、交通、医疗等安全关键系统的规模越来越大，如何提高复杂关键安全系统的安全性，防止重大人员伤亡，成为急需解决的问题。传统建模方式所创建的模型和实际的系统差别很大，模型不能在整个开发设计过程中使用。规范中很小的变动就可能导致重新遍历所有安全模型，容易出错也消耗资源。高级别建模语言AltaRica的提出解决了这一问题，AltaRica模型是一种组件可重用的层次结构，由法国工业和学术协会专门为工业系统的安全评估所设计的一门MBSA建模语言。
　　随着AltaRica3.0的更新，ARC等传统的AltaRica建模分析工具已不再支持，而SPIN作为一个穷尽式模型验证工具被广泛应用。由于SPIN不能直接用来对AltaRica3.0模型分析和验证，因此需要将AltaRica3.0模型转换为Promela模型。
　　针对上述问题，本文的主要工作是提出了来一种基于Simfia图形化建模，转换为AltaRica3.0模型，继而转换为Promela模型，随后使用SPIN工具验证的一套从建模到转换到验证的方法。具体工作如下所示：
　　(1)提出了基于Simfia的AltaRica3.0建模方法，并使用飞机的显示控制系统为例建模并分析其故障树。首先介绍了AltaRica3.0和Simfia的基本知识，分析了AltaRica3.0和Simfia模型的特点；提出了基于Simfia的AltaRica3.0模型的建模方法，指出了Simfia模型元素和AltaRica3.0模型元素之间的映射关系；最后以飞机的显示控制系统为例，为其建立了Simfia模型，并转换为了AltaRica3.0模型，使用故障树分析软件对其故障树做了简要分析。
　　(2)分析了 AltaRica3.0模型扁平化为 GTS模型的具体方法，并吸取其思想提出了AltaRica3.0模型转换为Promela模型的详细方法。首先分析了AltaRica3.0扁平化为GTS模型的详细规则；分析了 AltaRica3.0和 Promela的语义模型；根据扁平化思想提出了 AltaRica3.0模型转换为 Promela模型的详细规则，并验证了其可行性；最后以简单供水系统为例说明了AltaRica3.0模型转换为Promela模型的步骤。
　　(3)以飞机的机轮刹车系统为例，为其建立了AltaRica3.0模型，并转换为Promela模型进行分析和验证。以飞机的机轮刹车系统为例，对其建立AltaRica3.0模型，使用Arbre Analyste对其故障树进行分析；将其转换为Promela模型使用SPIN分析和验证，通过综合两种分析方式得出的结论对系统进行评估，并给出修改意见。

目录

声明

缩略词

第一章 绪论

1.1研究背景

1.2当前研究现状

1.3研究目的和意义

1.4论文研究内容

1.5论文组织结构

第二章 基于形式化的系统安全性分析概述

2.1形式化安全分析方法

2.2传统安全性分析方法

2.3基于模型的安全性分析

2.4本章小结

第三章 基于Simfia的AltaRica3.0建模

3.1 AltaRica3.0概述

3.2 Simfia概述

3.3 基于Simfia建立AltaRica3.0模型

3.4本章小结

第四章 AltaRica3.0到Promela的转换方法

4.1 AltaRica3.0扁平化为GTS模型规则

4.2 AltaRica模型和Promela模型的语义

4.3 AltaRica3.0模型到Promela模型的转换规则

4.4 AltaRica3.0模型转换为Promela模型流程

4.5本章小结

第五章 机轮刹车系统的建模分析与验证

5.1 机轮刹车系统简介

5.2 机轮刹车系统的AltaRica3.0建模

5.3 机轮刹车系统分析与验证

5.4 本章小结

第六章 总结与展望

6.1 论文工作总结

6.2 未来工作展望

参考文献

致谢

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