Dynamische Kommunikationssysteme (S02)

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

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