Personal


Kollegiaten


Ehemalige StipendiatInnen und KollegiatInnen


Motivation und Ziele

Das Konzept der reaktiven, technischen Systeme bildet den motivierenden Hintergrund für das hier zu beschreibende Forschungsgebiet. Abstrakt gesagt sind solche Systeme Konfigurationen von Betriebsmitteln, auf denen Prozesse, d. h. Folgen von Aktionen ablaufen; die Abfolgen der Aktionen hängen vom inneren Zustand des Systems oder von äußeren Vorgängen ab und realisieren somit den funktionalen Zweck des Systems. Beispiele für reaktive Systeme sind Betriebssysteme, Kommunikationssysteme, Kontrollsysteme verfahrenstechnischer Anlagen und ärztliche Diagnosesysteme.

Im Forschungsgebiet "Spezifikation diskreter Prozesse und Prozesssysteme durch operationelle Modelle und Logiken" sollen Prozesse, die auf reaktiven, technischen Systemen ablaufen, mit Hilfe formaler Methoden beschrieben werden. Aus dieser Beschreibung sollen Eigenschaften ableitbar oder verifizierbar sein, die alle auf solchen Systemen ablaufenden Prozesse haben. Beispielsweise möchte man in Betriebssystemen Aussagen über die Freiheit von Konflikten bei der Zuordnung von Rechnerbetriebsmitteln nachweisen können. Wegen der Komplexität der betrachteten Systeme eröffnet sich eine zuverlässige Möglichkeit der Verifikation nur durch die Verwendung formaler Methoden.

Für die Beschreibung von Prozessen gibt es eine große Vielfalt von Formalismen. Sie lassen sich in operationelle Modelle (z. B. Petri Netze, asynchrone Transitionssysteme, nebenläufige Automaten, CCS, pi-Kalkül, Term- und Graphersetzungssysteme) und Logiken (z. B. Prädikatenlogik, Fluentkalkül, Lineare Logik, temporale Logik, µ-Kalkül) einteilen.

Das Ziel des Forschungsprogramms ist einerseits, die in der ersten Förderperiode des Graduiertenkollegs begonnene Untersuchung der Formalismen und deren Zusammenhänge weiterzuführen, und andererseits, diese Formalismen um Methoden zur Verifikation von Eigenschaften von Prozessen anzureichern. Sofern die Gelegenheit besteht, sollen in einer dritten Förderperiode die bearbeiteten Spezifikations- und Verifikationstechniken auf ein konkretes Beispiel angewendet werden.


Forschungsprogramm

Das Forschungsprogramm unterteilt sich in fünf Forschungsschwerpunkte:

1. Algebraische Modelle für Prozesse

2. Kategorientheoretische Modelle für Prozesse

3. Logik-Spezifikation von Prozessen

4. Semiautomatische Verifikation von Prozesseigenschaften

5. Begriffliche Wissensverarbeitung bei diskreten Prozessen


Gäste und Veranstaltungen

der ersten Förderperiode (01.01.1997 bis 31.12.1999)

der zweiten Förderperiode (01.01.2000 bis 31.12.2002)

der dritten Förderperiode (01.01.2003 bis 31.12.2005)



GRK-Bibliothek

Bibliothek des Graduiertenkollegs



Dissertationen


Geeignete Vorlesungen für GRK-Stipendiaten

Vorlesungen Sommersemester 2000 - Wintersemester 2005/2006


Weitere Informationen ...

... können beim Sprecher des Graduiertenkollegs erfragt werden:

Technische Universität Dresden
Fakultät Informatik
Prof. Dr.-Ing. habil. Heiko Vogler
01062 Dresden
Tel.: 03 51/4 63-3 82 32
e-mail: vogler@inf.tu-dresden.de
http://www.orchid.inf.tu-dresden.de/gdp/