Directed model checking with AI exploration algorithms

• Applicant: Professor Dr. Stefan Edelkamp
• Subject Area: Image and Language Processing, Computer Graphics and Visualisation, Human Computer Interaction, Ubiquitous and Wearable Computing
• Term: from 2002 to 2010
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 5353726

Die formalen Methoden der Modellprüfung finden ein weiteres Anwendungsspektrum sowohl in der Hard- als auch in der Softwareentwicklung. Durch die Exploration großer Zustandsräume liefern sie entweder einen formalen Beweis für die Einhaltung einer geforderten Eigenschaft oder eine detaillierte Beschreibung eines möglichen Ablaufs, bei dem die Spezifikation verletzt wird. In den Techniken zur Bewältigung der enormen Zustandsraumgröße, die insbesondere durch die Festlegung konkurrierender Systeme hervorgerufen wird, ist die gerichtete Exploration ein neuer, vielversprechender Ansatz zur Fehlersuche, der sowohl die explizite als auch die symbolische Repräsentation des Zustandsraumes umfasst. Dabei werden die Zustandsräume als implizite Graphen interpretiert, die durch eine Nachfolgeerzeugungsfunktion aufgespannt werden und in denen ein möglichst kurzer Pfad als Zeuge eines Fehlers gesucht wird. Dieses Forschungsprojekt umfasst demnach die Anwendung algorithmischer Methoden der Künstlichen Intelligenz, ein Gebiet, in dem seit Jahrzehnten die gerichtete Suche in großen Zustandsräumen sehr erfolgreich eingesetzt wird. Da Problembeschreibungen in der Modellprüfung und Handlungsplanung trotz ihrer Vielfalt eine sehr starke Nähe zueinander aufweisen, wird das Spektrum der verschiedenen Lösungsmethoden in diesen Bereichen gemeinsam studiert.

• DFG Programme: Research Grants