高级检索
    邓延军 徐学洲. 支持扩展虚拟同步的组通信算法形式描述与验证[J]. 计算机研究与发展, 2005, 42(4): 676-683.
    引用本文: 邓延军 徐学洲. 支持扩展虚拟同步的组通信算法形式描述与验证[J]. 计算机研究与发展, 2005, 42(4): 676-683.
    Deng Yanjun and Xu Xuezhou. Formal Specification and Verification for Group Communication Algorithm Suiting Extended Virtual Synchrony[J]. Journal of Computer Research and Development, 2005, 42(4): 676-683.
    Citation: Deng Yanjun and Xu Xuezhou. Formal Specification and Verification for Group Communication Algorithm Suiting Extended Virtual Synchrony[J]. Journal of Computer Research and Development, 2005, 42(4): 676-683.

    支持扩展虚拟同步的组通信算法形式描述与验证

    Formal Specification and Verification for Group Communication Algorithm Suiting Extended Virtual Synchrony

    • 摘要: 组通信系统是为方便开发容错的分布式应用系统而提出的一种通信中间件.虚拟同步是组通 信系统中的一个重要概念.其本质是限制向所有组成员递交组成员资格变化信息和应用消息 的次序.为支持网络可划分的情况,引入了扩展虚拟同步模型.针对扩展虚拟同步模型的特点 ,提出了一种基于客户/服务器模式的组通信系统架构,并以I/O自动机的形式给出系统内部 各模块的服务和算法.最后以继承建模的方式逐步给出该算法的自动机模型,并用形式化的 方法验证其正确性.

       

      Abstract: Group communication systems(GCSs) are communication middleware systems which fac ilitate the development of fault-tolerant distributed systems. One of the import ant concepts in GCSs is virtual synchrony(VS), the essence of which is that it g uarantees the order of group membership messages and application multicasting me ssages which are delivered to group members. In order to handle network partitio ns, the extended virtual synchrony(EVS) model is introduced. Moreover, this pape r incrementally constructs the specifications of GCSs which satisfy the EVS mode l using the inheritance-based methodology of the I/O automata formalism. Conside ring the characteristics of the EVS model, this paper presents an architecture o f GCS which is based on a client/server model, and formally formulates the servi ce and algorithm of the system using an I/O automata model. The algorithm of sui ting the EVS model is emphasized. It is formally specified and verified using th e inheritance-based methodology of the I/O automata formalism.

       

    /

    返回文章
    返回