A Formal Verification Environment for Use in the Certification of Safety-Related C Programs
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
00101756-1.pdf | 2.32 MB | Adobe PDF | Anzeigen |
Sonstige Titel: | Eine formale Verifikationsumgebung zur Verwendung bei der Zertifizierung von sicherheitsbezogenen C-Programmen | Autor/Autorin: | Walter, Dennis | BetreuerIn: | Lüth, Christoph | 1. GutachterIn: | Lüth, Christoph | Weitere Gutachter:innen: | Peleska, Jan ![]() |
Zusammenfassung: | In this thesis the design of an environment for the formal verification of functional properties of safety-related software written in the programming language C is described. The focus lies on the verification of (primarily) geometric computations. We give an overview of the applicable regulations for safety-related software systems. We define a combination of higher-order logic as formalised in the theorem prover Isabelle and a specification language syntactically based on C expressions. The language retains the mathematical character of higher-level specifications in code specifications. A memory model for C is formalised which is appropriate to model low-level memory operations while keeping the entailed verification overhead in tolerable bounds. Finally, a Hoare style proof calculus is devised so that correctness proofs can be performed in one integrated framework. The applicability of the approach is demonstrated by describing its use in an industrial project. |
Schlagwort: | verification; certification; formal methods; safety-related software; robotics; Isabelle; theorem proving; IEC 61508 | Veröffentlichungsdatum: | 16-Nov-2010 | Dokumenttyp: | Dissertation | Zweitveröffentlichung: | no | URN: | urn:nbn:de:gbv:46-00101756-18 | Institution: | Universität Bremen | Fachbereich: | Fachbereich 03: Mathematik/Informatik (FB 03) |
Enthalten in den Sammlungen: | Dissertationen |
Seitenansichten
488
checked on 02.04.2025
Download(s)
162
checked on 02.04.2025
Google ScholarTM
Prüfe
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.