Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-4137
Main Title: A mechanized verification environment for real-time process algebras and low-level programming languages
Translated Title: Eine mechanisierte Verifikationsumgebung für zeitbehaftete Prozessalgebren und Low-Level Programmiersprachen
Author(s): Bartels, Björn
Advisor(s): Glesner, Sabine
Referee(s): Glesner, Sabine
Olderog, Ernst-Rüdiger
Jähnichen, Stefan
Granting Institution: Technische Universität Berlin, Fakultät IV - Elektrotechnik und Informatik
Type: Doctoral Thesis
Language: English
Language Code: en
Abstract: Eingebettete und reaktive Echtzeitsysteme sind heutzutage oft verteilt implementiert und werden in sich dynamisch ändernden Umgebungen eingesetzt. Ihre Nutzung in sicherheitskritischen Umgebungen erfordert, dass diese Systeme neben funktionalen Eigenschaften oft auch nicht-funktionalen Eigenschaften, wie z.B. Echtzeiteigenschaften, genügen müssen. Um besonders wichtige Eigenschaften formal nachweisen zu können, modellieren Entwicklingsprozesse für derartige Systeme diese auf verschiedenen Abstraktionsebenen mit potentiell unterschiedlichen Formalismen und Sprachen. Zeitbehaftete Prozesskalküle beispielsweise ermöglichen den Nachweis kritischer Eigenschaften auf verschiedenen Abstraktionsebenen. Es stellt sich allerdings noch immer problematisch dar, für Implementierungen in einer unstrukturierten Programmiersprache formal nachzuweisen, dass diese sich korrekt hinsichtlich einer abstrakten Spezifikation verhalten und auch deren Eigenschaften bewahren. In dieser Arbeit präsentieren wir eine mechanisierte Verifikationsumgebung für eingebettete Echtzeitsysteme. Diese ermöglicht die maschinelle und kompositionale Verifikation der Konformität zwischen abstrakten Spezifikationen im Prozesskalkül Timed CSP und Implementierungen in einer maschinennahen und unstrukturierten Sprache. Auf Ebene der prozess-algebraischen Spezifikationen nutzen wir eine bestehende Mechanisierung der operationalen Semantik von Timed CSP im Theorembeweiser Isabelle/HOL. Auf Implementierungsebene bauen wir auf eine kompositionale Semantik und einen zugehörigen Hoare-Kalkül für eine minimalistische unstrukturierte Sprache auf. Diese erweitern wir um Nichtdeterminismus und Echtzeiteigenschaften und stellen maschinengestützte Beweise für Korrektheit und Vollständigkeit sowohl für den Fall der partiellen Korrektheit, als auch für den Fall der totalen Korrektheit bereit. Wir ermöglichen den maschinengestützten Nachweis der Konformität einer Implementierung hinsichtlich ihrer abstrakten Spezifikation basierend auf dem Begriff der schwachen zeitbehafteten Bisimulation. Hierzu leiten wir ausgehend von der operationalen Semantik unserer low-level Sprache formal ein zeitbehaftetes und markiertes Transitionssystem ab. Wir stellen Theoreme bereit, die es ermöglichen, Aussagen unserer Programmlogik in Konformitäts- beweisen zu nutzen. Dadurch erhöhen wir die Wiederverwendbarkeit von Beweisen. Weiterhin präsentieren wir einen Ansatz zur Spezifikation und Verifikation von verteilten und adaptiven Systemen in CSP, welcher es ermöglicht funktionale und adaptive Aspekte eines Systems getrennt voneinander zu spezifizieren und zu analysieren. Die mittels dieses Ansatzes etablierten Eigenschaften lassen sich dann durch unserere Konformitätsrelation von der abstrakten Ebene auf die Implementierungsebene einer unstrukturierten Sprache transferieren. Die unserem Ansatz zugrunde liegende Theorie formalisieren wir im Theorembeweiser Isabelle/HOL. Dadurch wird die Korrektheit unserer Verifikationsumgebung sichergestellt. Weiterhin erhalten wir eine maschinengestützte Verifikationsumgebung für die kompositionale und mechanisierte Verifikation von Konformitätsrelationen zwischen low-level Programmen und ihren prozess-algebraischen Spezifikationen in sich dynamisch ändernden Umgebungen.
Nowadays, embedded and reactive real-time systems are often also distributed and operate in dynamically changing environments. Furthermore, these systems handle safety-critical tasks and therefore have to satisfy critical functional and non-functional requirements like, for example, real-time requirements. During development, such systems are often modeled on different levels of abstraction using different formalisms or languages in order to facilitate the verification of crucial properties. Timed process-algebraic formalisms like Timed CSP are well-suited for reasoning about properties of distributed systems on different levels of abstraction. However, it is still a challenging task to establish that implementations given in an unstructured low-level programming language correctly implement the respective process-algebraic specifications. The main challenge is to find a way of overcoming the semantic gap introduced by the different levels of abstraction that ensures that properties established on the higher levels of abstraction are preserved. In this thesis, we address this problem by developing a mechanized framework that enables the compositional verification of formal relations between timed process-algebraic specifications given in Timed CSP and their implementations given in a low-level programming language. On the level of process-algebraic specifications, we build on an existing mechanization of the operational semantics of Timed CSP in the theorem prover Isabelle/HOL. On the level of programming languages, our framework provides a mechanization and extension of an existing compositional big-step semantics and a Hoare-logic for a basic low-level language. We extend the semantics and the Hoare-logic to support non-determinism and real-time properties and provide mechanized soundness and completeness proofs for the partial and total correctness cases. For proofs about conformance between abstract specifications in Timed CSP and their implementations in the extended low-level language, we use the notion of weak timed bisimulation. As a basis for this relation, we formally derive a labeled transition system from the unlabeled transition system induced by the operational semantics of the extended low-level language. We show how our framework supports the transfer of verification results established using our proof calculus in order to discharge verification conditions resulting from conformance proofs. Furthermore, we provide a CSP-based approach for the specification and verification of distributed reactive systems, which adapt their behavior to changes in their environment. In this modeling approach, the notion of refinement in CSP is exploited to realize a layered specification approach separating the functional behavior of a system from its internal reconfiguration processes. We have formalized the underlying theory of our approach using the Isabelle/HOL theorem prover. This enables us to mechanically verify all results of this thesis and ensures that critical corner cases are not overlooked. At the same time, we thereby provide a machine-assisted verification environment that enables the mechanized compositional verification of conformance relations between low-level code and timed process-algebraic specifications in dynamically changing environments.
URI: urn:nbn:de:kobv:83-opus4-55430
http://depositonce.tu-berlin.de/handle/11303/4434
http://dx.doi.org/10.14279/depositonce-4137
Exam Date: 10-Apr-2014
Issue Date: 4-Aug-2014
Date Available: 4-Aug-2014
DDC Class: 000 Informatik, Informationswissenschaft, allgemeine Werke
Subject(s): Formale Verifikation
Low-Level Programme
Prozessalgebren
Konformitätsrelationen
Formal verification
low-level code
process-algebras
conformance relation
Usage rights: Terms of German Copyright Law
Appears in Collections:Institut für Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:
File Description SizeFormat 
bartels_bjoern.pdf3.23 MBAdobe PDFThumbnail
View/Open


Items in DepositOnce are protected by copyright, with all rights reserved, unless otherwise indicated.