Model checking under fairness in ProB and its application to fair exchange protocols

D.M. Williams, J.E.J. Ruiter, de, W.J. Fokkink

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    6 Citations (Scopus)

    Abstract

    Motivated by Murray’s work on the limits of refinement testing for CSP, we propose the use of ProB to check liveness properties under assumptions of strong and weak event fairness, whose refinement-closures cannot generally be expressed as refinement checks for FDR. Such properties are necessary for the analysis of fair exchange protocols in CSP, which assume at least some messages are sent over a resilient channel. As the properties we check are refinement-closed, we retain CSP’s theory of refinement, enabling subsequent step-wise refinement of the CSP model. Moreover, we improve upon existing CSP models of fair exchange protocols by proposing a revised intruder model inspired by the one of Cederquist and Dashti. Our intruder model is stronger as we use a weaker fairness constraint.
    Original languageEnglish
    Title of host publicationTheoretical Aspects of Computing – ICTAC 2012 : 9th International Colloquium, Bangalore, India, September 24-27, 2012. Proceedings
    EditorsA. Roychoudhury, M. D’Souza
    Place of PublicationBerlin
    PublisherSpringer
    Pages168-182
    ISBN (Print)978-3-642-32942-5
    DOIs
    Publication statusPublished - 2012
    Event9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012) - Bangalore, India
    Duration: 24 Sep 201227 Sep 2012
    Conference number: 9

    Publication series

    NameLecture Notes in Computer Science
    Volume7521
    ISSN (Print)0302-9743

    Conference

    Conference9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012)
    Abbreviated titleICTAC 2012
    Country/TerritoryIndia
    CityBangalore
    Period24/09/1227/09/12

    Fingerprint

    Dive into the research topics of 'Model checking under fairness in ProB and its application to fair exchange protocols'. Together they form a unique fingerprint.

    Cite this