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

发布时间：2017-04-03 21:18

  本文关键词：面向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模型和安全性需求的线性时序逻辑规约进行验证和分析,接着基于验证结果结合可追踪性信息模型发现系统安全性设计缺陷。说明了本文方法的有效性和可行性,为系统的安全性分析提供了一种新思路。
【关键词】：系统安全性设计 AltaRica模型 线性时序逻辑 可追踪性信息模型 模型检测
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2016
【分类号】：V227;TP368.1
【目录】：

• 摘要4-5
• ABSTRACT5-12
• 第一章 绪论12-18
• 1.1 课题研究背景12-14
• 1.2 国内外研究现状及选题依据14-16
• 1.2.1 国内外研究现状14-16
• 1.2.2 选题依据16
• 1.3 论文组织结构16-18
• 第二章 面向Alta Rica模型的系统安全性设计验证方法18-29
• 2.1 系统安全性设计AltaRica模型18-23
• 2.1.1 系统安全性设计AltaRica语言18-20
• 2.1.2 系统安全性设计AltaRica模型构建20-23
• 2.2 形式化方法和模型检测23-27
• 2.2.1 形式化方法23-24
• 2.2.2 模型检测方法和工具24-26
• 2.2.3 面向模型检测的可追踪性26-27
• 2.3 面向AltaRica模型的系统安全性设计验证框架27-28
• 2.4 本章小结28-29
• 第三章 基于SPIN的AltaRica模型转换与安全性验证29-42
• 3.1 Alta Rica模型和Promela模型的语义29-33
• 3.1.1 接口转换系统的语义描述29-30
• 3.1.2 基于接口转换系统的AltaRica模型语义描述30-32
• 3.1.3 基于接口转换系统的Promela模型语义描述32-33
• 3.2 Alta Rica模型到Promela模型的转换33-39
• 3.2.1 AltaRica模型到Promela模型的转换规则33-37
• 3.2.2 AltaRica模型和Promela模型语义等价性证明37-39
• 3.3 基于SPIN的AltaRica模型安全性验证39-41
• 3.3.1 基于线性时序逻辑的安全性需求规约39-40
• 3.3.2 基于SPIN的AltaRica模型安全性验证40-41
• 3.4 本章小结41-42
• 第四章 系统安全性设计的可追踪性42-53
• 4.1 面向系统安全性设计的可追踪性信息模型构建42-46
• 4.1.1 可追踪性信息模型的元模型42-43
• 4.1.2 可追踪性信息模型的构建43-46
• 4.2 基于模型检测的设计缺陷自动查找46-49
• 4.2.1 模型检测验证结果文件的处理46-48
• 4.2.2 基于可追踪性信息模型的设计缺陷查找48-49
• 4.3 基于模型检测的可追踪性实例分析49-52
• 4.4 本章小结52-53
• 第五章 系统安全性设计验证工具的设计与实现53-65
• 5.1 系统安全性设计验证工具A2STool的设计53-56
• 5.1.1 原型工具设计框架53-55
• 5.1.2 原型工具处理流程55-56
• 5.2 系统安全性设计验证工具A2STool的实现56-59
• 5.2.1 AltaRica模型语法检查56-57
• 5.2.2 模型转换与验证57-59
• 5.3 机轮刹车系统控制单元的实例分析59-64
• 5.3.1 机轮刹车系统控制单元描述59-60
• 5.3.2 机轮刹车系统控制单元AltaRica模型构建60-61
• 5.3.3 机轮刹车系统控制单元的安全性验证61-64
• 5.4 本章小结64-65
• 第六章 总结与展望65-67
• 6.1 论文工作总结65-66
• 6.2 未来工作展望66-67
• 参考文献67-72
• 致谢72-73
• 在学期间的研究成果及发表的学术论文73-74
• 附录 TFTA系统安全性设计模型AltaRica模型74-75

  本文关键词：面向AltaRica模型的系统安全性设计验证方法研究，由笔耕文化传播整理发布。

，

本文编号：284994