传值进程与移动进程的模型检测方法
| 摘要 | 第1-6页 |
| Abstract | 第6-14页 |
| 第一章 引言 | 第14-27页 |
| ·并发系统 | 第14-18页 |
| ·形式化验证方法 | 第18-19页 |
| ·模型检测 | 第19-25页 |
| ·状态爆炸问题 | 第23-24页 |
| ·模型检测工具及应用 | 第24-25页 |
| ·本文的工作和论文的结构 | 第25-27页 |
| 第二章 模型检测的基础 | 第27-38页 |
| ·CCS | 第27-29页 |
| ·基本定义 | 第27页 |
| ·标号迁移系统 | 第27-28页 |
| ·互模拟和弱互模拟 | 第28-29页 |
| ·模态逻辑 | 第29-31页 |
| ·模态算了 | 第29-30页 |
| ·Hennessy-Milner逻辑 | 第30-31页 |
| ·时序逻辑 | 第31-38页 |
| ·格和不动点 | 第31-33页 |
| ·命题模态μ演算 | 第33-36页 |
| ·命题μ演算的模型检测方法 | 第36-38页 |
| ·全局模型检测算法 | 第36页 |
| ·局部的模型检测算法 | 第36-38页 |
| 第三章 传值进程模型和谓词μ演算 | 第38-66页 |
| ·传值CCS及其操作语义 | 第38-42页 |
| ·传值CCS语言 | 第38-40页 |
| ·带赋值的符号迁移图 | 第40-41页 |
| ·STGA的互模拟和弱互模拟 | 第41-42页 |
| ·谓词μ演算 | 第42-46页 |
| ·谓词μ演算的语法 | 第42-43页 |
| ·谓词μ演算的语义 | 第43-46页 |
| ·模态图 | 第46-49页 |
| ·模态图的语法 | 第47页 |
| ·模态图的语义 | 第47-49页 |
| ·嵌套谓词等式系 | 第49-53页 |
| ·嵌套谓词等式系的语法语义 | 第49-51页 |
| ·嵌套谓词等式系的语义刻划 | 第51-53页 |
| ·谓词μ演算公式和模态图的对应关系 | 第53-58页 |
| ·谓词μ演算公式到嵌套谓词等式系的转换算法 | 第53页 |
| ·转换算法的正确性证明 | 第53-56页 |
| ·嵌套谓词等式系的模态图表示 | 第56-58页 |
| ·一个谓词μ演算公式的等式系和模态图表示 | 第58-59页 |
| ·互模拟和谓词μ演算的关系 | 第59-66页 |
| ·弱谓词μ演算 | 第59-61页 |
| ·弱谓词μ演算的语法 | 第59页 |
| ·弱谓词μ演算的语义 | 第59页 |
| ·弱谓词μ演算和谓词μ演算之间的关系 | 第59-61页 |
| ·互模拟和谓词μ演算的关系 | 第61-66页 |
| 第四章 传值进程模型检测及诊断信息生成 | 第66-79页 |
| ·传值进程模型检测算法 | 第66-69页 |
| ·模型检测算法的分析 | 第69-71页 |
| ·诊断信息的生成 | 第71-75页 |
| ·证明图 | 第72-74页 |
| ·示例 | 第74-75页 |
| ·实例分析 | 第75-79页 |
| 第五章 传值进程模型检测的偏序归约方法 | 第79-87页 |
| ·直观的思想 | 第79-80页 |
| ·惰性迁移 | 第80-83页 |
| ·偏序归约模型检测算法 | 第83-87页 |
| 第六章 移动界程的模型检测 | 第87-95页 |
| ·有限控制界程演算 | 第87-90页 |
| ·带不动点的界程逻辑 | 第90-92页 |
| ·界程逻辑的语法 | 第90-92页 |
| ·界程逻辑的语义 | 第92页 |
| ·移动界程的模型检测算法 | 第92-95页 |
| 第七章 移动界程模型检测工具 | 第95-111页 |
| ·界程演算的de Bruijn表示 | 第95-101页 |
| ·de Bruijn变换 | 第96-97页 |
| ·维护函数 | 第97-101页 |
| ·有限控制界程演算的范式表示 | 第101-103页 |
| ·de Bruijn表示下的范式和迁移规则 | 第103-105页 |
| ·模型检测算法的实现 | 第105-106页 |
| ·系统的实现和测试 | 第106-111页 |
| ·系统的结构 | 第107-108页 |
| ·状态空间存取 | 第108页 |
| ·实例分析 | 第108-111页 |
| 第八章 结论 | 第111-116页 |
| ·总结及相关工作的讨论 | 第111-114页 |
| ·命题μ演算和谓词μ演算的相关工作 | 第112页 |
| ·诊断信息生成方面的相关工作 | 第112-113页 |
| ·在偏序归约方法方面 | 第113-114页 |
| ·在移动界程的模型检测工具方面 | 第114页 |
| ·进一步的工作 | 第114-116页 |
| 参考文献 | 第116-122页 |
| 附录A ABP的输入检测文本 | 第122-125页 |
| 附录B FireWall的输入检测文本 | 第125-127页 |
| 个人简历、在学期间的研究成果及发表的论文 | 第127-128页 |
| 致谢及声明 | 第128-130页 |
