| 摘要 | 第1-5页 |
| ABSTRACT | 第5-12页 |
| 缩略词 | 第12-13页 |
| 第一章 绪论 | 第13-18页 |
| ·课题研究背景及意义 | 第13-14页 |
| ·当前研究现状 | 第14-15页 |
| ·论文研究内容与论文结构 | 第15-18页 |
| 第二章 基于模型的系统安全性分析概述 | 第18-29页 |
| ·模型驱动系统工程 | 第18-21页 |
| ·系统工程概述 | 第18-19页 |
| ·模型驱动工程 | 第19-21页 |
| ·传统的安全性分析方法 | 第21-24页 |
| ·故障树分析方法 | 第21-23页 |
| ·故障模式及影响分析方法 | 第23-24页 |
| ·基于模型的系统安全性分析 | 第24-27页 |
| ·面向需求的四变量模型 | 第25页 |
| ·面向设计的AltaRica模型 | 第25-27页 |
| ·从需求分析到模型设计的系统安全性分析验证框架 | 第27-28页 |
| ·本章小结 | 第28-29页 |
| 第三章 基于四变量模型的系统需求建模 | 第29-42页 |
| ·四变量模型概述 | 第29-32页 |
| ·关系REQ与关系NAT | 第29-31页 |
| ·关系IN与关系OUT | 第31-32页 |
| ·需求层面的软件行为定义 | 第32页 |
| ·SCR方法及形式化语义 | 第32-38页 |
| ·SCR基本结构 | 第33页 |
| ·基于SCR方法的实例分析 | 第33-34页 |
| ·SCR方法形式化语义 | 第34-38页 |
| ·四变量模型需求分析实例 | 第38-41页 |
| ·机轮刹车系统中的隔离阀建模 | 第39-40页 |
| ·机轮刹车系统中的选择阀建模 | 第40-41页 |
| ·本章小结 | 第41-42页 |
| 第四章 面向ALTARICA的模型转换与系统设计建模 | 第42-54页 |
| ·AltaRica模型的形式化定义 | 第42-44页 |
| ·四变量模型与AltaRica模型的语义映射 | 第44-50页 |
| ·MV和CV与AltaRica之间的映射 | 第44-46页 |
| ·IV和OV与AltaRica之间的映射 | 第46-48页 |
| ·关系NAT与AltaRica之间的映射 | 第48页 |
| ·关系REQ与AltaRica之间的映射 | 第48-49页 |
| ·关系IN和OUT与AltaRica之间的映射 | 第49-50页 |
| ·四变量模型与AltaRica模型之间的映射框架 | 第50页 |
| ·模型转换实例分析 | 第50-53页 |
| ·隔离阀的AltaRica模型设计 | 第51-52页 |
| ·选择阀的AltaRica模型设计 | 第52-53页 |
| ·本章小结 | 第53-54页 |
| 第五章 机轮刹车系统实例建模与安全性分析验证 | 第54-71页 |
| ·机轮刹车系统(WBS)概述 | 第54-57页 |
| ·刹车系统控制单元(BSCU) | 第55-56页 |
| ·WBS系统中的部件蓄压阀 | 第56页 |
| ·WBS系统中的部件限量阀 | 第56-57页 |
| ·WBS系统需求的四变量模型分析 | 第57-59页 |
| ·BSCU子系统的四变量模型 | 第57-58页 |
| ·蓄压阀的四变量模型 | 第58页 |
| ·限量阀的四变量模型 | 第58-59页 |
| ·WBS系统的四变量模型 | 第59页 |
| ·WBS系统的SCR表设计 | 第59-62页 |
| ·WBS系统的模式转换表构造 | 第59-60页 |
| ·WBS系统的事件表构造 | 第60-61页 |
| ·WBS系统的条件表构造 | 第61-62页 |
| ·WBS系统的AltaRica设计模型 | 第62-66页 |
| ·BSCU子系统的AltaRica模型 | 第63页 |
| ·蓄压阀的AltaRica模型 | 第63-64页 |
| ·限量阀的AltaRica模型 | 第64-65页 |
| ·WBS系统的AltaRica模型 | 第65-66页 |
| ·WBS系统安全性分析与验证 | 第66-69页 |
| ·构建故障树 | 第66-67页 |
| ·安全性属性总结及验证 | 第67-69页 |
| ·本章小节 | 第69-71页 |
| 第六章 总结与展望 | 第71-73页 |
| ·总结 | 第71-72页 |
| ·展望 | 第72-73页 |
| 参考文献 | 第73-78页 |
| 致谢 | 第78-79页 |
| 在学期间的研究成果及发表的学术论文 | 第79页 |