SMT-as-a-Service at the Edge

Abstract

Die steigende Anzahl der Geräte im Internet der Dinge (engl. Internet of Things, IoT) führt zu neuartigen technologischen Anwendungsbereichen wie Smart Cities, Industrie 4.0 oder E-Health. Ein Großteil der dort verwendeten Geräte verfügt nur über sehr limitierte Ressourcen wie Speicherkapazität und Rechenleistung, was bezüglich Kostenfaktor einen Vorteil darstellt, jedoch bei der Verarbeitung von großen Datenmengen in Echtzeit zu Problemen führt. Durch die Einführung von Cloud Computing wurde dieses Problem vorerst mit der Auslagerung der Datenverarbeitung gelöst. Der Umstand, dass die Daten auf den IoT Geräten entstehen und das Ergebnis der Verarbeitung in den meisten Fällen dort wieder benötigt wird, führt zu dem Paradigma von Edge Computing, bei dem die Verarbeitung wieder näher an die Endgeräte rückt. Neben dieser Entwicklung gewinnt der formale Ansatz von Satisfyability Modulo Theories (SMT) immer mehr an Bedeutung, mit der Modellierung von Optimierungsproblemen oder Verifikationen im IoT Bereich. Diese Probleme sind zum Teil sehr rechenintensiv, was den Einsatz von Edge und Cloud Computing zur Folge hat. Auf der anderen Seite ist ein essenzieller Punkt die Verarbeitung in Echtzeit, welcher die Beachtung der Latenzen bedingt. Dies resultiert daher in die Notwendigkeit eines Systems, welches das gesamte device-to-cloud Kontinuum für die Lösung von SMT Problemen nutzt.Die vorliegende Arbeit folgt genau dieser Notwendigkeit und präsentiert die Idee eines “SMT-as-a-Service at the Edge”-Systems.Der Kerninhalt der Arbeit ist ein Entscheidungsprozess, der entscheidet, in welchem Bereich des device-to-cloud Kontinuums die SMT-Probleme in Abhängigkeit von den aktuellen Bedingungen am effizientesten gelöst werden können. Dabei gilt es die Architektur des IoT-Umfelds zu beachten, die aktuellen Bedingungen, sowie die Ziele, die verfolgt werden wollen. Dieser Prozess agiert in einem sich wechselnden Umfeld und soll möglichst flexibel in verschiedene Umgebungen integriert werden können. Dazu wird in dieser Arbeit Reinforcement Learning in unterschiedlichen Ausprägungen verwendet, um den Anforderungen standzuhalten. In der Arbeit wird eine Proof of Concept Implementierung vorgestellt, wobei bei der Architektur großer Wert auf den breiten Einsatz in verschiedenen Szenarien und die einfache Konfigurierbarkeit gelegt wird. In einer umfangreichen Evaluierung der prototypischen Implementierung vergleichen wir verschiedene Deployment Szenarien in einer umfassenden Testumgebung bestehend aus einem echten Roboter, Einplatinencomputern und virtuellen Maschinen in der Cloud. Dabei kommen SMT Probleme aus verschiedenen Komplexitätsklassen zum Einsatz. Neben diesen Benchmarks stellen wir einen konkreten Anwendungsfall, nämlich “Path Planning for Fog-Supported Robots” vor. Die Ergebnisse zeigen, dass ein System mit intelligenter Entscheidungsfindung mittels Reinforcement Learning in der Lage ist, SMT Probleme effizienter zu lösen. Unser Ansatz ist daher ein vielversprechender Schritt zur Nutzung von SMT im IoT in Kombination mit Auslagerung von Datenverarbeitung.

The increasing number of devices in the Internet of Things (IoT) is leading to new technological application areas such as smart cities, industry 4.0 or e-health. Most of the devices used there only have very limited resources such as storage capacity and computing power, which is an advantage in terms of the cost factor, but leads to problems when processing large amounts of data in real-time. With the advent of cloud computing, the problem of limited resources was addressed and solved by computational offloading. However, the fact that the data originate and the processing results are in most cases needed at the IoT devices causes the paradigm shift to edge computing, in which the processing moves closer to the edge devices again. Alongside this development, the formal approach of Satisfiability Modulo Theories (SMT) is gaining importance in IoT by being used to model optimisation or verification problems. These problems can become computationally intensive, which leads to the use of edge and cloud computing. On the other hand, real-time processing is an essential point, which requires attention to latencies. This results in the need for a system that utilises the entire device-to-cloud continuum.In this work, we follow exactly these requirements and present the idea of an “SMT-as-a-Service at the Edge” system. The core content of the work is a decision making process that decides in which area of the device-to-cloud continuum the SMT problems can be solved most efficiently depending on the current conditions. It is important to consider the architecture of the IoT environment, as well as the goals that want to be pursued by the underlying systems. This process operates in changing environments and should be able to be integrated into different settings as flexible as possible. For this purpose, we use reinforcement learning in various forms to meet the objectives. We present a proof of concept implementation, whereby great importance is attached to the broad use in various scenarios and simple configurability. In an extensive evaluation of the prototype implementation, we compare several deployment scenarios over a fully-fledged testbed featuring a real robot, single-board computers and virtual machines in the cloud. Furthermore, we use SMT problems from different complexity classes. Besides these benchmarks, we present a concrete use case, namely “Path Planning for Fog-Supported Robots”. The results show that our system using reinforcement learning is able to solve SMT problems more efficiently. Our approach is thus a promising step towards using SMT in IoT with the combination of computational offloading.