基于移动计算环境下卷回恢复算法及仿真研究

摘要

由于移动节点的不可靠和无线网络连接的脆弱性，研究移动计算系统容错机制具有重要意义。但由于移动计算系统自身的特殊性，使得先前为分布式系统研发的各种容错技术和手段不能直接运用于移动计算系统中，因此研究适合于移动分布式计算系统应用的容错机制显得尤为必要。
　　因果日志方法可以实现移动节点的异步卷回恢复，适用于移动计算环境。但针对网络规模较大的的移动计算网络系统，传统的因果日志方法存在通信和存储开销过大的缺点，文中提出了一种基于分层的因果日志卷回恢复算法，通过在移动支持站上记录小区内移动节点间传递消息的先行图(AG)来记录移动节点间的因果依赖关系，在移动支持站之间通过FBL协议记录跨区消息确定因子，该协议可以实现移动节点失效以及移动支持站失效的一致卷回恢复。
　　文中通过使用主要面向分布式软件和协议系统验证、由贝尔实验室J.Holzmann等于1989年开发的模型检测工具SPIN搭建了移动计算环境，使用PROMELA语言建立系统的状态机模型，并使用线性时态逻辑(LTL)公式对系统的需求属性进行形式化描述，应用自动机理论实现系统的模拟运行和正确性验证。在此移动计算环境中，对分层因果日志及完全AG图因果日志无故障运行时的状态进行仿真，仿真结果比较表明，分层因果日志在为移动节点实现异步的卷回恢复时显著的降低了通信和存储开销。

目录

基于移动计算环境下卷回恢复算法及仿真研究

RESEARCH ON ROLLBACK RECOVERY MECHANISM AND SIMULATION BASED ON THE MOBILE COMPUTING ENVIRONMENT

摘要

Abstract

第1章 绪论

1.1课题背景

1.2国内外研究现状

1.3本论文的主要工作

第2章 卷回恢复机制

2.1检查点技术

2.2基于日志的卷回恢复

2.3各种检查点技术的比较

2.4 SPIN模型检测器

本章小结

第3章 移动计算环境下消息日志算法

3.1消息日志概述

3.2因果日志协议

3.3移动计算环境

3.4算法描述

3.5卷回恢复

本章小结

第4章 移动计算系统建模及仿真

4.1移动计算系统建模

4.2移动计算系统各种行为实现

4.3完全AG图方法

4.4分层因果日志(Mobile_HCML)

4.5 全局一致检查点的设置

4.6协议仿真

4.7仿真结果

4.8一致性证明

本章小结

结论

参考文献

哈尔滨工业大学硕士学位论文原创性声明

哈尔滨工业大学硕士学位论文使用授权书

哈尔滨工业大学硕士学位涉密论文管理

致谢