Modelling and Reasoning about Dynamic Networks as Concurrent Systems

Authors Yanti Rusmawati, David Rydeheard

Thumbnail PDF


  • Filesize: 0.53 MB
  • 6 pages

Document Identifiers

Author Details

Yanti Rusmawati
David Rydeheard

Cite AsGet BibTex

Yanti Rusmawati and David Rydeheard. Modelling and Reasoning about Dynamic Networks as Concurrent Systems. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 80-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


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.
  • dynamic networks
  • temporal logic
  • concurrent systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail