带实时的传值与移动系统研究
| 摘要 | 第1-7页 |
| 第一章 引言 | 第7-14页 |
| ·并发系统 | 第7-9页 |
| ·实时系统 | 第9-11页 |
| ·形式化验证 | 第11-12页 |
| ·本文的目标、贡献和组成 | 第12-14页 |
| 第二章 实时传值系统的计算模型 | 第14-19页 |
| ·实时传值系统现状 | 第14-15页 |
| ·时间符号迁移图(TSTG) | 第15-19页 |
| 第三章 实时传值系统上的等价关系 | 第19-40页 |
| ·几种重要的互模拟 | 第19-22页 |
| ·基于等价类划分的判定方法 | 第22-40页 |
| ·域(Region)等价 | 第23-24页 |
| ·时间抽象互模拟的判定方法 | 第24-25页 |
| ·时间互模拟的判定方法 | 第25-28页 |
| ·时间互模拟算法及其正确性证明 | 第28-36页 |
| ·无穷数据域及其他情况的处理 | 第36-40页 |
| 第四章 连续时间的数据表示和操作 | 第40-53页 |
| ·时间区域的表示方法 | 第40-44页 |
| ·DBM | 第41-42页 |
| ·更一般的“区”的表示 | 第42-44页 |
| ·范式化与信息消冗 | 第44-53页 |
| 第五章 实时传值系统上的模型检测 | 第53-86页 |
| ·模型检测简介 | 第53页 |
| ·基本约定 | 第53-55页 |
| ·基于可达性分析的模型检测 | 第55-60页 |
| ·验证工具及实现 | 第60-65页 |
| ·协议验证实例分析-限时重传协议 | 第65-73页 |
| ·文件传输服务 | 第65-69页 |
| ·使用RealM建模和验证 | 第69-73页 |
| ·更一般的模型检测 | 第73-86页 |
| ·一阶谓词实时μ演算 | 第74-76页 |
| ·布尔图 | 第76-79页 |
| ·一个局部算法 | 第79-84页 |
| ·数据无关变量处理 | 第84-86页 |
| 第六章 实时移动进程演算 | 第86-160页 |
| ·移动进程演算简介 | 第86-87页 |
| ·语法和语义 | 第87-101页 |
| ·强实互模拟和强互模拟关系 | 第101-126页 |
| ·弱实互模拟和弱互模拟关系 | 第126-139页 |
| ·公理化 | 第139-160页 |
| ·强实互模拟的公理化 | 第140-145页 |
| ·强互模拟的公理化 | 第145-160页 |
| 第七章 结论 | 第160-163页 |
| ·总结以及相关工作讨论 | 第160-161页 |
| ·进一步工作的讨论 | 第161-163页 |
| 参考文献 | 第163-170页 |
| 攻读博士学位论文期间发表和录用的文章 | 第170-171页 |
| 致谢 | 第171-173页 |
| 附录A RealM接收语言的语法定义 | 第173-177页 |
