Kombination dynamischer und formaler Methoden zur Verifikation objektorientierter Software

DSpace Repository


Dateien:

URI: http://hdl.handle.net/10900/101242
http://nbn-resolving.de/urn:nbn:de:bsz:21-dspace-1012425
http://dx.doi.org/10.15496/publikation-42621
Dokumentart: Dissertation
Date: 2020-07-31
Language: German
Faculty: 7 Mathematisch-Naturwissenschaftliche Fakultät
Department: Informatik
Advisor: Rosenstiel, Wolfgang (Prof. Dr.)
Day of Oral Examination: 2020-04-24
DDC Classifikation: 004 - Data processing and computer science
Keywords: Software , Verifikation , Testen , Korrektheit , Objektorientierung
Other Keywords: Modulare Verifikation
Kombination dynamischer und formaler Methoden
verification
testing
software
correctness
object-orientated
modular verification
combining dynamic and formal methods
ISBN: 978-3-946552-38-3
License: Creative Commons - Attribution, Non Commercial, No Derivs
Show full item record

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.
 
Erste PDF enthält Abbildungen in scharz-weiß; zweite PDF enthält farbige Abbildungen.
 

This item appears in the following Collection(s)

cc_by-nc-nd Except where otherwise noted, this item's license is described as cc_by-nc-nd