Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FSFMA.2013.80
URN: urn:nbn:de:0030-drops-40921
URL: https://drops.dagstuhl.de/opus/volltexte/2013/4092/
Rusmawati, Yanti ; Rydeheard, David
Modelling and Reasoning about Dynamic Networks as Concurrent Systems
| pdf-format: |
|
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.
BibTeX - Entry
@InProceedings{rusmawati_et_al:OASIcs:2013:4092,
author = {Yanti Rusmawati and David Rydeheard},
title = {{Modelling and Reasoning about Dynamic Networks as Concurrent Systems}},
booktitle = {1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
pages = {80--85},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-939897-56-9},
ISSN = {2190-6807},
year = {2013},
volume = {31},
editor = {Christine Choppy and Jun Sun},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4092},
URN = {urn:nbn:de:0030-drops-40921},
doi = {10.4230/OASIcs.FSFMA.2013.80},
annote = {Keywords: dynamic networks, temporal logic, concurrent systems}
}
| Keywords: | dynamic networks, temporal logic, concurrent systems | |
| Seminar: | 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013) | |
| Issue date: | 2013 | |
| Date of publication: | 14.07.2013 |
