面向网构软件资源自适应的可信性研究
| 摘要 | 第1-7页 |
| ABSTRACT | 第7-10页 |
| 目录 | 第10-12页 |
| 第1章 绪论 | 第12-17页 |
| ·研究背景及意义 | 第12-13页 |
| ·相关研究现状 | 第13-14页 |
| ·论文主要工作 | 第14-15页 |
| ·论文组织结构 | 第15-16页 |
| ·本章小结 | 第16-17页 |
| 第2章 网构软件基本理论 | 第17-21页 |
| ·网构软件的提出 | 第17-18页 |
| ·网构软件的基本特征 | 第18-19页 |
| ·网构软件的发展 | 第19-20页 |
| ·本章小结 | 第20-21页 |
| 第3章 接口自动机理论 | 第21-24页 |
| ·接口自动机简介 | 第21页 |
| ·接口自动机的形式化定义 | 第21-22页 |
| ·接口自动机网络的形式化定义 | 第22-23页 |
| ·本章小结 | 第23-24页 |
| 第4章 构件的随机性资源满足性验证 | 第24-34页 |
| ·随机性资源接口自动机 | 第24-28页 |
| ·随机性资源接口自动机的非形式描述 | 第24-25页 |
| ·随机性资源接口自动机的形式化描述 | 第25-26页 |
| ·随机性资源接口自动机网络的形式化描述 | 第26-28页 |
| ·随机性资源满足的验证 | 第28-32页 |
| ·验证方法 | 第28-29页 |
| ·相关算法 | 第29-32页 |
| ·检查组合系统是否满足随机性资源约束算法 | 第29-31页 |
| ·组合系统运行资源最小量算法 | 第31-32页 |
| ·实例研究 | 第32-33页 |
| ·本章小结 | 第33-34页 |
| 第5章 构件的时限资源满足性验证 | 第34-41页 |
| ·时限资源接口自动机 | 第34-36页 |
| ·时限资源接口自动机的非形式描述 | 第34-35页 |
| ·时限资源接口自动机的形式化描述 | 第35-36页 |
| ·时限资源接口自动机网络的形式化描述 | 第36页 |
| ·资源满足是否具有时限性验证 | 第36-39页 |
| ·验证方法 | 第37-38页 |
| ·相关算法 | 第38-39页 |
| ·实例研究 | 第39-40页 |
| ·本章小结 | 第40-41页 |
| 第6章 基于Spin的系统模型验证 | 第41-52页 |
| ·模型检测工具Spin | 第41-42页 |
| ·SPIN的历史背景 | 第41页 |
| ·SPIN的特征 | 第41-42页 |
| ·基于Spin的网构软件模型验证 | 第42-51页 |
| ·随机性资源接口自动机模型的验证 | 第43-46页 |
| ·时限资源接口自动机模型的验证 | 第46-51页 |
| ·本章小结 | 第51-52页 |
| 第7章 总结与展望 | 第52-53页 |
| 参考文献 | 第53-56页 |
| 攻读学位期间发表的学术论文目录 | 第56-57页 |
| 致谢 | 第57页 |
