Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-8638
Main Title: Formal verification of low-level code in a model-based refinement process
Translated Title: Formale Verifikation von Low-Level Programmen im Rahmen eines modellbasierten Verfeinerungsprozesses
Author(s): Berg, Nils Erik
Advisor(s): Glesner, Sabine
Referee(s): Glesner, Sabine
König, Barbara
Lüttgen, Gerald
Granting Institution: Technische Universität Berlin
Type: Doctoral Thesis
References: http://dx.doi.org/10.14279/depositonce-8636
Language Code: en
Abstract: Embedded systems often control safety critical environments, such as cars, airplanes, traffic control, or pacemakers. Embedded systems are often non-terminating and communicating. To confine the complexity of those systems (e.g. introduced by communication details), comprehensive verification and simulation is usually done on an abstract model (e.g. a formal specification) instead of the implemented system itself. However, it is still an open problem how to relate the actual executable low-level code with the abstract models. In industrial practice, embedded systems in safety critical areas are commonly designed with model-based approaches. The model-based development of (embedded) systems starts with the verification (or simulation) of properties on an abstract model. There are two important categories of properties: safety properties, which exclude bad behavior, and liveness properties, which ensure good behavior. The abstract model is implemented and/or compiled to executable low-level code, but there is a large verification gap between the model whose properties are verified and the system that is actually executed. Both manual implementation and the compilation process are complex and error prone. Furthermore, complexity of the verification rises even higher when concurrent systems that communicate with each other are developed. We address the problem that the executed low-level code is not guaranteed to have the same safety and liveness properties as the abstract model. To overcome this problem, we present a formal framework that enables rigorous verification of preservation of safety and liveness properties from an abstract model to low-level code. The key idea of our approach is to divide the relation between abstract model and low-level code into two steps to achieve compositionality: - A compositional relation between the abstract model and an intermediate model, and - a non-compositional relation between the intermediate model and the low-level code. This separation enables us to reason compositionally about the first half, relating the abstract model and the intermediate model, and use a general theorem for the second half, which results in an overall compositional verification. With our framework, we enable the verification of the conformance of a program in low-level code to its Communicating Sequential Processes (CSP) specification, \ie that all safety and liveness properties are preserved. To this end, we have transferred and extended the notion of CSP refinement to also cover low-level code. To separate the verification into two steps, we define our low-level language with abstract communication Communicating Unstructured Code (CUC) as intermediate model. To relate the specification in CSP and the intermediate model in CUC, we present a Hoare calculus which allows us to reason over the communication behavior of a (possibly non-terminating) CUC program. To relate the intermediate model in CUC with our low-level language Shared Variables (SV), we define our notion of \vhb and prove in a general theorem the preservation of both safety and liveness properties for related CUC and SV programs. Our formalization in a theorem prover enables users to mechanize and reuse their proofs. Together with the compositionality of our approach, this makes it possible to provide rigorous guarantees of concurrent low-level programs in a way that scales with the number of components.
Eingebettete Systeme steuern häufig sicherheitskritische Umgebungen wie z.B. Autos, Flugzeuge, Verkehrssteuerungen oder Herzschrittmacher. Eingebettete Systeme sind oft nicht-terminierend und kommunizieren miteinander. Um die Komplexität dieser Systeme (die z.B. durch Kommunikationsdetails entsteht) in den Griff zu bekommen, werden normalerweise abstraktere Modelle (z.B. in Form einer formalen Spezifikation) zur Verifikation oder Simulation herangezogen anstelle des Systems selbst. Den ausführbaren Low-Level-Code mit den abstrakten Modellen in Beziehung zu setzen ist ein noch ungelöstes Problem. In der industriellen Praxis werden eingebettete Systeme in sicherheitskritischen Bereichen im Allgemeinen mit modellbasierten Ansätzen entworfen. Die modellbasierte Entwicklung von (eingebetteten) Systemen beginnt mit der Verifikation (oder Simulation) von Eigenschaften eines abstrakten Modells. Es gibt zwei wichtige Kategorien von Eigenschaften: Sicherheitseigenschaften, die unerwünschtes Verhalten ausschließen, und Lebendigkeitseigenschaften, die erwünschtes Verhalten gewährleisten. Das abstrakte Modell wird durch implementieren und/oder kompilieren in ausführbaren Low-Level-Code überführt. Jedoch ist der Erhalt der Eigenschaften vom abstrakten Modell hin zum tatsächlich ausgeführten System nicht gesichert; es entsteht die sogenannte Verifikationslücke. Um diese Verifikationslücke zu schließen, stellen wir ein formales Framework vor, das die rigorose Verifikation der Erhaltung der Sicherheits- und Lebendigkeitseigenschaften von einem abstrakten Modell bis hin zum Low-Level-Code ermöglicht. Die Kernidee unseres Ansatzes besteht darin, die Beziehung zwischen dem abstrakten Modell und dem Low-Level-Code in zwei Schritte zu unterteilen, um so Kompositionalität zu erreichen: - Eine Relation zwischen dem abstrakten Modell und einem Zwischenmodell und - eine weitere Relation zwischen dem Zwischenmodell und dem Low-Level-Code. Diese Unterteilung erlaubt es uns, kompositional über Relation vom abstrakten Modell zum Zwischenmodell zu argumentieren, und ein allgemeingültiges Theorem für die zweite Hälfte zu verwenden. Insgesamt ist so eine kompositionale Verifikation möglich. Unser Framework ermöglicht die Verifikation der Konformität eines Programms in Low-Level-Code zu seiner Spezifikation in Communicating Sequential Processes (CSP), d.h., dass alle Sicherheits- und Lebendigkeitseigenschaften erhalten bleiben. Zu diesem Zweck haben wir den Begriff der CSP-Verfeinerung auf Low-Level-Code übertragen und erweitert. Um die Verifizierung in zwei Schritte zu unterteilen, definieren wir als Zwischenmodell unsere Low-Level Sprache mit abstrakter Kommunikation Communicating Unstuctured Code (CUC). Um die Spezifikation in CSP und das Zwischenmodell in CUC in Beziehung zu setzen, stellen wir einen Hoare-Kalkül vor, der die Verifikation von Kommunikationsverhalten eines (möglicherweise nicht-terminierenden) CUC-Programms ermöglicht. Um das Zwischenmodell in CUC mit unserer Low-Level Sprache Shared Variables (SV) in Verbindung zu bringen, definieren wir unseren Begriff der Handshake-Verfeinerung und beweisen in einem allgemeingültigen Theorem den Erhalt von Sicherheits- und Lebendigkeitseigenschaften für in Beziehung stehende CUC- und SV-Programme. Unsere Formalisierung in einem Theorembeweiser ermöglicht es dem Benutzer, Beweise zu mechanisieren und wiederzuverwenden. Zusammen mit der Kompositionalität unseres Ansatzes ermöglichen wir, rigoros Eigenschaften für Low-Level-Programme zu garantieren, und zwar gut skalierbar mit der Anzahl der nebenläufigen Komponenten des Systems.
URI: https://depositonce.tu-berlin.de/handle/11303/9593
http://dx.doi.org/10.14279/depositonce-8638
Exam Date: 10-May-2019
Issue Date: 2019
Date Available: 21-Oct-2019
DDC Class: 005 Computerprogrammierung, Programme, Daten
Subject(s): communicating sequential processes
unstructured code
formal semantics
liveness properties
hoare calculus
refinement
unstrukturiertes Programm
formale Semantik
Hoare-Kalkül
Verfeinerung
Sponsor/Funder: DFG, 20128325, Konstruktion und Verifikation eingebetteter echtzeitfähiger Steuerungssoftware und ihrer Transformation in ausführbaren Code unter besonderer Berücksichtigung von Multicore und Adaptivität
License: https://creativecommons.org/licenses/by/4.0/
Appears in Collections:Inst. Technische Informatik und Mikroelektronik » Publications

Files in This Item:
File Description SizeFormat 
berg_nils.pdf1.44 MBAdobe PDFThumbnail
View/Open


This item is licensed under a Creative Commons License Creative Commons