Dynamic Communication Systems (S02)

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 Programme CRC/Transregios

Subproject of TRR 14:  Automatic Verification and Analysis of Complex Systems

Applicant Institution Carl von Ossietzky Universität Oldenburg

Co-Applicant Institution Albert-Ludwigs-Universität Freiburg; Max-Planck-Institut für Informatik; Universität des Saarlandes

Project Heads Professor Dr. Werner Damm; Professor Dr. Bernd Finkbeiner; Professor Dr.-Ing. Holger Hermanns; Professor Dr. Andreas Podelski; Professor Dr. Christoph Weidenbach