Auch als elektronisches Dokument vorh ; Oldenburg, Univ., Diss., 2008
HochschulschriftEingebettetes SystemDatentypReduktionKürzungGegenmaßnahmeCyber-physisches System
Dynamic Communication Systems (DTR) bestehen aus einer veraenderlichen und unbeschraenkten Anzahl von eingebetteten Systemen, die in veraenderlichen Kommunikationstopologien interagieren. Ein prominentes Beispiel ist ein verteilter Algorithmus zur Verwaltung von Fahrzeug-Kolonnen, wobei ein Fahrzeug einem eingebetteten System entspricht. In dieser Arbeit wird die Eignung einer bestimmten, fuer parametrisierte Systeme bekannten Abstraktion zur Verifikation von DTS in einem Graph-basierten Kontext untersucht. Dazu fuehren wir basierend auf klassischen Transitionssystemen ein neues formales Modell solcher Systeme ein und schlagen eine Temporallogik 1. Stufe vor, die insbesondere das vorzeitige Verschwinden von Agenten adequat behandelt. Die praktische Relevanz des Verfahrens wird anhand von Fallstudien demonstriert unter Verwendung einer syntaktischen Transformation, die ausgehend von einer High-Level-Beschreibung des Originalsystems das endliche, abstrakte Transitionssystem liefert. <dt.>
A Dynamic Topology Systems (DTS) is composed of a varying and unbounded number of embedded systems interacting in a varying communication topology. A prominent example is distributed control of car platooning, where each cars is seen as a single embedded system. We address the need of formal verification for such critical systems by investigating a certain abstraction technique known for parameterised systems. To this end, we propose a new computational model of DTS, a conservative extension of classical transitions systems, and a first-order extension of classical temporal logic which in particular caters faithfully for pre-mature disappearance of agents. The potential of the studied abstraction is assessed via a new, graph-based formalisation. The practical applicability is demonstrated by case-studies employing a syntactical transformation procedure which efficiently yields the finite abstract transition system, given a high-level description of the original systems. <engl.>
