Advanced Search
    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

    • 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.
    • loading

    Catalog

      Turn off MathJax
      Article Contents

      /

      DownLoad:  Full-Size Img  PowerPoint
      Return
      Return