面向服务计算的拜占庭容错方案及其正确性证明

摘要

针对现有拜占庭容错协议的假设(要求被保护的对象是被动的和独立的)不适用于服务计算等新兴计算模型的问题,提出一种面向服务计算的拜占庭容错协议.该协议在服务请求方和服务提供方两端均创建服务复制品,采用基于状态机的主动复制技术,在服务复制品间进行三轮通信,就该请求的编号和内容达成一致,随后该请求被提交给上层应用逻辑处理;收到应答后,服务请求方的复制品进行三轮通信就应答的编号和内容达成一致后接受该应答.针对现有面向服务计算的拜占庭容错协议只有简单的正确性推理缺乏形式化验证的问题,采用I/O自动机和模拟关系方法进行正确性证明,更加严谨和正式.构造一个高度抽象的简单I/O自动机S,此自动机满足安全性和及时性;将协议中的各方分解成若干简单I/O自动机:前端自动机、后端自动机和多播通道自动机;最后用模拟关系方法证明各成员自动机构成的系统实现了自动机S,从而证明协议的正确性.使用I/O自动机可以精确描述协议,以此为基础进行证明比感性推理的证明方法更加规范.