Dynamische Kommunikationssysteme (S02)

Fachliche Zuordnung Softwaretechnik und Programmiersprachen
Förderung Förderung von 2004 bis 2015
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5485999
 

Projektbeschreibung

Im Teilprojekt sollen automatische Verifikationsmethoden für Dynamische Kommunikationssysteme(DCSs) entwickelt werden. Diese bestehen aus sich dynamisch ändernden Mengen von Objekten; dieObjekte etablieren sich unter dynamisch ändernden Kommunikationsbeziehungen mit anderen Objekten.Weder die Kommunikationskanäle selbst, noch die Anzahl der gleichzeitig aktiven Instanzen vonKommunikationsbeziehungen, noch die Anzahl der gleichzeitig aktiven Objekte ist beschränkt. Aufdie so erhaltenen unendlichen Zustandssysteme ist Finite-Model-Checking nicht direkt anwendbar.Der Schlüssel liegt in neuartigen Abstraktionsmethoden, durch die man endliche Modelle aus unendlichenautomatisch erstellt. Das langfristige Ziel des Projekts ist die Weiterentwicklung von Abstraktionsmethodenaus der Programmanalyse und ihre Integration mit Konzepten und Verfahren aus demModel-Checking zur automatischen Verifikation von Dynamischen Kommunikationssystemen.
DFG-Verfahren Transregios
Teilprojekt zu TRR 14:  AVACS - Automatische Verifikation und Analyse komplexer Systeme
Antragstellende Institution Carl von Ossietzky Universität Oldenburg
Mitantragstellende Institution Albert-Ludwigs-Universität Freiburg; Max-Planck-Institut für Informatik; Universität des Saarlandes
Teilprojektleiter Professor Dr. Werner Damm; Professor Dr. Bernd Finkbeiner; Professor Dr.-Ing. Holger Hermanns; Professor Dr. Andreas Podelski; Professor Dr. Christoph Weidenbach