Failure tolerance for edge offloading based on model checking

Abstract

The number of mobile devices has been rising significantly and consequently a vast number of demanding applications are connected to the internet. Therefore, batterylifetime and low latency requirements are gaining more and more importance for the end users experience. In mobile cloud computing parts of applications are offloaded to a remote cloud server in order to save energy on the mobile devices. Concerning geographical distribution of cloud computing data centers and the resulting increase in offloading time, mobile edge computing is one solution to overcome these issues. It is proposed to handle this vast amount of devices and connections and to ensure low latency and fast response time. The decision whether an application is offloaded or not depends on several factors including network connectivity and free resources on the remote server. In this thesis the formal verification technique statistical model checking is used to support the offloading decision and to minimize offloading errors. Based upon the well-known model checker Uppaal, failure tolerance for edge offloading will be analysed. The proof of concept includes the Edge Offloading Prototype which uses the Uppaal engine for analyzing the edge network and a state-of-the-art web application to enable convenient testing and interacting with the prototype. In order to predict and handle the mobility of mobile device users in an edge environment, two real data traces are used for evaluation. The worst-case and best-case analysis show that the prototype is able to predict offloading activity in mobile edge computing accurately. Furthermore, the results show that it is a promising approach for static and low mobility scenarios in mobile edge computing. Therefore, this proof of concept is able to support ISPs or cloud service providers in planning their edge infrastructure.

Die Anzahl der mobilen Endgeräte ist in den letzten Jahren erheblich gestiegen und folglich gibt es eine immer größer werdende Anzahl an komplexen Anwendungen, die mit dem Internet verbunden sind. Daher werden Batterielebensdauer und niedrige Latenzanforderungen immer wichtiger für die Nutzerinnen und Nutzer von mobilen Endgeräten. In Mobile Cloud Computing werden Teile der Applikationen auf einen entfernten Cloud Server transferiert um eine Energieersparnis auf den mobilen Endgeräten zu erreichen. Da die Cloud Computing Datenzentren einerseits meist geographisch weit voneinander entfernt sind, und andererseits auch die Distanz zu der Endanwenderin oder dem Endanwender erheblich sein kann, steigt die Zeitspanne, die für die Übermittlung der Daten nötig ist, enorm. Eine Lösung zur Bewältigung dieses Problems ist Mobile Edge Computing, wodurch niedrigere Latenzzeiten und schnellere Antwortzeiten erreicht werden können. Die Entscheidung, ob eine Applikation oder ein Teil davon auf einem entfernten Server ausgeführt wird, hängt von einigen Faktoren ab, wie zum Beispiel einer bestehenden Netzwerkverbindung oder genügend freier Ressourcen am betreffenden Server. In dieser Arbeit wird die formale Verifikationstechnik Statistisches Model Checking verwendet um die Entscheidung, ob eine Aufgabe auf einem Edge Server ausgeführt wird, zu unterstützen. Ebenso sollen dadurch falsche Entscheidungen minimiert werden. Um die Fehlertoleranz zu analysieren wird der bekannte Model Checker Uppaal verwendet. Das Proof of Concept beinhaltet einen Edge Offloading Prototype, welcher die Uppaal- Engine verwendet um das Edge Netzwerk zu analysieren. Zusätzlich unterstützt eine Webapplikation das Testen und ermöglicht eine bessere Interaktion mit dem Prototyp. In der Praxis spielt auch die Mobilität der Benutzerinnen und Benutzer von mobilen Geräten eine entscheidende Rolle. Aus diesem Grund wurden zwei Datensätze aus der Praxis verwendet um den Prototypen zu evaluieren. Dabei zeigt eine worst-case und best-case Analyse in einem Mobile Edge Computing Szenario, dass der Prototyp in der Lage ist, die Entscheidung, ob eine Aufgabe auf einem Edge Server ausgeführt werden soll, präzise vorhersagen kann. Darüber hinaus zeigen die Ergebnisse der Evaluierung, dass es ein vielsprechender Ansatz sowohl für statische Szenarien, als auch Szenarien mit geringer Mobilität der Benutzerinnen und Benutzer ist. Das Proof of Concept ist daher imstande ISPs oder Anbieter von Cloud Diensten bei der Planung ihrer Edge- Infrastruktur zu unterstützen.