Formal Specification and Analysis of Accelerated Heartbeat Protocols.

M. Atif and M.R. Mousavi. Technical Report CSR-09-04, Department of Computer Science, Eindhoven University of Technology, March 2009.

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

@TechReport{MousaviHeartbeat09,
    author      = "Atif, M. and Mousavi, M.R", 
    title       = "Formal Specification and Analysis of Accelerated Heartbeat Protocols",
    number      = "CSR-09-04",
    school      = "Department of Computer Science, Eindhoven University of Technology",
    year        = "2009"
}