组合式Petri网对PI演算的转换与验证
| 提要 | 第1-8页 |
| 第1章 绪论 | 第8-11页 |
| ·背景简介 | 第8-9页 |
| ·本文主要工作 | 第9页 |
| ·论文组织结构 | 第9-10页 |
| 本章小结 | 第10-11页 |
| 第2章 相关基础理论概述 | 第11-15页 |
| ·Petri 网介绍 | 第11-12页 |
| ·Petri 网图形及代数定义 | 第11-12页 |
| ·激发规则 | 第12页 |
| ·PI 演算介绍 | 第12-14页 |
| ·基本定义 | 第12-13页 |
| ·操作语法 | 第13-14页 |
| 本章小结 | 第14-15页 |
| 第3章 PI 演算转换为Petri 网的一般方法 | 第15-24页 |
| ·基于上下文的 PI 演算表达方法 | 第15-17页 |
| ·扩展的 Petri 网-rp 网 | 第17-23页 |
| ·rp 网定义 | 第17-19页 |
| ·基本动作的rp 网形式 | 第19-20页 |
| ·组合方式 | 第20-22页 |
| ·完整转换方法 | 第22-23页 |
| ·变迁规则 | 第23页 |
| 本章小结 | 第23-24页 |
| 第4章 PI 演算递归结构转换 | 第24-37页 |
| ·准备与讨论 | 第25-31页 |
| ·对表达式的解析 | 第25-26页 |
| ·追踪与层次记录 | 第26-27页 |
| ·定值选择判断 | 第27-29页 |
| ·信息保存与返回 | 第29-31页 |
| ·rp’-网 | 第31-32页 |
| ·将 PI 演算递归结构转换成rp’-网 | 第32页 |
| ·初始化标记 | 第32-33页 |
| ·其他 PI 演算自递归形式的讨论 | 第33-36页 |
| 本章小结 | 第36-37页 |
| 第5章 验 证 | 第37-49页 |
| ·验证用例 | 第37页 |
| ·验证工具 | 第37页 |
| ·验证设计 | 第37-41页 |
| ·托肯设计 | 第37-38页 |
| ·输入数据与收集结果 | 第38页 |
| ·条件库所及相连弧的替换 | 第38-39页 |
| ·栈库所 | 第39页 |
| ·追踪托肯的修改 | 第39-40页 |
| ·其他部分的修改 | 第40页 |
| ·全景图 | 第40-41页 |
| ·验证的正确性标准 | 第41页 |
| ·验证过程 | 第41-48页 |
| 本章小结 | 第48-49页 |
| 第6章 结语 | 第49-51页 |
| ·本文工作总结 | 第49-50页 |
| ·未来工作展望 | 第50-51页 |
| 参考文献 | 第51-54页 |
| 致谢 | 第54-55页 |
| 摘要 | 第55-57页 |
| Abstract | 第57-59页 |
