Specification and verification of dynamic topology systems: on the applicability of query- and data-type-reduction-based abstractions

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.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Oldenburg

Year

2008

Author dc:creator

• Westphal, Bernd

• [Keine Schlagwörter von Autor/in vergeben.]

Repository record source_url

http://oops.uni-oldenburg.de/754

OAI identifier oai:identifier

oai:oops.uni-oldenburg.de:754