Cones and foci : a mechanical framework for protocol verification

W.J. Fokkink, J. Pang, J.C. Pol, van de

    Research output: Contribution to journalArticleAcademicpeer-review

    11 Citations (Scopus)

    Abstract

    We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects. Compared to the original cones and foci method from Groote and Springintveld, our method is more generally applicable, because it does not require a preprocessing step to eliminate t-loops. We prove soundness of our approach and present a set of rules to prove the reachability of focus points. Our method has been formalized and proved correct using PVS. Thus we have established a framework for mechanical protocol verification. We apply this framework to the Concurrent Alternating Bit Protocol.
    Original languageEnglish
    Pages (from-to)1-31
    JournalFormal Methods in System Design
    Volume29
    Issue number1
    DOIs
    Publication statusPublished - 2006

    Fingerprint Dive into the research topics of 'Cones and foci : a mechanical framework for protocol verification'. Together they form a unique fingerprint.

    Cite this