Technical Report accompanying: Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages
| dc.contributor.author | Berg, Nils | |
| dc.contributor.author | Göthel, Thomas | |
| dc.contributor.author | Danziger, Armin | |
| dc.contributor.author | Glesner, Sabine | |
| dc.date.accessioned | 2018-07-23T08:12:19Z | |
| dc.date.available | 2020-03-05T08:12:19Z | |
| dc.date.issued | 2020 | |
| dc.description.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. | en |
| dc.description.abstract | 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. | de |
| dc.identifier.uri | https://depositonce.tu-berlin.de/handle/11303/8028 | |
| dc.identifier.uri | http://dx.doi.org/10.14279/depositonce-7192 | |
| dc.language.iso | en | en |
| dc.relation.ispartof | 10.14279/depositonce-8638 | |
| dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | en |
| dc.subject.ddc | 005 Computerprogrammierung, Programme, Daten | en |
| dc.subject.other | communicating sequential processes | en |
| dc.subject.other | unstructured code | en |
| dc.subject.other | formal semantics | en |
| dc.subject.other | liveness properties | en |
| dc.subject.other | refinement | en |
| dc.subject.other | unstrukturiertes Programm | de |
| dc.subject.other | formale Semantik | de |
| dc.subject.other | Verfeinerung | de |
| dc.subject.other | formale Verifikation | de |
| dc.title | Technical Report accompanying: Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages | en |
| dc.title.translated | Technischer Bericht, begleitend fĂĽr: Erhalt von Lebendigkeitseigenschaften von synchroner Kommunikation bei der Implementierung in asynchronen, unstrukturierten Low-Level-Sprachen | de |
| dc.type | Report | en |
| dc.type.version | publishedVersion | en |
| tub.accessrights.dnb | free | en |
| tub.affiliation | Fak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik::FG Software and Embedded Systems Engineering | de |
| tub.affiliation.faculty | Fak. 4 Elektrotechnik und Informatik | de |
| tub.affiliation.group | FG Software and Embedded Systems Engineering | de |
| tub.affiliation.institute | Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.publisher.universityorinstitution | Technische Universität Berlin | en |