Modelling and Reasoning about Dynamic Networks as Concurrent Systems

David Rydeheard, Yanti Rusmawati

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

    Abstract

    We propose a new approach to modelling and reasoning about dynamic networks. Dynamic networks consist of nodes and edges whose operating status may change over time (for example, the edges may be unreliable and operate intermittently). Message-passing in such networks is inherently difficult and reasoning about the behaviour of message-passing algorithms is also difficult. We develop a series of abstract models which allow us to focus on the correctness of routing methods. We model the dynamic network as a ``demonic'' process which runs concurrently with routing updates and message-passing. This allows us to use temporal logic and fairness constraints to reason about dynamic networks. The models are implemented as multi-threaded programs and, to validate them, we use an experimental run-time verification tool called RuleR.
    Original languageEnglish
    Title of host publicationProceedings of the 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
    EditorsChristine Choppy, Jun Sun
    Place of PublicationInProceedings
    PublisherWadern Schloss Dagstuhl and Leibniz-Zentrum fuer Informatik
    Pages80-85
    Number of pages6
    Volume31
    ISBN (Print)978-3-939897-56-9
    DOIs
    Publication statusPublished - 21 Jun 2013
    Event1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013) - National University of Singapore, Singapore, Singapore
    Duration: 15 Jul 201316 Jul 2013
    http://drops.dagstuhl.de/opus/volltexte/2013/4092/

    Conference

    Conference1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)
    Country/TerritorySingapore
    CitySingapore
    Period15/07/1316/07/13
    Internet address

    Keywords

    • Dynamic networks
    • Concurrent systems
    • Message-passing networks
    • Fairness constraints

    Fingerprint

    Dive into the research topics of 'Modelling and Reasoning about Dynamic Networks as Concurrent Systems'. Together they form a unique fingerprint.

    Cite this