Heuristisches Suchen und abstraktes Modell-Checking für Realzeit-Systeme (R03)

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

Ziel des Teilprojektes ist die Bekämpfung der Zustandsexplosion durch die Kombination zweier Ansätze:der Heuristischen Suche (also gerichtetes Model-Checking und Planungsverfahren aus derKünstlichen Intelligenz) und Abstraktion (in Kombination mit automatischer Abstraktionsverfeinerung).Das Leitmotiv des Vorhabens ist es, die beiden Ansätze zu kombinieren, indem die Suche aufAbstraktionen durch Heuristiken gelenkt wird, die durch das Lösen von Suchproblemen auf noch gröberenAbstraktionen berechnet wurden. Mit diesem Russische-Puppen-Prinzip ist das Projekt in derLage, informative Heurisiken effizient zu generieren, um sie rekursiv für die Suche zur Herleitungbesserer Abstraktionen und letztendlich zum Korrektheitsbeweis zu benutzen.

• 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; Universität des Saarlandes
• Teilprojektleiter: Professor Dr. Bernd Finkbeiner; Professor Dr. Bernhard Nebel; Professor Dr. Andreas Podelski