Proceedings of the Second International Conference on Internet of things, Data and Cloud Computing New York : ACM, 2017 (2017), Art.-Nr. 85, insges. 6 S. 1349 Seiten
International conference on embedded wireless systems and networks (EWSN) 2017 Canada : Junction Publishing, 2017 (2017), Seite 36-47 1 Online-Ressource (336 pages)
Selbststabilisierung ist ein Konzept der Fehlertoleranz, welches eine Wiederherstellung eines Systems nach Ausfall durch transiente Fehler garantiert, ohne von sich aus in einen solchen zu geraten. In der Literatur wird Selbststabilisierung meist in Hinblick auf die Wiederherstellung einer sicheren Ausführung untersucht. In dieser Arbeit wird das Konzept der Selbststabilisierung generalisiert, um mehrere Eigenschaftsarten abzudecken, die die Betrachtung der Wiederherstellung eines Systems hin zu einer möglichst hohen Servicequalität ermöglichen. Hierzu wird das Design, die Analyse und das Re-Engineering von Systemen, die bekannte Probleme in verteilten Systemen lösen, angewendet. Die Probleme sind: die Slot-Zuteilung in zeitbasierten Multiplexverfahren sowie der wechselseitige Ausschluss und eine erweiterte Version davon. Zusätzlich wird eine automatische Verifikationsmethode präsentiert, die die Verifikation solcher Eigenschaften in selbststabilisierenden Systemen erleichtert. <dt.>
Self-stabilization is a fault tolerance concept which ensures that a system finally recovers itself from failures due to transient faults, without running into them by itself. In the related work, self-stabilization almost exclusively regards the recovery to a safe behavior. In this work, the self-stabilization concept is generalized to cover more properties, which provides the ability of studying the recovery of a system to reach a possible high quality of service. To this end, this work concerns designing, analyzing, and re-engineering systems that solve common problems in distributing computing. The problems are: Time-Division-Multiple-Access (TDMA) slot assignment, mutual exclusion and an extended version of it. In addition, an automatic verification approach that simplifies verifying such properties in self-stabilizing systems is presented. <engl.>
Die Überprüfung der Erreichbarkeit kontrollorientierter Softwaresysteme wird komplexer, wenn sie arithmetische und probabilistische Hybridmodelle umfassen. Das Erkennen nichterreichbarer Codesegmente eines Programms (sog. tote Codes) ist in verschiedenen Standards für die Entwicklung eingebetteter Systeme erforderlich. Die meisten früheren Arbeiten können nicht mit Programmen umgehen, die nichtlineare Arithmetik induzieren. Diese Einschränkung wurde durch die Kombination mehrerer Techniken überwunden, welche die Zustandsraumexplosion angehen und große arithmetische Randbedingungen lösen. Eine Variante dieser Technik würde die probabilistische Erreichbarkeit durch Berechnen der maximalen Wahrscheinlichkeit des Erreichens schlechter Zustände in einem probabilistischen Modell verifizieren. Schließlich wird ein Modell-Slicing-Ansatz eingeführt, um Assumption-Commitment-Eigenschaften in Rechenmodellen zu verifizieren, die eine konsistente Semantik des Übergangssystems induzieren. <dt.>
Verifying reachability of control-oriented software systems is an industrial quest which is becoming more complex to answer when programs involve arithmetic and probabilistic hybrid models. Whenever code segments of a program are unreachable, they are called dead codes. Detecting dead code is required in various standards for embedded system development. Most previous work can’t handle programs inducing non-linear arithmetic, as they are confined to linear programs. This restriction was overcome by combining several techniques that attack state space explosion and solve large arithmetic constraints system. Additionally, a variant of this technique would verify probabilistic reachability by computing the maximum probability of reaching bad states in a probabilistic model. Finally, a model-slicing approach is introduced to verify assumption-commitment properties in computational models which induce consistent transition system semantics. <engl.>