Formal specification and analysis of accelerated heartbeat protocols

M. Atif, M.R. Mousavi

    Research output: Book/ReportReportAcademic

    76 Downloads (Pure)


    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 counterexamples 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.
    Original languageEnglish
    Place of PublicationEindhoven
    PublisherTechnische Universiteit Eindhoven
    Number of pages24
    Publication statusPublished - 2009

    Publication series

    NameComputer science reports
    ISSN (Print)0926-4515


    Dive into the research topics of 'Formal specification and analysis of accelerated heartbeat protocols'. Together they form a unique fingerprint.

    Cite this