一种扩展的并发传值进程抽象模型
| 摘要 | 第1-7页 |
| Abstract | 第7-9页 |
| 目录 | 第9-17页 |
| 第一章 引言 | 第17-21页 |
| ·研究背景 | 第17-18页 |
| ·论文主要工作 | 第18-19页 |
| ·论文的组织 | 第19-21页 |
| 第二章 形式化方法和并发传值系统 | 第21-27页 |
| ·形式化方法 | 第21-22页 |
| ·并发系统 | 第22页 |
| ·并发系统描述语言 | 第22-23页 |
| ·模型检测 | 第23-27页 |
| 第三章 STGA的一种扩展-STGA~2 | 第27-49页 |
| ·纯CCS和传值CCS | 第27-29页 |
| ·传值CCS符号 | 第28-29页 |
| ·传值CCS语法 | 第29页 |
| ·符号迁移图 | 第29-30页 |
| ·带赋值的符号迁移图 | 第30-33页 |
| ·带双赋值的符号迁移图-STGA~2 | 第33-36页 |
| ·STGA~2的基本定义 | 第36-49页 |
| ·赋值与动作 | 第36-37页 |
| ·STGA~2的定义 | 第37页 |
| ·STGA~2的生成规则 | 第37-39页 |
| ·STGA~2图的并发合成 | 第39-41页 |
| ·STGA~2的操作语义 | 第41-43页 |
| ·互模拟 | 第43-44页 |
| ·消除“void”动作 | 第44-49页 |
| 第四章 其它STGA的相关工作 | 第49-53页 |
| ·加后赋值的STG | 第49-50页 |
| ·后赋值的STGA—STGA′ | 第50-51页 |
| ·STGLA | 第51-53页 |
| 第五章 STGA~2工具实现 | 第53-61页 |
| ·μ演算 | 第53-57页 |
| ·模态逻辑 | 第53-54页 |
| ·时序逻辑 | 第54-56页 |
| ·命题μ演算 | 第56页 |
| ·谓词μ演算 | 第56-57页 |
| ·工具的结构与实现 | 第57-61页 |
| 第六章 检测实例与数据结果 | 第61-67页 |
| ·实例说明 | 第61-64页 |
| ·数据缓冲器 | 第61页 |
| ·交错位协议 | 第61页 |
| ·CIM协议 | 第61-62页 |
| ·TMR协议 | 第62-64页 |
| ·实测结果 | 第64-67页 |
| 第七章 结束语 | 第67-69页 |
| 附录A 互模拟、模型检测脚本 | 第69-75页 |
| A.1 Bag3 | 第69-70页 |
| A.2 ABP协议 | 第70-71页 |
| A.3 CIM | 第71-72页 |
| A.4 TMR | 第72-75页 |
| 附录B 程序源码 | 第75-79页 |
| 参考文献 | 第79-83页 |
| 发表文章目录 | 第83-85页 |
| 致谢 | 第85页 |
