Atif, MuhammadMousavi, Mohammad Reza2015-12-13July 12-149781617387029http://hdl.handle.net/1885/72665We 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.Keywords: Formal analysis; Formal specification and analysis; Functional requirement; Model check; Model-checking techniques; Process algebras; Automata theory; Computer simulation; Model checking; Algebra Formal Analysis; Heartbeat protocols; Model checking; Process algebra; Requirement verification20102016-02-24