测试目的引导的模型检测方法与技术研究

摘要	第1-4页
Abstract	第4-8页
引言	第8-9页
1 绪论	第9-11页
·研究现状	第9-10页
·课题研究内容和方法	第10页
·论文组织结构	第10-11页
2 相关理论和技术介绍	第11-17页
·服务组合描述语言BPEL	第11页
·形式化描述语言LOTOS	第11-12页
·命题μ-演算	第12-13页
·模型检测技术	第13-15页
·模型检测工具集CADP	第15-16页
·测试目的引导的模型检测方法	第16-17页
3 BPEL到LOTOS自动转换工具的设计与实现	第17-23页
·BPEL到LOTOS的自动转换工具的设计	第17-20页
·BPEL到LOTOS的自动转换工具的实现	第20-23页
4 μ-演算编辑器的设计与实现	第23-42页
·μ-演算词法分析器设计与实现	第23-25页
·词法分析器的设计	第23-24页
·词法分析器的实现	第24-25页
·μ-演算语法分析器的设计与实现	第25-41页
·μ-演算文法的二义性证明	第25-26页
·构造LR(0)项目集规范族	第26-31页
·构造LR分析表	第31-37页
·语法分析器的实现	第37-41页
·μ-演算编辑器的实现	第41-42页
5 测试目的引导模型检测方法的实现	第42-45页
6 案例分析	第45-56页
·八皇后算法检测	第45-49页
·背包算法检测	第49-52页
·哲学家算法检测	第52-56页
7 案例评估	第56-58页
结论	第58-59页
参考文献	第59-62页
申请学位期间的研究成果及发表的学术论文	第62-63页
致谢	第63页