可信普适服务的形式化分析与验证
| 摘要 | 第1-5页 |
| ABSTRACT | 第5-8页 |
| 目录 | 第8-13页 |
| 表格索引 | 第13-14页 |
| 插图索引 | 第14-16页 |
| 第一章 引言 | 第16-33页 |
| ·研究背景 | 第16-17页 |
| ·普适计算 | 第16页 |
| ·面向服务计算 | 第16-17页 |
| ·可信普适服务的构建 | 第17页 |
| ·研究目标与方案 | 第17-23页 |
| ·研究目标 | 第17-18页 |
| ·研究方案 | 第18-23页 |
| ·相关研究工作 | 第23-30页 |
| ·普适计算的研究现状 | 第23-24页 |
| ·面向服务计算研究现状 | 第24-26页 |
| ·可信普适服务的构建及验证 | 第26-30页 |
| ·本文主要工作及贡献 | 第30-31页 |
| ·本文结构 | 第31-32页 |
| ·本章小结 | 第32-33页 |
| 第二章 普适服务的形式化模型 | 第33-50页 |
| ·普适计算环境 | 第33-34页 |
| ·设备模型 | 第34-36页 |
| ·普适服务模型 | 第36-39页 |
| ·类型和效果系统 | 第39-43页 |
| ·程序分析和类型系统 | 第39-40页 |
| ·类型和效果系统技术 | 第40-43页 |
| ·进程演算及模型检验 | 第43-47页 |
| ·进程演算 | 第43-45页 |
| ·模型检验 | 第45-47页 |
| ·动态更新技术 | 第47-49页 |
| ·本章小结 | 第49-50页 |
| 第三章 基于行为一致的普适服务替换 | 第50-74页 |
| ·服务抽象模型 | 第50-52页 |
| ·形式化语言 | 第52-56页 |
| ·语法 | 第53页 |
| ·操作语义 | 第53-56页 |
| ·典型的场景 | 第56-58页 |
| ·并发行为表达式 | 第58-60页 |
| ·语法 | 第58-59页 |
| ·指称语义 | 第59-60页 |
| ·类型系统 | 第60-67页 |
| ·类型和效果系统技术 | 第60-63页 |
| ·基于类型的可替换性 | 第63页 |
| ·行为效果 | 第63-64页 |
| ·行为一致性 | 第64-66页 |
| ·行为一致的服务替换 | 第66页 |
| ·类型安全 | 第66-67页 |
| ·机械化证明 | 第67-69页 |
| ·在普适服务中的应用 | 第69-73页 |
| ·普适服务的XML定义 | 第70-72页 |
| ·服务替换的体系结构 | 第72-73页 |
| ·本章小结 | 第73-74页 |
| 第四章 形式化验证普适服务行为的可信属性 | 第74-85页 |
| ·形式化验证方法 | 第74-77页 |
| ·普适服务行为分析 | 第77-82页 |
| ·有限状态进程语言 | 第78页 |
| ·普适服务行为的刻画 | 第78-80页 |
| ·行为属性的验证 | 第80-82页 |
| ·模型验证的整体步骤 | 第82-83页 |
| ·应用案例分析 | 第83-84页 |
| ·本章小结 | 第84-85页 |
| 第五章 普适环境下的动态服务更新 | 第85-114页 |
| ·需求背景 | 第85-87页 |
| ·普适应用 | 第85-86页 |
| ·需求与目标 | 第86-87页 |
| ·体系结构 | 第87-93页 |
| ·基本概念 | 第87页 |
| ·整体结构 | 第87-91页 |
| ·动态服务更新框架 | 第91-93页 |
| ·动态服务更新机制 | 第93-99页 |
| ·形式化分析与验证 | 第99-106页 |
| ·动态服务更新框架的形式化模型 | 第101-103页 |
| ·动态服务更新框架的属性验证 | 第103-104页 |
| ·类型安全更新 | 第104-106页 |
| ·原型实现与实验 | 第106-113页 |
| ·原型实现 | 第106-107页 |
| ·测试与性能评价 | 第107-111页 |
| ·更新目标的评估与分析 | 第111-113页 |
| ·本章小结 | 第113-114页 |
| 第六章 基于OSGi的普适应用场景 | 第114-126页 |
| ·应用背景 | 第114-115页 |
| ·OSGi服务平台 | 第115-117页 |
| ·OSGi规范 | 第115-116页 |
| ·R-OSGi中间件技术 | 第116-117页 |
| ·基于OSGi/R-OSGi框架上支撑平台的实现 | 第117-121页 |
| ·平台的体系结构 | 第118-120页 |
| ·核心部件之间的关系与说明 | 第120-121页 |
| ·场景案例 | 第121-125页 |
| ·普适服务替换的应用 | 第121-122页 |
| ·普适服务动态更新的应用 | 第122-124页 |
| ·评价与讨论 | 第124-125页 |
| ·本章小结 | 第125-126页 |
| 第七章 全文总结 | 第126-129页 |
| ·主要结论 | 第126-127页 |
| ·研究展望 | 第127-129页 |
| 附录 A 第3章相关定理证明 | 第129-135页 |
| 附录 B Coq证明脚本部分核心代码 | 第135-151页 |
| 附录 C 第4章中FSP部分代码及其属性定义 | 第151-152页 |
| C.1 FSP代码 | 第151页 |
| C.2 相关的属性定义 | 第151-152页 |
| 参考文献 | 第152-166页 |
| 致谢 | 第166-167页 |
| 攻读学位论文期间发表的学术论文目录 | 第167-169页 |
| 攻读博士期间参与的的科研项目 | 第169-171页 |
