Technical Report accompanying: Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages

dc.contributor.authorBerg, Nils
dc.contributor.authorGöthel, Thomas
dc.contributor.authorDanziger, Armin
dc.contributor.authorGlesner, Sabine
dc.date.accessioned2018-07-23T08:12:19Z
dc.date.available2020-03-05T08:12:19Z
dc.date.issued2020
dc.description.abstractIn 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.abstractBei 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.urihttps://depositonce.tu-berlin.de/handle/11303/8028
dc.identifier.urihttp://dx.doi.org/10.14279/depositonce-7192
dc.language.isoenen
dc.relation.ispartof10.14279/depositonce-8638
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/en
dc.subject.ddc005 Computerprogrammierung, Programme, Datenen
dc.subject.othercommunicating sequential processesen
dc.subject.otherunstructured codeen
dc.subject.otherformal semanticsen
dc.subject.otherliveness propertiesen
dc.subject.otherrefinementen
dc.subject.otherunstrukturiertes Programmde
dc.subject.otherformale Semantikde
dc.subject.otherVerfeinerungde
dc.subject.otherformale Verifikationde
dc.titleTechnical Report accompanying: Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languagesen
dc.title.translatedTechnischer Bericht, begleitend für: Erhalt von Lebendigkeitseigenschaften von synchroner Kommunikation bei der Implementierung in asynchronen, unstrukturierten Low-Level-Sprachende
dc.typeReporten
dc.type.versionpublishedVersionen
tub.accessrights.dnbfreeen
tub.affiliationFak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik::FG Software and Embedded Systems Engineeringde
tub.affiliation.facultyFak. 4 Elektrotechnik und Informatikde
tub.affiliation.groupFG Software and Embedded Systems Engineeringde
tub.affiliation.instituteInst. Softwaretechnik und Theoretische Informatikde
tub.publisher.universityorinstitutionTechnische Universität Berlinen

Files

Original bundle
Now showing 1 - 1 of 1
Loading…
Thumbnail Image
Name:
berg_etal_2020.pdf
Size:
404.33 KB
Format:
Adobe Portable Document Format
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