Der Forschungsschwerpunkt „Modellbasierte Verifikation softwarebasierter Automatisierungssysteme“ befasst sich mit der Entwicklung und der Evaluierung von Verfahren zur Erkennung bzw. zum Ausschluss logischer Fehler zu vorspezifiziertem Verhalten. Hierzu gehören insbesondere safety-relevante Fehler bzw. security-relevante Schwachstellen, die im Zusammenhang mit dem Entwurf bzw. der Implementierung softwarebasierter Steuerungen entstehen, sowie Konzeptfehler bei der Erfassung bzw. der Realisierung kooperierender mobiler Agenten (z.B. Roboter).
Zum Zwecke einer systematischen Verifikation des anzustrebenden autonomen bzw. kooperierenden Verhaltens sind zunächst geeignete
formale Notationen auszuwählen, die das jeweils zu analysierende Systemverhalten
auf einer problemangemessenen Abstraktionsebene zu erfassen und zu analysieren
erlauben. In Abhängigkeit von anwendungsspezifischen Merkmalen (Codenähe, Beschränktheit
der Zustände, Nebenläufigkeit, zeitgesteuertes bzw. ereignisgesteuertes Verhalten,
anzustrebende Skalierbarkeit in Bezug auf die Anzahl der Agenten) bieten sich unterschiedliche
Formalismen an, etwa
- (datenflussannotierte) Kontrollflussgraphen,
- endliche (zeitbehaftete) Zustandsmaschinen,
- kommunizierende erweiterte Zustandsmaschinen,
- Farbige Petri-Netze, etc.