| 论文摘要 | 第1-9页 |
| ABSTRACT | 第9-16页 |
| 第一章 绪论 | 第16-26页 |
| ·研究背景 | 第16-19页 |
| ·国内外研究现状 | 第19-21页 |
| ·本文研究内容 | 第21-24页 |
| ·本文组织结构 | 第24-26页 |
| 第二章 相关技术概述 | 第26-34页 |
| ·UML 2.0 | 第26-29页 |
| ·UML概述 | 第26-27页 |
| ·UML状态图 | 第27-28页 |
| ·UML顺序图 | 第28-29页 |
| ·形式化方法 | 第29-32页 |
| ·形式化方法概述 | 第29-31页 |
| ·基于LTS结构的pi演算 | 第31-32页 |
| ·概率模型检测 | 第32页 |
| ·XMI概述 | 第32-34页 |
| 第三章 UML状态图的LTS操作语义 | 第34-52页 |
| ·引言 | 第34-36页 |
| ·研究背景 | 第34-35页 |
| ·相关工作 | 第35-36页 |
| ·UML状态图的组装机制及其LTS操作语义 | 第36-41页 |
| ·顺序组装和无触发组装 | 第36-37页 |
| ·选择组装 | 第37-38页 |
| ·分叉组装和汇聚组装 | 第38-40页 |
| ·并行组装和复制组装 | 第40-41页 |
| ·UML状态图的LTS形式语义生成算法 | 第41-46页 |
| ·关键XMI标签及其数据结构 | 第41-44页 |
| ·算法描述 | 第44-46页 |
| ·UML状态图在模型精化中的语义等价自动证明 | 第46-49页 |
| ·小结 | 第49-52页 |
| 第四章 UML序列图的操作语义及在模型精化一致性检查 | 第52-76页 |
| ·引言 | 第52-54页 |
| ·研究背景 | 第52-53页 |
| ·相关工作 | 第53-54页 |
| ·UML序列图的操作语义 | 第54-60页 |
| ·消息的异步发送 | 第54-55页 |
| ·消息的同步发送和内部消息 | 第55-56页 |
| ·分支组合片段 | 第56-57页 |
| ·循环组合片段 | 第57-58页 |
| ·中断组合片段 | 第58-59页 |
| ·并发组合片段 | 第59-60页 |
| ·其它 | 第60页 |
| ·UML序列图的LTS操作语义生成算法 | 第60-68页 |
| ·关键XMI标签及其数据结构 | 第60-65页 |
| ·算法描述 | 第65-68页 |
| ·UML状态图和序列图的一致性检查 | 第68-74页 |
| ·电话系统的UML序列图模型及其pi演算转换 | 第68-69页 |
| ·电话系统的UML状态图模型及其pi演算转换 | 第69-71页 |
| ·进程代数工具的自动验证 | 第71页 |
| ·系统死锁性的手动推导及其时间复杂度 | 第71-73页 |
| ·UML子图间的语义一致性手动推导及时间复杂度 | 第73-74页 |
| ·小结 | 第74-76页 |
| 第五章 基于概率模型检测的扩展UML状态图量化分析 | 第76-104页 |
| ·引言 | 第76-79页 |
| ·研究背景 | 第76-77页 |
| ·相关工作 | 第77-78页 |
| ·概率/随机Kripke结构的形式化定义 | 第78-79页 |
| ·扩展UML状态图的概率/随机Kripke结构语义 | 第79-87页 |
| ·系统初始化和状态标签 | 第79-80页 |
| ·状态顺序迁移 | 第80-82页 |
| ·状态内部迁移 | 第82页 |
| ·状态的选择迁移 | 第82-85页 |
| ·模块声明和模块重命名 | 第85-86页 |
| ·同步并发组合和异步并发组合 | 第86-87页 |
| ·概率/随机Kripke形式语义生成算法 | 第87-92页 |
| ·关键XMI标签及其数据结构 | 第87-90页 |
| ·算法描述 | 第90-92页 |
| ·基于概率Kripke结构的模型量化分析 | 第92-97页 |
| ·UML状态图的概率Kripke结构语义 | 第92-94页 |
| ·系统关键属性的PCTL描述和自动验证 | 第94-97页 |
| ·基于随机Kripke结构的系统性能分析 | 第97-102页 |
| ·排队网络的CTMC形式语义 | 第97-98页 |
| ·关键系统属性的自动推导和证明 | 第98-100页 |
| ·关键系统属性的手动推导和分析 | 第100-102页 |
| ·小结 | 第102-104页 |
| 第六章 软件原型工具的设计与实现 | 第104-110页 |
| ·UML形式语义转换器的体系架构 | 第104-105页 |
| ·UML形式语义转换器的设计与实现 | 第105-109页 |
| ·软件原型工具的设计原则 | 第105-106页 |
| ·算法和数据结构 | 第106-108页 |
| ·软件原型工具的运行和使用 | 第108-109页 |
| ·小结 | 第109-110页 |
| 第七章 结束语 | 第110-113页 |
| ·本文的主要贡献 | 第110-111页 |
| ·下一步研究工作 | 第111-113页 |
| 参考文献 | 第113-121页 |
| 作者在攻读博士学位期间发表的论文 | 第121-122页 |
| 作者在攻读博士学位期间取得的其它成果 | 第122-123页 |
| 致谢 | 第123-124页 |
