2026-07-24T09:32:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4092 2024-03-06T10:29:16Z ddc:004 open_access

Modelling and Reasoning about Dynamic Networks as Concurrent Systems Rusmawati, Yanti Rydeheard, David dynamic networks temporal logic concurrent systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yanti Rusmawati and David Rydeheard 2013 Is Part Of OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FSFMA.2013.80 urn:nbn:de:0030-drops-40921 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.80 eng https://creativecommons.org/licenses/by/3.0/legalcode