Strukturelle Testverfahren zur Verifikation existentieller temporallogischer Formeln in erweiterten endlichen Zustandsmaschinen

Language
de
Document Type
Doctoral Thesis
Issue Date
2019-02-18
Issue Year
2019
Authors
Spisländer, Marc
Editor
Abstract

Im Rahmen dieser Arbeit wird ein Verfahren zur Verifikation existentieller und universeller temporallogischer Formeln in erweiterten endlichen Zustandsmaschinen vorgestellt. Da aufgrund der Turing-Vollständigkeit letzterer die Möglichkeit systematischer, automatisierter Verifikationsmethoden ausscheidet, besteht der Ansatz in dieser Arbeit aus einer Kombination zwischen einer formalen und einer informalen, heuristikbasierten Herangehensweise. Dazu wird das Verifikationsproblem in ein Überdeckungsproblem transformiert, indem zunächst ausgehend von der zu untersuchenden Maschine und der zu verifizierenden Formel eine neue erweiterte endliche Zustandsmaschine konstruiert wird. Anschließend werden bezüglich dieser neuen Maschine strukturelle Testüberdeckungskriterien definiert, für die bewiesen wird, dass deren Erfüllbarkeit Rückschlüsse über die Gültigkeit der betrachteten Formel erlauben. Zur tatsächlichen Erfüllung der eingeführten Überdeckungskriterien wird ein auf bereits bekannten Arbeiten basierendes, heuristisches Verfahren zur automatisierten Generierung entsprechender kriteriumerfüllender Testdaten entwickelt. Um seine Praktikabilität zu demonstrieren, wurde das in der Arbeit entwickelte Verfahren in Form eines Werkzeugs implementiert und zur Verifikation eines Systems bestehend aus autonomen, kooperierenden Robotern angewendet.

DOI
Faculties & Collections
Zugehörige ORCIDs