Spisländer M (2019)
Publication Language: German
Publication Type: Thesis
Publication year: 2019
URI: https://opus4.kobv.de/opus4-fau/frontdoor/index/index/docId/10445
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.
APA:
Spisländer, M. (2019). Strukturelle Testverfahren zur Verifikation existentieller temporallogischer Formeln in erweiterten endlichen Zustandsmaschinen (Dissertation).
MLA:
Spisländer, Marc. Strukturelle Testverfahren zur Verifikation existentieller temporallogischer Formeln in erweiterten endlichen Zustandsmaschinen. Dissertation, 2019.
BibTeX: Download