| 摘要 | 第1-7页 |
| ABSTRACT | 第7-14页 |
| 第一章 引言 | 第14-27页 |
| ·研究背景 | 第14-20页 |
| ·网构软件技术 | 第14-16页 |
| ·网构软件模型的设计需求 | 第16页 |
| ·OSGi 服务平台 | 第16-18页 |
| ·抽象状态机理论 | 第18-20页 |
| ·需求与目标 | 第20-21页 |
| ·需求刻画的正确性 | 第20-21页 |
| ·精化过程的正确性 | 第21页 |
| ·目标属性的可验证性 | 第21页 |
| ·关键问题 | 第21-23页 |
| ·网构软件特征 | 第22-23页 |
| ·抽象状态机刻画机制 | 第23页 |
| ·普适环境网构原型验证系统 | 第23页 |
| ·本文的研究内容及主要贡献 | 第23-25页 |
| ·本文结构 | 第25-26页 |
| ·本章小结 | 第26-27页 |
| 第二章 基于构件的形式化技术 | 第27-36页 |
| ·构件的定义 | 第27-28页 |
| ·构件库 | 第28-30页 |
| ·构件形式化目前的现状 | 第30-34页 |
| ·网构软件构建对形式化方法的挑战 | 第34-35页 |
| ·本章小结 | 第35-36页 |
| 第三章 网构软件形式化抽象模型 | 第36-62页 |
| ·构件模型及基础模型(GROUND MODEL)概念 | 第37-38页 |
| ·构件模型 | 第37-38页 |
| ·基础模型(Ground Model)概念 | 第38页 |
| ·抽象状态机相关概念 | 第38-42页 |
| ·抽象状态和更新集 | 第38-40页 |
| ·抽象状态机的转移规则和运行 | 第40-41页 |
| ·抽象状态机中函数、关系及位置的分类 | 第41-42页 |
| ·构件的基础模型(GROUND MODEL) | 第42-51页 |
| ·构件的互操作性 | 第42-43页 |
| ·接口相容性 | 第43页 |
| ·行为相容性 | 第43-44页 |
| ·网络构件高层次模型 | 第44-46页 |
| ·高层模型基调及域名分析 | 第46-47页 |
| ·抽象信息发送机制 | 第47-48页 |
| ·发送抽象状态机 | 第48页 |
| ·基本双向交互模式 | 第48-50页 |
| ·交互模式相关问题 | 第50-51页 |
| ·网构软件的基础模型(GROUND MODEL) | 第51-60页 |
| ·构件组装的正确性和形式化验证方法 | 第51-52页 |
| ·组装模型映射架构 | 第52-53页 |
| ·匹配机制 | 第53-54页 |
| ·调度机制 | 第54页 |
| ·高层抽象状态机规则定义 | 第54-57页 |
| ·组装仲裁模型 | 第57-60页 |
| ·本章小结 | 第60-62页 |
| 第四章 网构软件抽象模型的精化 | 第62-84页 |
| ·精化机制简介 | 第62-63页 |
| ·精化过程 | 第63-65页 |
| ·网构软件形式化精化模型 | 第65-70页 |
| ·交互模式的组装精化 | 第65-69页 |
| ·构件精化 | 第69-70页 |
| ·基于R-OSGI 智能家庭协作模型精化案例 | 第70-73页 |
| ·案例介绍 | 第70-72页 |
| ·精化模型 | 第72-73页 |
| ·基于OSGI 的网构软件平台模型 | 第73-82页 |
| ·OSGi 平台运行机理 | 第74页 |
| ·OSGi Framework 主要域名 | 第74-75页 |
| ·OSGi Framework 基调集 | 第75-78页 |
| ·目标精化模型初始状态 | 第78页 |
| ·目标模型主要精化规则 | 第78-80页 |
| ·确定动态更新顺序精化案例 | 第80-82页 |
| ·本章小节 | 第82-84页 |
| 第五章 模型验证 | 第84-100页 |
| ·验证方法 | 第84-85页 |
| ·KIV | 第85-91页 |
| ·逻辑基础及验证机制 | 第86-88页 |
| ·验证案例 | 第88-91页 |
| ·可执行验证机制 | 第91-98页 |
| ·CoreASM | 第92-94页 |
| ·其它相关执行引擎 | 第94页 |
| ·基于可执行的验证案例 | 第94-98页 |
| ·本章小结 | 第98-100页 |
| 第六章 基于R-OSGI 的案例研究 | 第100-112页 |
| ·应用背景 | 第100-101页 |
| ·R-OSGI | 第101-107页 |
| ·技术概述 | 第101-102页 |
| ·远程服务注册和发现模型 | 第102-103页 |
| ·远程事件处理模型 | 第103-104页 |
| ·基于R-OSGi 中间件的Bundle 启动机制 | 第104-107页 |
| ·关键技术 | 第107-110页 |
| ·本章小结 | 第110-112页 |
| 第七章 总结 | 第112-116页 |
| ·主要结论 | 第112-114页 |
| ·研究展望 | 第114-116页 |
| 参考文献 | 第116-128页 |
| 致谢 | 第128-130页 |
| 攻读博士学位期间已发表或录用的论文 | 第130-132页 |