Directed Model Checking in the Analysis of Real-Time and Probabilistic Systems

• Applicant: Professor Dr. Stefan Leue
• Subject Area: Software Engineering and Programming Languages
• Term: from 2005 to 2009
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5454936

Die Komplexität eingebetteter Softwaresysteme verlangt nach effizienten, automatischen Methoden die überprüfen, ob diese Systeme Korrektheitsanforderungen erfüllen, die ihr sicheres Funktionieren gewährleisten. Wichtige Klassen von Eigenschaften, die diese Systeme zu erfüllen haben, beziehen sich auf das Echtzeitverhalten dieser Systeme, und auf die Wahrscheinlichkeit, einen gewissen Dienst innerhalb einer vorgegebenen Zeitspanne zu erbringen. In diesem Projekt entwickeln wir automatische Verifikationsmethoden die es erlauben, solche Eigenschaften für ein gegebenes Entwurfsmodell zu überprüfen. Die besondere Herausforderung liegt dabei darin, sicher zu stellen, dass sich diese Methoden auf die immense Größe der von nebenläufigen, eingebetteten Softwaresystemen erzeugten Zustandsräume skalieren lassen. Wir gehen diese Herausforderung insbesondere dadurch an, dass wir Modellprüfverfahren für Echtzeit- und probabilistische Systeme mit heuristischen, intelligenten Techniken der Zustandsraumanalyse verbinden. Dieser Ansatz ist unter dem Begriff Gerichtete Modellprüfverfahren bekannt geworden. Insbesondere verwenden wir heuristische Techniken, um die Effizienz der Abstraktionsverfeinerung für Echtzeit-Modellprüfverfahren zu erhöhen, und um bedeutungsvolle Gegenbeispiele für probabilistische Systemmodelle zu finden.

• DFG Programme: Research Grants