TY  - THES
AB  - Viele Alltagsgegenstände führen Software aus. Daher sollte sie fehlerfrei sein. Firmen betreiben viel Aufwand, .z.B. formale Verifikation, um Fehler in der Software zu eliminieren oder deren Abwesenheit zu zeigen. Software aufwändig validiert wurde, kann bedenkenlos installiert werden.Früher installierten Verbraucher Software aus großen Softwarehäusern, von denen sie Software bereits nutzten. Aufgrund langzeitiger Geschäftsbeziehung konnten Verbraucher die Softwarequalität dieser Hersteller abschätzen. Heute wird Software vermehrt von unbekannten Entwicklern geschrieben. Daher kann nicht erwartet werden, dass der Verbraucher auf die Fehlerfreiheit der Software vertraut.In dieser Arbeit entwickeln wir Techniken, die ohne Vertrauen in den Hersteller auskommen und den Verbraucher von der Fehlerfreiheit einer Software überzeugen. Die Techniken basieren auf formaler Verifikation, sind automatisch und können an die zu prüfende Eigenschaft und die Verifikationstechnik angepasst werden. Die Idee ist, dass der Hersteller die Informationen aus der aufwändigen Verifikation nutzt, um die Nachprüfung des Verbrauchers zu vereinfachen. Wir verfolgen zwei Ansätze, und deren Integration. In der konfigurierbaren Programmzertifizierung liefert der Hersteller das Programm und ein Zertifikat (Teile des Verifikationsbeweises). Der Verbraucher prüft, ob das Zertifikat bezeugt, dass die Verifikation erfolgreich war. Das Konzept Programs from Proofs nutzt die Informationen der Verifikation, um ein Programm zu erzeugen, dass der Verbraucher mit einer Datenflussanalyse verifizieren kann. Wir beweisen für alle Techniken, dass im Falle einer erfolgreichen Nachprüfung das Softwareprodukt die geprüfte Eigenschaft erfüllt, und, dass die Nachprüfung bei regelkonformen Produzenten erfolgreich ist. Alle Techniken wurden auch praktisch evaluiert.
AU  - Jakobs, Marie-Christine
CY  - Paderborn
DA  - 2017
DO  - 10.17619/UNIPB/1-104
DP  - Universität Paderborn
LA  - eng
N1  - Tag der Verteidigung: 05.05.2017
N1  - Universität Paderborn, Dissertation, 2017
PB  - Veröffentlichungen der Universität
PY  - 2017
SP  - 1 Online-Ressource (XI, 352 Seiten)
T2  - Institut für Informatik
TI  - On-The-Fly safety checking - customizing program certification and program restructuring
UR  - https://nbn-resolving.org/urn:nbn:de:hbz:466:2-28514
Y2  - 2026-01-17T12:02:05
ER  -