面向AltaRica模型的系统安全性设计验证方法研究

摘要

随着计算机技术的迅速发展，嵌入式系统在医疗、交通、通信、航空航天等安全关键领域已得到广泛运用。如何提高系统的安全性，防止灾难性事故发生，已经成为当前软件工程领域重要的研究课题。AltaRica语言是一种描述正常情况下系统功能行为，同时描述系统存在的失效行为的建模语言，面向AltaRica模型的系统安全性分析是当前的研究热点之一。目前已有相应的一些工具利用AltaRica模型进行系统安全性分析，而支持AltaRica模型的穷举分析和时序属性方面的验证工具还很缺少，成熟的模型检测工具SPIN对模型的穷举分析和线性时序逻辑验证有很大优势，但SPIN工具并不能直接对AltaRica模型进行验证。
　　针对以上问题，本文首先将AltaRica模型转换到Promela模型，对安全需求使用线性时序逻辑进行规约；然后将Promela模型导入模型检测工具SPIN进行验证和分析；最后结合验证结果和可追踪性信息模型，追踪AltaRica模型存在的设计缺陷。本文的主要研究内容如下：
　　第一，通过对AltaRica模型和Promela模型的语义分析，提出了AltaRica模型到Promela模型的转换规则，并对两模型语义的等价性进行证明。使用线性时序逻辑对安全性需求进行规约并结合转换得到的Promela模型导入模型检测工具进行形式化验证。在此基础上，提出一种面向AltaRica模型的系统安全性设计验证方法。
　　第二，针对模型检测的验证结果，给出了根据验证结果的反例路径追踪到AltaRica模型设计缺陷的可追踪性信息模型。通过对验证结果和AltaRica模型的分析，首先给出验证结果可追踪性信息模型的元模型；然后根据具体的追踪目标实例化元模型，得到可追踪性信息模型；最后基于可追踪性信息模型设计追踪算法，实现根据验证结果的反例路径追踪查找AltaRica模型的设计缺陷甚至系统组件存在的安全性问题。
　　第三，针对本文提出的面向AltaRica模型的系统安全性设计验证方法，设计并实现相应的原型工具A2STool，对A2STool的功能模块进行相应地说明，并给出该工具的设计框架、执行流程以及关键的实现技术。
　　最后，运用本文提出的方法对机轮刹车系统控制单元进行案例分析，利用原型工具给出了AltaRica模型到Promela模型转换的完整过程，使用SPIN对Promela模型和安全性需求的线性时序逻辑规约进行验证和分析，接着基于验证结果结合可追踪性信息模型发现系统安全性设计缺陷。说明了本文方法的有效性和可行性，为系统的安全性分析提供了一种新思路。

目录

封面

声明

中文摘要

英文摘要

目录

缩略词

第一章 绪论

1.1 课题研究背景

1.2 国内外研究现状及选题依据

1.3 论文组织结构

第二章 面向AltaRica模型的系统安全性设计验证方法

2.1 系统安全性设计AltaRica模型

2.2 形式化方法和模型检测

2.3 面向AltaRica模型的系统安全性设计验证框架

2.4 本章小结

第三章 基于SPIN的AltaRica模型转换与安全性验证

3.1 AltaRica模型和Promela模型的语义

3.2 AltaRica模型到Promela模型的转换

3.3 基于SPIN的AltaRica模型安全性验证

3.4 本章小结

第四章 系统安全性设计的可追踪性

4.1 面向系统安全性设计的可追踪性信息模型构建

4.2 基于模型检测的设计缺陷自动查找

4.3 基于模型检测的可追踪性实例分析

4.4 本章小结

第五章 系统安全性设计验证工具的设计与实现

5.1 系统安全性设计验证工具A2STool的设计

5.2 系统安全性设计验证工具A2STool的实现

5.3 机轮刹车系统控制单元的实例分析

5.4 本章小结

第六章 总结与展望

6.1 论文工作总结

6.2 未来工作展望

参考文献

致谢

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

附录TFTA系统安全性设计模型AltaRica模型