针对现有拜占庭容错协议的假设(要求被保护的对象是被动的和独立的)不适用于服务计算等新兴计算模型的问题,提出一种面向服务计算的拜占庭容错协议。该协议在服务请求方和服务提供方两端均创建服务复制品,采用基于状态机的主动复制技术,在服务复制品间进行三轮通信,就该请求的编号和内容达成一致,随后该请求被提交给上层应用逻辑处理;收到应答后,服务请求方的复制品进行三轮通信就应答的编号和内容达成一致后接受该应答。针对现有面向服务计算的拜占庭容错协议只有简单的正确性推理缺乏形式化验证的问题,采用1/0自动机和模拟关系方法进行正确性证明,更加严谨和正式。构造一个高度抽象的简单1/0自动机S,此自动机满足安全性和及时性;将协议中的各方分解成若干简单1/0自动机:前端自动机、后端自动机和多播通道自动机;最后用模拟关系方法证明各成员自动机构成的系统实现了自动机S,从而证明协议的正确性。使用1/0自动机可以精确描述协议,以此为基础进行证明比感性推理的证明方法更加规范。
声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
全部0条评论
快来发表一下你的评论吧 !