Formal Specification and Analysis of Accelerated Heartbeat Protocols
Muhammad Atif and MohammadReza Mousavi
The 2010 Summer Computer Simulation Conference (SCSC 10)
Ottawa, Canada, July 11-14, 2010
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 fixes for different version of the protocol and model check the fixed versions; the model checking results indicate that the fixed versions indeed satisfy the requirements.
Conference Manager (V2.56.8 - Rev. 1182)