Westphal, Bernd (2008) Specification and verification of dynamic topology systems: on the applicability of query- and data-type-reduction-based abstractions. PhD, Universität Oldenburg.

Preview

Volltext (3639Kb)

Abstract

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.

["eprint_fieldname_abstract_plus" not defined]

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 adaequat 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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	[Keine Schlagwörter von Autor/in vergeben.]
Controlled Keywords:	Eingebettete Systeme, Kommunikationstopologie
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law
Date Deposited:	17 Jan 2013 14:22
Last Modified:	08 Jul 2013 13:04
URI:	https://oops.uni-oldenburg.de/id/eprint/754
URN:	urn:nbn:de:gbv:715-oops-7900
DOI:
Nutzungslizenz:

Actions (login required)

View Item