面向对象MSVL语言及其在组合Web服务验证中的应用
| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| 第一章 绪论 | 第11-21页 |
| ·研究背景与意义 | 第11-12页 |
| ·时序逻辑程序设计语言 | 第12-16页 |
| ·XYZ/E | 第13-14页 |
| ·Tempura | 第14页 |
| ·MSVL | 第14-15页 |
| ·其它语言 | 第15-16页 |
| ·组合Web 服务的形式化验证 | 第16-17页 |
| ·论文的主要工作与组织结构 | 第17-21页 |
| 第二章 框架时序逻辑语言MSVL | 第21-39页 |
| ·相关研究 | 第21-23页 |
| ·XYZ/E | 第21-22页 |
| ·Tempura | 第22-23页 |
| ·投影时序逻辑 | 第23-26页 |
| ·语法 | 第24页 |
| ·语义 | 第24-26页 |
| ·MSVL | 第26-29页 |
| ·语法 | 第26-28页 |
| ·语义 | 第28-29页 |
| ·MSVL解释器 | 第29-33页 |
| ·应用实例 | 第33-37页 |
| ·小结 | 第37-39页 |
| 第三章 MSVL 的指针 | 第39-57页 |
| ·指针与形式化方法 | 第39-41页 |
| ·时序逻辑语言的指针 | 第41-43页 |
| ·XYZ/E的指针 | 第42-43页 |
| ·Tempura的指针 | 第43页 |
| ·基于名字常量的指针 | 第43-47页 |
| ·形式化定义 | 第44-45页 |
| ·实现方案 | 第45-47页 |
| ·基于内容变量的指针 | 第47-50页 |
| ·形式化定义 | 第47-49页 |
| ·实现方案 | 第49-50页 |
| ·应用实例 | 第50-54页 |
| ·小结 | 第54-57页 |
| 第四章 面向对象MSVL | 第57-85页 |
| ·面向对象方法与形式化方法 | 第57-59页 |
| ·XYZ/E的面向对象特征 | 第59-61页 |
| ·面向对象MSVL | 第61-69页 |
| ·扩展投影时序逻辑 | 第61-64页 |
| ·基本语句 | 第64-69页 |
| ·面向对象MSVL的解释器 | 第69-79页 |
| ·基本框架 | 第69-74页 |
| ·实现方案 | 第74-79页 |
| ·应用实例 | 第79-83页 |
| ·小结 | 第83-85页 |
| 第五章 组合Web 服务的形式化验证 | 第85-107页 |
| ·Web 服务与OWL-S | 第86-89页 |
| ·组合Web 服务的形式化验证 | 第89-93页 |
| ·基于面向对象MSVL的OWL-S建模与验证 | 第93-97页 |
| ·建模方法 | 第93-96页 |
| ·验证方法 | 第96-97页 |
| ·建模与验证实例 | 第97-105页 |
| ·小结 | 第105-107页 |
| 第六章 总结与展望 | 第107-111页 |
| ·论文总结 | 第107-108页 |
| ·进一步的研究 | 第108-111页 |
| 致谢 | 第111-113页 |
| 参考文献 | 第113-122页 |
| 博士在读期间的研究成果 | 第122-123页 |
| 博士在读期间参加的科研项目 | 第123-124页 |
| 附录A 面向对象MSVL 的Bison 产生式 | 第124-129页 |
| 附录B 面向对象MSVL 程序正则形的存在性 | 第129-135页 |
