Formal verification of low-level code in a model-based refinement process

dc.contributor.advisorGlesner, Sabine
dc.contributor.authorBerg, Nils Erik
dc.contributor.grantorTechnische Universität Berlinen
dc.contributor.refereeGlesner, Sabine
dc.contributor.refereeKönig, Barbara
dc.contributor.refereeLüttgen, Gerald
dc.date.accepted2019-05-10
dc.date.accessioned2019-10-21T13:07:26Z
dc.date.available2019-10-21T13:07:26Z
dc.date.issued2019
dc.description.abstractEmbedded 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.en
dc.description.abstractEingebettete 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.de
dc.description.sponsorshipDFG, 20128325, Konstruktion und Verifikation eingebetteter echtzeitfähiger Steuerungssoftware und ihrer Transformation in ausführbaren Code unter besonderer Berücksichtigung von Multicore und Adaptivitäten
dc.identifier.urihttps://depositonce.tu-berlin.de/handle/11303/9593
dc.identifier.urihttp://dx.doi.org/10.14279/depositonce-8638
dc.language.isoenen
dc.relation.referenceshttp://dx.doi.org/10.14279/depositonce-8636
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/en
dc.subject.ddc005 Computerprogrammierung, Programme, Datende
dc.subject.othercommunicating sequential processesen
dc.subject.otherunstructured codeen
dc.subject.otherformal semanticsen
dc.subject.otherliveness propertiesen
dc.subject.otherhoare calculusen
dc.subject.otherrefinementen
dc.subject.otherunstrukturiertes Programmde
dc.subject.otherformale Semantikde
dc.subject.otherHoare-Kalkülde
dc.subject.otherVerfeinerungde
dc.titleFormal verification of low-level code in a model-based refinement processen
dc.title.translatedFormale Verifikation von Low-Level Programmen im Rahmen eines modellbasierten Verfeinerungsprozessesde
dc.typeDoctoral Thesisen
dc.type.versionacceptedVersionen
tub.accessrights.dnbfreeen
tub.affiliationFak. 4 Elektrotechnik und Informatik::Inst. Technische Informatik und Mikroelektronikde
tub.affiliation.facultyFak. 4 Elektrotechnik und Informatikde
tub.affiliation.instituteInst. Technische Informatik und Mikroelektronikde
tub.publisher.universityorinstitutionTechnische Universität Berlinen

Files

Original bundle
Now showing 1 - 1 of 1
Loading…
Thumbnail Image
Name:
berg_nils.pdf
Size:
1.41 MB
Format:
Adobe Portable Document Format
Description:
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
4.9 KB
Format:
Item-specific license agreed upon to submission
Description:

Collections