基于π-演算的BPEL4WS性质检验
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-7页 |
| 目录 | 第7-11页 |
| 第一章 绪论 | 第11-21页 |
| ·研究背景 | 第11-12页 |
| ·研究现状 | 第12-15页 |
| ·本文的主要工作 | 第15-19页 |
| ·研究内容 | 第15-17页 |
| ·研究难点和技术路线 | 第17-18页 |
| ·创新之处 | 第18-19页 |
| ·本文结构 | 第19-21页 |
| 第二章 模型检验 | 第21-27页 |
| ·简介 | 第21-23页 |
| ·模型检验工具 | 第23-27页 |
| ·基于计算树逻辑的模型检验工具 | 第23-24页 |
| ·基于命题线性时序逻辑的模型检验工具 | 第24-25页 |
| ·基于μ-演算的模型检验工具 | 第25-27页 |
| 第三章 π-演算建模BPEL4WS | 第27-49页 |
| ·π-演算 | 第27-29页 |
| ·π-演算的语法定义 | 第27-28页 |
| ·π-演算的操作语义 | 第28-29页 |
| ·BPEL4WS | 第29-37页 |
| ·建模方法 | 第37-49页 |
| ·外部原子活动的建模 | 第38-40页 |
| ·结构化活动的建模 | 第40-45页 |
| ·关于链接的建模 | 第45-48页 |
| ·其它活动的建模 | 第48-49页 |
| 第四章 μ-演算描述性质 | 第49-55页 |
| ·HML | 第49-50页 |
| ·μ-演算 | 第50-51页 |
| ·检验的一般性质分析 | 第51-52页 |
| ·BPEL4WS检验性质分析 | 第52-54页 |
| ·死锁 | 第52-53页 |
| ·可达性 | 第53-54页 |
| ·小结 | 第54-55页 |
| 第五章 检验工具 | 第55-77页 |
| ·引言 | 第55页 |
| ·BPEL4WS到π-演算的自动建模方法 | 第55-62页 |
| ·无注释信息的自动建模方法 | 第56-59页 |
| ·有注释信息的自动建模方法 | 第59-62页 |
| ·检验算法 | 第62-72页 |
| ·算法的总体思想 | 第62页 |
| ·推理规则 | 第62-70页 |
| ·算法及其改进 | 第70-72页 |
| ·出错路径标识 | 第72-77页 |
| ·在π-演算表达式上匹配出错路径 | 第72-74页 |
| ·标识到BPEL4WS文件 | 第74-77页 |
| 第六章 使用π-演算检验BPEL4WS的实例 | 第77-84页 |
| ·建模 | 第78-79页 |
| ·性质分析 | 第79-80页 |
| ·检验 | 第80-81页 |
| ·改进 | 第81-82页 |
| ·检验 | 第82页 |
| ·小结 | 第82-84页 |
| 第七章 结束语 | 第84-87页 |
| ·本文的主要贡献 | 第84-85页 |
| ·未来的工作 | 第85-87页 |
| 参考文献 | 第87-93页 |
| 附录1 银行贷款BPEL4WS文件一 | 第93-96页 |
| 附录2 银行贷款BPEL4WS文件一出错路径标识 | 第96-100页 |
| 附录3 银行贷款BPEL4WS文件二 | 第100-103页 |
| 附录4 攻读硕士期间发表的学术论文 | 第103-104页 |
| 附录5 致谢 | 第104-105页 |
