TU Darmstadt / ULB / TUbiblio

Correct-by-Construction Development of Dynamic Topology Control Algorithms

Speith, Roland (2018)
Correct-by-Construction Development of Dynamic Topology Control Algorithms.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung

Kurzbeschreibung (Abstract)

Wireless devices are influencing our everyday lives today and will even more so in the future. A wireless sensor network (WSN) consists of dozens to hundreds of small, cheap, battery-powered, resource-constrained sensor devices (motes) that cooperate to serve a common purpose. These networks are applied in safety- and security-critical areas (e.g., e-health, intrusion detection). The topology of such a system is an attributed graph consisting of nodes representing the devices and edges representing the communication links between devices. Topology control (TC) improves the energy consumption behavior of a WSN by blocking costly links. This allows a mote to reduce its transmission power. A TC algorithm must fulfill important consistency properties (e.g., that the resulting topology is connected). The traditional development process for TC algorithms only considers consistency properties during the initial specification phase. The actual implementation is carried out manually, which is error prone and time consuming. Thus, it is difficult to verify that the implementation fulfills the required consistency properties. The problem becomes even more severe if the development process is iterative. Additionally, many TC algorithms are batch algorithms, which process the entire topology, irrespective of the extent of the topology modifications since the last execution. Therefore, dynamic TC is desirable, which reacts to change events of the topology.

In this thesis, we propose a model-driven correct-by-construction methodology for developing dynamic TC algorithms. We model local consistency properties using graph constraints and global consistency properties using second-order logic. Graph transformation rules capture the different types of topology modifications. To specify the control flow of a TC algorithm, we employ the programmed graph transformation language story-driven modeling. We presume that local consistency properties jointly imply the global consistency properties. We ensure the fulfillment of the local consistency properties by synthesizing weakest preconditions for each rule. The synthesized preconditions prohibit the application of a rule if and only if the application would lead to a violation of a consistency property. Still, this restriction is infeasible for topology modifications that need to be executed in any case. Therefore, as a major contribution of this thesis, we propose the anticipation loop synthesis algorithm, which transforms the synthesized preconditions into routines that anticipate all violations of these preconditions. This algorithm also enables the correct-by-construction runtime reconfiguration of adaptive WSNs. We provide tooling for both common evaluation steps. Cobolt allows to evaluate the specified TC algorithms rapidly using the network simulator Simonstrator. cMoflon generates embedded C code for hardware testbeds that build on the sensor operating system Contiki.

Typ des Eintrags: Dissertation
Erschienen: 2018
Autor(en): Speith, Roland
Art des Eintrags: Erstveröffentlichung
Titel: Correct-by-Construction Development of Dynamic Topology Control Algorithms
Sprache: Englisch
Referenten: Schürr, Prof. Andy ; Giese, Prof. Holger
Publikationsjahr: 30 November 2018
Ort: Darmstadt
Datum der mündlichen Prüfung: 14 März 2019
URL / URN: https://tuprints.ulb.tu-darmstadt.de/8562
Kurzbeschreibung (Abstract):

Wireless devices are influencing our everyday lives today and will even more so in the future. A wireless sensor network (WSN) consists of dozens to hundreds of small, cheap, battery-powered, resource-constrained sensor devices (motes) that cooperate to serve a common purpose. These networks are applied in safety- and security-critical areas (e.g., e-health, intrusion detection). The topology of such a system is an attributed graph consisting of nodes representing the devices and edges representing the communication links between devices. Topology control (TC) improves the energy consumption behavior of a WSN by blocking costly links. This allows a mote to reduce its transmission power. A TC algorithm must fulfill important consistency properties (e.g., that the resulting topology is connected). The traditional development process for TC algorithms only considers consistency properties during the initial specification phase. The actual implementation is carried out manually, which is error prone and time consuming. Thus, it is difficult to verify that the implementation fulfills the required consistency properties. The problem becomes even more severe if the development process is iterative. Additionally, many TC algorithms are batch algorithms, which process the entire topology, irrespective of the extent of the topology modifications since the last execution. Therefore, dynamic TC is desirable, which reacts to change events of the topology.

In this thesis, we propose a model-driven correct-by-construction methodology for developing dynamic TC algorithms. We model local consistency properties using graph constraints and global consistency properties using second-order logic. Graph transformation rules capture the different types of topology modifications. To specify the control flow of a TC algorithm, we employ the programmed graph transformation language story-driven modeling. We presume that local consistency properties jointly imply the global consistency properties. We ensure the fulfillment of the local consistency properties by synthesizing weakest preconditions for each rule. The synthesized preconditions prohibit the application of a rule if and only if the application would lead to a violation of a consistency property. Still, this restriction is infeasible for topology modifications that need to be executed in any case. Therefore, as a major contribution of this thesis, we propose the anticipation loop synthesis algorithm, which transforms the synthesized preconditions into routines that anticipate all violations of these preconditions. This algorithm also enables the correct-by-construction runtime reconfiguration of adaptive WSNs. We provide tooling for both common evaluation steps. Cobolt allows to evaluate the specified TC algorithms rapidly using the network simulator Simonstrator. cMoflon generates embedded C code for hardware testbeds that build on the sensor operating system Contiki.

