Formal specification and analysis of Accelerated Heartbeat Protocols

Abstract

We present a formal analysis of all different variations of accelerated heartbeat protocols presented in [M.G. Gouda and T.M. McGuire, Accelerated Heartbeat Protocols, Proc. of ICDCS'98]. We formalize the specification of the protocols both in a process-algebraic and in an automata-theoretic formalism. Then, we formulate some natural functional requirements on the above-mentioned protocols and formalize these requirements. Using model-checking techniques, we verify these requirement on each and every version. We report counter-examples witnessing that the formulated requirements are not satisfied. We propose solutions for different versions of the protocol and model check the fixed versions; the model checking results indicate that the fixed versions indeed satisfy the requirements. Show more