| 摘要 | 第6-8页 |
| ABSTRACT | 第8-9页 |
| 第一章 绪论 | 第13-19页 |
| 1.1 关键问题及研究现状概述 | 第15-17页 |
| 1.2 本文的组织结构 | 第17-19页 |
| 第二章 数据精化及并发系统的精化 | 第19-27页 |
| 2.1 数据精化 | 第19-24页 |
| 2.2 并发系统的精化 | 第24-27页 |
| 第三章 情景化多智能体系统逐步精化 | 第27-50页 |
| 3.1 逐步精化，Object-Z和活动系统简介 | 第28-31页 |
| 3.2 情景化多智能体系统的叠加精化 | 第31-39页 |
| 3.2.1 SMAS的建模及叠加精化 | 第31-34页 |
| 3.2.2 修复机器人系统示例 | 第34-39页 |
| 3.3 带有时间段谓词的操作精化 | 第39-48页 |
| 3.3.1 带有时间段谓词的模式及其精化 | 第39-42页 |
| 3.3.2 自由飞行协议示例 | 第42-48页 |
| 3.4 小结及相关工作 | 第48-50页 |
| 第四章 软件事务内存实现的精化验证 | 第50-71页 |
| 4.1 TMS1及TL2-RCAD简介 | 第50-59页 |
| 4.1.1 软件事务存储标准TMS1 | 第50-55页 |
| 4.1.2 TL2-RCAD | 第55-59页 |
| 4.2 基于语义交换的TMS1验证 | 第59-69页 |
| 4.2.1 抽象事务及具体实现的语法及语义 | 第60-63页 |
| 4.2.2 基于语义交换的验证技术 | 第63-69页 |
| 4.3 小结及相关工作 | 第69-71页 |
| 第五章 弱内存模型TSO新操作语义及精化验证 | 第71-90页 |
| 5.1 现有的TSO操作语义及公理语义 | 第71-76页 |
| 5.1.1 现有的TSO操作语义 | 第71-74页 |
| 5.1.2 现有的TSO公理语义 | 第74-75页 |
| 5.1.3 现有语义在精化验证时存在的问题 | 第75-76页 |
| 5.2 新公理语义及基于新公理语义的新操作语义 | 第76-83页 |
| 5.2.1 新公理语义及其正确性、完备性 | 第76-80页 |
| 5.2.2 新操作语义及其正确性、完备性 | 第80-83页 |
| 5.3 编译器优化及局部转换规则的精化验证 | 第83-88页 |
| 5.3.1 TSO上编译器优化规则及局部转换规则 | 第83页 |
| 5.3.2 TSO优化规则及局部转换规则对精化的要求 | 第83-86页 |
| 5.3.3 TSO优化规则及局部转换规则的验证 | 第86-88页 |
| 5.4 小结及相关工作 | 第88-90页 |
| 第六章 TSO并发数据结构的线性化 | 第90-106页 |
| 6.1 写缓存操作语义上线性化定义简介 | 第91-92页 |
| 6.2 SC上线性化定义存在的问题分析 | 第92-94页 |
| 6.2.1 非重叠性的保持 | 第92-93页 |
| 6.2.2 SC上历史的不充分性 | 第93-94页 |
| 6.3 新线性化定义 | 第94-98页 |
| 6.3.1 历史及使用对象系统的语义 | 第94-97页 |
| 6.3.2 TSO上线性化的定义 | 第97-98页 |
| 6.4 线性化与上下文精化的等价 | 第98-102页 |
| 6.4.1 正确性和完备性 | 第98-102页 |
| 6.5 常见原子性的TSO规格说明 | 第102-104页 |
| 6.5.1 TSO上两种原子性表示 | 第102页 |
| 6.5.2 线性化实例 | 第102-104页 |
| 6.6 小结及相关工作 | 第104-106页 |
| 第七章 TSO线性化的模块化验证 | 第106-127页 |
| 7.1 TSO上基于依赖保证的精化验证 | 第106-115页 |
| 7.1.1 使用并发数据结构的程序的语义 | 第107-108页 |
| 7.1.2 TSO上基于依赖保证的模拟 | 第108-115页 |
| 7.2 线性化实例 | 第115-125页 |
| 7.2.1 TSO上循环锁 | 第115-118页 |
| 7.2.2 票循环锁 | 第118-120页 |
| 7.2.3 读-拷贝更新 | 第120-125页 |
| 7.3 小结及相关工作 | 第125-127页 |
| 第八章 结束语 | 第127-130页 |
| 8.1 主要贡献 | 第127-128页 |
| 8.2 将来的工作 | 第128-130页 |
| 参考文献 | 第130-139页 |
| 作者在攻读博士学位期间公开发表的论文 | 第139-140页 |
| 作者在攻读博士学位期间所作的项目 | 第140-141页 |
| 致谢 | 第141-142页 |