Formal specification and analysis of accelerated heartbeat protocols

M. Atif, M.R. Mousavi

    Onderzoeksoutput: Boek/rapportRapportAcademic

    84 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.
    Originele taal-2Engels
    Plaats van productieEindhoven
    UitgeverijTechnische Universiteit Eindhoven
    Aantal pagina's24
    StatusGepubliceerd - 2009

    Publicatie series

    NaamComputer science reports
    ISSN van geprinte versie0926-4515


    Duik in de onderzoeksthema's van 'Formal specification and analysis of accelerated heartbeat protocols'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit