Kombination dynamischer und formaler Methoden zur Verifikation objektorientierter Software

DSpace Repositorium (Manakin basiert)

Zur Kurzanzeige

dc.contributor.advisor Rosenstiel, Wolfgang (Prof. Dr.)
dc.contributor.author Huster, Stefan
dc.date.accessioned 2020-06-04T11:34:23Z
dc.date.available 2020-06-04T11:34:23Z
dc.date.issued 2020-07-31
dc.identifier.isbn 978-3-946552-38-3 de_DE
dc.identifier.other 1725979535 de_DE
dc.identifier.uri http://hdl.handle.net/10900/101242
dc.identifier.uri http://nbn-resolving.de/urn:nbn:de:bsz:21-dspace-1012425 de_DE
dc.identifier.uri http://dx.doi.org/10.15496/publikation-42621
dc.description.abstract 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. de_DE
dc.description.abstract Erste PDF enthält Abbildungen in scharz-weiß; zweite PDF enthält farbige Abbildungen. de_DE
dc.language.iso de de_DE
dc.publisher Universität Tübingen de_DE
dc.rights cc_by-nc-nd de_DE
dc.rights.uri http://creativecommons.org/licenses/by-nc-nd/3.0/de/deed.de de_DE
dc.rights.uri http://creativecommons.org/licenses/by-nc-nd/3.0/de/deed.en en
dc.subject.classification Software , Verifikation , Testen , Korrektheit , Objektorientierung de_DE
dc.subject.ddc 004 de_DE
dc.subject.other Modulare Verifikation de_DE
dc.subject.other Kombination dynamischer und formaler Methoden de_DE
dc.subject.other verification en
dc.subject.other testing en
dc.subject.other software en
dc.subject.other correctness en
dc.subject.other object-orientated en
dc.subject.other modular verification en
dc.subject.other combining dynamic and formal methods en
dc.title Kombination dynamischer und formaler Methoden zur Verifikation objektorientierter Software de_DE
dc.type PhDThesis de_DE
dcterms.dateAccepted 2020-04-24
utue.publikation.fachbereich Informatik de_DE
utue.publikation.fakultaet 7 Mathematisch-Naturwissenschaftliche Fakultät de_DE

Dateien:

Das Dokument erscheint in:

Zur Kurzanzeige

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