Kombination dynamischer und formaler Methoden zur Verifikation objektorientierter Software

DSpace Repositorium (Manakin basiert)


Dateien:

Zitierfähiger Link (URI): http://hdl.handle.net/10900/106716
http://nbn-resolving.de/urn:nbn:de:bsz:21-dspace-1067162
http://dx.doi.org/10.15496/publikation-48094
Dokumentart: Dissertation
Erscheinungsdatum: 2020-09
Sprache: Deutsch
Fakultät: 7 Mathematisch-Naturwissenschaftliche Fakultät
Fachbereich: Informatik
Gutachter: Rosenstiel, Wolfgang (Prof. Dr.)
Tag der mündl. Prüfung: 2020-04-24
DDC-Klassifikation: 004 - Informatik
Schlagworte: Software , Verifikation , Testen , Korrektheit , Objektorientierung
Freie Schlagwörter: Modulare Verifikation
Kombination dynamischer und formaler Methoden
testing
software
verification
correctness
object-orientated
modular verification
combining dynamic and formal methods
ISBN: 978-3-946552-38-3
Lizenz: http://creativecommons.org/licenses/by-nc-nd/3.0/de/deed.de http://creativecommons.org/licenses/by-nc-nd/3.0/de/deed.en
Zur Langanzeige

Inhaltszusammenfassung:

 
Der Anteil von Software in industriellen Gütern und Dienstleistungen steigt stetig und deren Korrektheit ist eine deren wichtigsten Eigenschaften. Häufig werden für die Entwicklung objektorientierte Programmiersprachen eingesetzt. Die Korrektheit objektorientierter Software kann mit Hilfe dynamischer Testverfahren oder mit Hilfe formaler Methoden verifiziert werden. Dynamische Testverfahren können leicht auf jede Software angewandt werden, garantieren jedoch keine Fehlerfreiheit. Methoden der formalen Verifikation können hingegen dafür genutzt werden, Fehlerfreiheit zu garantieren. Jedoch ist ihre Anwendung wesentlich komplexer. In dieser Arbeit wird ein neues Verfahren zu Kombination modularer, formaler Verifikationsmethoden und dynamischer Testverfahren vorgestellt. Das Ziel der vorgestellten Methodik ist es möglichst große Anteile der Software automatisiert, modular und formal zu verifizieren. Dadurch können zeitintensive, dynamische Testfälle eingespart und die Sicherheit der Software erhöht werden. Die Korrektheit von Programmabschnitten, die nicht formal verifiziert werden konnten, wird mit dynamischen Testfällen und Robustheitstests überprüft. Die Robustheitstests simulieren Fehler bezüglich aller nicht formal verifizierten Programmeigenschaften. Mit Hilfe dieser Tests wird das Verhalten der formal verifizierten Programmabschnitte im Fehlerfall analysiert. Ein sicherer Umgang mit Fehlern verhindert, dass Fehler unbemerkt durch das Gesamtsystem propagiert werden können. Stattdessen werden Fehler durch das Programm korrigiert oder die Programmausführung mit einem definierten Prozess unterbrochen. Die Robustheitstests helfen dem Entwickler, die notwendige Fehlerbehandlung zu identifizieren, zu entwickeln und final zu testen. Die auf diesem Weg entstandene Fehlerbehandlung erhöht auch die Robustheit des Gesamtsystems gegenüber potentiell nicht entdeckter Fehler.
 
2. Auflage (mit farbigen Abbildungen)
 

Das Dokument erscheint in:

cc_by-nc-nd Solange nicht anders angezeigt, wird die Lizenz wie folgt beschrieben: cc_by-nc-nd