| 摘要 | 第1-5页 |
| ABSTRACT | 第5-12页 |
| 第一章 绪论 | 第12-18页 |
| ·课题研究背景 | 第12-14页 |
| ·国内外研究现状及选题依据 | 第14-16页 |
| ·国内外研究现状 | 第14-16页 |
| ·选题依据 | 第16页 |
| ·论文组织结构 | 第16-18页 |
| 第二章 面向Alta Rica模型的系统安全性设计验证方法 | 第18-29页 |
| ·系统安全性设计AltaRica模型 | 第18-23页 |
| ·系统安全性设计AltaRica语言 | 第18-20页 |
| ·系统安全性设计AltaRica模型构建 | 第20-23页 |
| ·形式化方法和模型检测 | 第23-27页 |
| ·形式化方法 | 第23-24页 |
| ·模型检测方法和工具 | 第24-26页 |
| ·面向模型检测的可追踪性 | 第26-27页 |
| ·面向AltaRica模型的系统安全性设计验证框架 | 第27-28页 |
| ·本章小结 | 第28-29页 |
| 第三章 基于SPIN的AltaRica模型转换与安全性验证 | 第29-42页 |
| ·Alta Rica模型和Promela模型的语义 | 第29-33页 |
| ·接口转换系统的语义描述 | 第29-30页 |
| ·基于接口转换系统的AltaRica模型语义描述 | 第30-32页 |
| ·基于接口转换系统的Promela模型语义描述 | 第32-33页 |
| ·Alta Rica模型到Promela模型的转换 | 第33-39页 |
| ·AltaRica模型到Promela模型的转换规则 | 第33-37页 |
| ·AltaRica模型和Promela模型语义等价性证明 | 第37-39页 |
| ·基于SPIN的AltaRica模型安全性验证 | 第39-41页 |
| ·基于线性时序逻辑的安全性需求规约 | 第39-40页 |
| ·基于SPIN的AltaRica模型安全性验证 | 第40-41页 |
| ·本章小结 | 第41-42页 |
| 第四章 系统安全性设计的可追踪性 | 第42-53页 |
| ·面向系统安全性设计的可追踪性信息模型构建 | 第42-46页 |
| ·可追踪性信息模型的元模型 | 第42-43页 |
| ·可追踪性信息模型的构建 | 第43-46页 |
| ·基于模型检测的设计缺陷自动查找 | 第46-49页 |
| ·模型检测验证结果文件的处理 | 第46-48页 |
| ·基于可追踪性信息模型的设计缺陷查找 | 第48-49页 |
| ·基于模型检测的可追踪性实例分析 | 第49-52页 |
| ·本章小结 | 第52-53页 |
| 第五章 系统安全性设计验证工具的设计与实现 | 第53-65页 |
| ·系统安全性设计验证工具A2STool的设计 | 第53-56页 |
| ·原型工具设计框架 | 第53-55页 |
| ·原型工具处理流程 | 第55-56页 |
| ·系统安全性设计验证工具A2STool的实现 | 第56-59页 |
| ·AltaRica模型语法检查 | 第56-57页 |
| ·模型转换与验证 | 第57-59页 |
| ·机轮刹车系统控制单元的实例分析 | 第59-64页 |
| ·机轮刹车系统控制单元描述 | 第59-60页 |
| ·机轮刹车系统控制单元AltaRica模型构建 | 第60-61页 |
| ·机轮刹车系统控制单元的安全性验证 | 第61-64页 |
| ·本章小结 | 第64-65页 |
| 第六章 总结与展望 | 第65-67页 |
| ·论文工作总结 | 第65-66页 |
| ·未来工作展望 | 第66-67页 |
| 参考文献 | 第67-72页 |
| 致谢 | 第72-73页 |
| 在学期间的研究成果及发表的学术论文 | 第73-74页 |
| 附录 TFTA系统安全性设计模型AltaRica模型 | 第74-75页 |
