Analyzing energy consumption of wireless networks : a model-based approach

Yue, Haidi; Katoen, Joost-Pieter

doi:4510

Analyzing energy consumption of wireless networks : a model-based approach = Analyse des Energieverbrauchs von drahtlosen Netzwerken : ein modellbasierter Ansatz

Yue, Haidi (Author)

2013

Verantwortlichkeitsangabevorgelegt von Haidi Yue

ImpressumAachen : Publikationsserver der RWTH Aachen University 2013

Umfang169 S. : Ill., graph. Darst.

Aachen, Techn. Hochsch., Diss., 2013

Zsfassung in dt. und engl. Sprache

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2013-03-04

Online
URN: urn:nbn:de:hbz:82-opus-45100
URL: https://publications.rwth-aachen.de/record/211692/files/4510.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Drahtloses vermaschtes Netz (Genormte SW) ; Drahtloses lokales Netz (Genormte SW) ; Drahtloses Sensorsystem (Genormte SW) ; Ad-hoc-Netz (Genormte SW) ; Protokoll <Datenverarbeitungssystem> (Genormte SW) ; Analyse (Genormte SW) ; Energieverbrauch (Genormte SW) ; Modellierung (Genormte SW) ; Informatik (frei) ; Netzwerk (frei) ; drahtloses Netzwerk (frei) ; Protokolle (frei) ; network (frei) ; wireless network (frei) ; protocols (frei) ; energy (frei) ; modeling (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Drahtlose Netzwerke sind schon seit Jahrzehnten ein heißes Thema, sowohl in der Wissenschaft wie auch in der Industrie. Heute gibt es schon viele verschiedene Arten von drahtlosen Netzwerken. Hierzu zählen zum Beispiel drahtlose lokale Netze, drahtlose persönliche Netze, drahtlose Ad-hoc-Netzwerke und drahtlose Sensornetzwerke. Bei allen drahtlosen Netzen ist der Energieverbrauch ein sehr wichtiger Punkt. Entsprechend wurde schon viel Mühe investiert, um die Energieeffizienz in diesen Netzen zu analysieren und zu verbessern. In dieser Dissertation wird ein modellbasierter Ansatz für die Analyse des Energieverbrauchs von verschiedenen drahtlosen Netzwerk-Protokollen betrachtet. Hierbei ist mit modellbasiertem Ansatz gemeint, dass alle Protokolle als mathematische Modelle formalisiert werden, genauer gesagt als diskrete endliche Markov-Ketten (DTMCs), Markov-Entscheidungsprozesse (MDP) oder stochastische Zeitautomaten (STA). Die betrachteten Protokolle sind ein Leader-Election-Protokoll, ein Routing-Protokoll, und zwei Medium-Access-Control-(MAC)-Protokolle. Die Formalisierungen von Protokollen, die auf DTMCs und MDP basieren, werden in PRISM modelliert, einem bekannten Model-Checker für probabilistisches Model-Checking. Die Technik des Model-Checking gehört zur Familie der formalen Methoden. Sie untersucht abschließend alle möglichen (erreichbaren) Zustände von Modellen und prüft, ob diese eine bestimmte Spezifikation erfüllen. In dieser Arbeit werden diese Spezifikationen hinsichtlich der gewünschten Systemeigenschaften untersucht. Diese werden in der Regel durch Logiken ausgedrückt, wie zum Beispiel die probabilistische Computer Tree Logic (PCTL). Da das Model-Checking-Verfahren auf strengen mathematischen Grundlagen basiert und den gesamten Zustandsraum eines Modells erkundet, ist seine Anwendbarkeit durch das sogenannte Zustandsraum-Explosionsproblem beschränkt. Hierbei handelt es sich um die Problematik, dass der Zustandsraum mit der Größe des Modells exponentiell wächst. Das heißt, dass selbst für Systeme mit mittlerer Größe die Analyse nicht ohne Weiteres möglich ist. Im Gegenteil zu DTMCs und MDP müssen STA-Modelle mit Hilfe der ereignisorientierten Simulation simuliert werden, da derzeit kein Model-Checking-Programm existiert, das mit der mächtigen Aussagestärke, beziehungsweise allen Eigenschaften von STA-Modellen umgehen kann. Neben der eigentlichen Energieverbrauchsanalyse dieser Protokolle, werden Modifikationen vorgeschlagen, die zu einer erhöhten Energieeffizienz führen können.

During the last decades, wireless networking has been continuously a hot topic both in academy and in industry. Many different wireless networks have been introduced like wireless local area networks, wireless personal networks, wireless ad hoc networks, and wireless sensor networks. If these networks want to have a long term usability, the power consumed by the wireless devices in each of these networks needs to be managed efficiently. Hence, a lot of effort has been carried out for the analysis and improvement of energy efficiency, either for a specific network layer (protocol), or new cross-layer designs. In this thesis, we apply model-based approach for the analysis of energy consumption of different wireless protocols. The protocols under consideration are: one leader election protocol, one routing protocol, and two medium access control protocols. By model-based approach we mean that all these four protocols are formalized as some formal models, more precisely, as discrete-time Markov chains (DTMCs), Markov decision processes (MDPs), or stochastic timed automata (STA). For the first two models, DTMCs and MDPs, we model them in PRISM, a prominent model checker for probabilistic model checking, and apply model checking technique to analyze them. Model checking belongs to the family of formal methods. It discovers exhaustively all possible (reachable) states of the models, and checks whether these models meet a given specification. Specifications are system properties that we want to study, usually expressed by some logics, for instance, probabilistic computer tree logic (PCTL). However, while model checking relies on rigorous mathematical foundations and automatically explores the entire state space of a model, its applicability is also limited by the so-called state space explosion problem -- even systems of moderate size often yield models with an exponentially larger state space that thwart their analysis. Hence for the STA models in this thesis, since there is currently no model checking tool available to deal with all features of them, we use a discrete-event simulator to analyze these models by means of simulations. For each of these protocols, we not only analyze their energy consumption, but also propose some modifications to improve their energy efficiency.

Fulltext:
PDF