Dynamic Communication Systems (S02)

Subject Area Software Engineering and Programming Languages
Term from 2004 to 2015
Project identifier Deutsche Forschungsgemeinschaft (DFG) - Project number 5485999
 

Project Description

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