Directed model checking with AI exploration algorithms

点击翻译按钮获取中文摘要

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.