Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-7192
For citation please use:
Main Title: Technical Report accompanying: Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages
Translated Title: Technischer Bericht, begleitend für: Erhalt von Lebendigkeitseigenschaften von synchroner Kommunikation bei der Implementierung in asynchronen, unstrukturierten Low-Level-Sprachen
Author(s): Berg, Nils
Göthel, Thomas
Danziger, Armin
Glesner, Sabine
Type: Report
Is Part Of: 10.14279/depositonce-8638
Language Code: en
Abstract: In the implementation of abstract synchronous communication in asynchronous unstructured low-level languages, e. g., using shared variables, the preservation of safety and especially liveness properties is a hitherto open problem due to inherently different abstraction levels. Our approach to overcome this problem is threefold: First, we present our notion of handshake refinement with which we formally prove the correctness of the implementation relation of a handshake protocol. Second, we verify the soundness of our handshake refinement, i. e., all safety and liveness properties are preserved to the lower level. Third, we apply our handshake refinement to show the correctness of all implementations that realize the abstract synchronous communication with the handshake protocol. To this end, we employ an exemplary language with asynchronous shared variable communication. Our approach is scalable and closes the verification gap between different abstraction levels of communication.
Bei der Implementierung von abstrakter, synchroner Kommunikation in asynchronen, unstrukturierten Low-Level-Sprachen, zum Beipspiel mit Hilfe von geteilten Variablen, ist die Erhaltung von Sicherheits- und Lebendigkeitseigenschaften ein bis dato ein ungelöstes Problem aufgrund der verschiedenen Abstraktionsstufen. Unser Ansatz um dieses Problem zu lösen ist dreiteilig: Zu erst stellen wir unseren Begriff der Handschlag-Verfeinerung vor, mit dem wir die Korrektheit von Implementierungen, die das Handschlag-Protokoll benutzen, zeigen können. Zweitens weisen wir nach, dass die Handschlag-Verfeinerung die Sicherheits- und Lebendigkeitseigenschaften erhält. Drittens, zeigen wir das alle Programme, die synchrone Kommunikation mit dem Handschlag-Protokoll implementieren, korrekt sind. Wir verwenden dazu eine beispielhafte Sprache mit asynchroner Kommunikation mit Hilfe von geteilten Variablen. Unser Ansatz ist skalierbar und schließt die Verifikationslücke zwischen den verschiedenen Abstraktionsstufen der Kommunikation.
URI: https://depositonce.tu-berlin.de//handle/11303/8028
http://dx.doi.org/10.14279/depositonce-7192
Issue Date: 2020
Date Available: 5-Mar-2020
DDC Class: 005 Computerprogrammierung, Programme, Daten
Subject(s): communicating sequential processes
unstructured code
formal semantics
liveness properties
refinement
unstrukturiertes Programm
formale Semantik
Verfeinerung
formale Verifikation
License: https://creativecommons.org/licenses/by/4.0/
Appears in Collections:FG Software and Embedded Systems Engineering » Publications

Files in This Item:
berg_etal_2020.pdf
Format: Adobe PDF | Size: 404.33 kB
DownloadShow Preview
Thumbnail

Item Export Bar

This item is licensed under a Creative Commons License Creative Commons