Date and Time: Thursday, 11 December 2008, 15:30 - 16:30

Location: HG 6.96

Speaker: Muhammad Atif (OAS)

Title: Formal Verification of Heartbeat Protocols

Abstract:

Heartbeat protocols form an essential ingredient of many other distributed systems and protocols, such as failure detectors. We present a formal analysis of a class of 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 in process-algebraic and automata-theoretic formalisms mCRL2 and UPPAAL. Then, we formulate and formalize some natural functional requirements on the above-mentioned protocols. Using model-checking techniques, we verify these requirements on each and every version. We report counter-examples witnessing that the formulated requirements are not satisfied.
(joint work with Mohammad Mousavi)