Alternatives oder übersetztes Abstract:
Alternatives AbstractSprache

Drahtlos kommunizierende Geräte sind ein wesentlicher Bestandteil der zunehmenden Digitalisierung unserer Gesellschaft. Ein drahtloses Sensornetzwerk (engl. Wireless Sensor Network, WSN) umfasst eine Vielzahl günstiger, kleiner, batteriebetriebener Sensoren, die gemeinschaftlich einem Ziel dienen (z.B. in einer e-Health-Anwendung). Die Topologie eines WSNs ist ein attributierter Graph, dessen Knoten die Geräte und dessen Kanten deren Kommunikationsverbindungen darstellen. Topologiekontrolle (engl. Topology Control, TC) reduziert den Energieverbrauch eines WSN, indem bestimmte physische Nachbarn eines Geräts ausgeblendet werden, wodurch sich dessen Sendeleistung reduzieren lässt. Der Topologiekontrollalgorithmus muss dabei wesentliche Konsistenzeigenschaften erhalten (z.B. den Zusammenhang des Topologie). Ungeachtet ihrer großen Bedeutung werden Konsistenzeigenschaften in der traditionellen Entwicklung von TC-Algorithmen nur in der anfänglichen Spezifikationsphase betrachtet. Die anschließende Implementierung des TC-Algorithmus wird von Hand durchgeführt und ist damit fehleranfällig und zeitaufwändig. Es ist schwierig nachzuweisen, dass die Implementierung die geforderten Konsistenzeigenschaften erfüllt, insbesondere da TC-Algorithmen typischerweise iterativ entwickelt werden. Die bestehenden Batch-TC-Algorithmen verarbeiten jeweils die gesamte Topologie ohne Wissen aus vorherigen Ausführungen zu nutzen. Daher ist es wünschenswert dynamische TC-Algorithmen zu entwicklen, die inkrementell auf Ereignisse reagieren.

In dieser Arbeit stellen wir eine modellbasierte Entwicklungsmethodik für garantiert korrekte dynamische TC-Algorithmen vor. Wir modellieren lokale Konsistenzeigenschaften mittels Graph-Constraints, globale Konsistenzeigenschaften mittels Prädikatenlogik zweiter Stufe sowie die möglichen Änderungen der Topologie und deren Kontrollfluss mittels programmierter Graphtransformationsregeln. Unter der Annahme, dass die lokalen Konsistenzbedingungen gemeinsam die globalen Konsistenzbedingungen implizieren, können wir mithilfe bestehender statischer Analysetechniken Vorbedingungen für die Graphtransformationsregeln synthetisieren, die sicherstellen, dass die modifizierten Regeln die Konsistenzbedingungen erhalten. Die resultierende Einschränkung ist für diejenigen Regeln, die das Umweltverhalten beschreiben, jedoch nicht zulässig. Wir stellen daher einen Algorithmus vor, der jede synthetisierte Vorbedingung systematisch in eine Antizipationsschleife überführt, welche alle unvermeidlichen Verletzungen der entsprechenden Vorbedingungen auflöst. Wir zeigen, dass sich dieser neuartige Algorithmus auch für die Rekonfiguration von adaptiven WSNs eignet. Um dem Nutzer unseres Ansatzes eine schnelle Erprobung eines entwickelten TC-Algorithmus zu ermöglichen, bieten wir Werkzeuge zur Evaluation im Netzwerksimulator (Cobolt) und Hardware-Testbed (cMoflon) an.

Deutsch
URN: urn:nbn:de:tuda-tuprints-85627
Sachgruppe der Dewey Dezimalklassifikatin (DDC): 000 Allgemeines, Informatik, Informationswissenschaft > 004 Informatik
Fachbereich(e)/-gebiet(e): 18 Fachbereich Elektrotechnik und Informationstechnik
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik > Echtzeitsysteme
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik
DFG-Sonderforschungsbereiche (inkl. Transregio)
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet > A: Konstruktionsmethodik
DFG-Sonderforschungsbereiche (inkl. Transregio) > Sonderforschungsbereiche > SFB 1053: MAKI – Multi-Mechanismen-Adaption für das künftige Internet > A: Konstruktionsmethodik > Teilprojekt A1: Modellierung
Hinterlegungsdatum: 07 Apr 2019 19:55
Letzte Änderung: 07 Apr 2019 19:55
PPN:
Referenten: Schürr, Prof. Andy ; Giese, Prof. Holger
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: 14 März 2019
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen