复杂信息系统模型的形式化验证方法研究
| 摘要 | 第1-7页 |
| Abstract | 第7-13页 |
| 第1章 绪论 | 第13-29页 |
| ·研究背景及意义 | 第13-14页 |
| ·研究现状 | 第14-25页 |
| ·形式化方法 | 第14-15页 |
| ·形式化规约技术 | 第15-19页 |
| ·软件验证方法 | 第19-24页 |
| ·复杂信息系统行为建模与验证 | 第24-25页 |
| ·论文的研究内容 | 第25-27页 |
| ·论文的组织结构 | 第27-29页 |
| 第2章 顶层需求形式化验证方法研究 | 第29-53页 |
| ·引言 | 第29页 |
| ·相关工作 | 第29-30页 |
| ·顶层需求抽象建模 | 第30-33页 |
| ·面向行为抽象 | 第30-31页 |
| ·面向行为建模 | 第31-33页 |
| ·顶层需求模型的 RSL 规约 | 第33-36页 |
| ·RSL 的基本语法结构 | 第33-34页 |
| ·面向模型的规约 | 第34-35页 |
| ·面向性质的规约 | 第35-36页 |
| ·顶层需求模型检测方法 | 第36-45页 |
| ·顶层需求模型检测过程 | 第37页 |
| ·Promela 语言 | 第37-38页 |
| ·顶层需求模型到 Promela 的转换 | 第38-45页 |
| ·实例分析 | 第45-52页 |
| ·验证实例 | 第45页 |
| ·抽象建模 | 第45-49页 |
| ·生成 Promela 模型 | 第49-51页 |
| ·验证分析 | 第51-52页 |
| ·本章小结 | 第52-53页 |
| 第3章 技术层面需求形式化验证研究 | 第53-74页 |
| ·引言 | 第53页 |
| ·相关工作 | 第53-54页 |
| ·UML 顺序图 | 第54-61页 |
| ·UML 顺序图的形式化描述 | 第55页 |
| ·UML 顺序图的操作语义 | 第55-57页 |
| ·UML 顺序图的 XMI 文档 | 第57-61页 |
| ·UML 顺序图的形式化验证 | 第61-67页 |
| ·形式化验证过程 | 第61-62页 |
| ·顺序图 XMI 文档解析算法 | 第62-64页 |
| ·顺序图模型到 Promela 程序的语义转换 | 第64-67页 |
| ·实例分析 | 第67-73页 |
| ·验证实例 | 第67-69页 |
| ·生成 Promela 模型 | 第69-70页 |
| ·执行模拟 | 第70-71页 |
| ·关键性质验证 | 第71-73页 |
| ·本章小结 | 第73-74页 |
| 第4章 设计模型形式化验证方法研究 | 第74-103页 |
| ·引言 | 第74页 |
| ·相关工作 | 第74-75页 |
| ·基于符号模型检测的验证过程 | 第75-78页 |
| ·形式化验证过程 | 第75-76页 |
| ·NuSMV 建模语言 | 第76-78页 |
| ·NuSMV 验证性质描述与分类 | 第78页 |
| ·UML 状态图 | 第78-85页 |
| ·状态图的形式化描述 | 第80-82页 |
| ·状态图的操作语义 | 第82-83页 |
| ·关键 XMI 标签及数据解析算法 | 第83-85页 |
| ·设计模型到 NuSMV 模型的转换 | 第85-94页 |
| ·到 NuSMV 模块结构的转换 | 第86页 |
| ·到 NuSMV 变量声明的转换 | 第86-88页 |
| ·到 NuSMV 赋值声明的转换 | 第88-93页 |
| ·转换过程正确性证明 | 第93-94页 |
| ·实例分析 | 第94-102页 |
| ·验证实例 | 第94-98页 |
| ·生成 NuSMV 输入模型 | 第98-100页 |
| ·关键性质验证 | 第100-102页 |
| ·本章小结 | 第102-103页 |
| 第5章 实时性能分析方法研究 | 第103-117页 |
| ·引言 | 第103页 |
| ·相关工作 | 第103-104页 |
| ·基于实时模型检测的性能分析 | 第104-109页 |
| ·性能分析过程 | 第104-105页 |
| ·UPPAAL 中的时间自动机定义 | 第105-106页 |
| ·UPPAAL 的需求规范语言 | 第106-107页 |
| ·UML 协作图的实时扩展 | 第107-109页 |
| ·基于事件顺序分析性能 | 第109-110页 |
| ·基于实时协作图的时间自动机建模 | 第110-114页 |
| ·建模时间自动机进程 | 第111页 |
| ·建模协作图子系统的时间自动机 | 第111-114页 |
| ·建模实时系统调度过程 | 第114页 |
| ·验证分析 | 第114-115页 |
| ·本章小结 | 第115-117页 |
| 结论 | 第117-119页 |
| 参考文献 | 第119-129页 |
| 攻读博士学位期间发表的论文和取得的科研成果 | 第129-131页 |
| 致谢 | 第131页 |
