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