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.accessioned2020-03-09T09:22:00Z
dc.date.available2020-03-09T09:22:00Z
dc.date.issued2018-10-11
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.identifier.eissn1611-3349
dc.identifier.isbn978-3-030-02449-9
dc.identifier.isbn978-3-030-02450-5
dc.identifier.issn0302-9743
dc.identifier.urihttps://depositonce.tu-berlin.de/handle/11303/10900
dc.identifier.urihttp://dx.doi.org/10.14279/depositonce-9793
dc.language.isoenen
dc.relation.references10.14279/depositonce-7192
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subject.ddc005 Computerprogrammierung, Programme, Datende
dc.subject.otherunstructured codeen
dc.subject.otherliveness propertiesen
dc.subject.otherhandshake protocolen
dc.subject.otherformal verificationen
dc.subject.otherrefinementen
dc.titlePreserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languagesen
dc.typeConference Objecten
dc.type.versionacceptedVersionen
dcterms.bibliographicCitation.doi10.1007/978-3-030-02450-5_18en
dcterms.bibliographicCitation.originalpublishernameSpringeren
dcterms.bibliographicCitation.originalpublisherplaceChamen
dcterms.bibliographicCitation.pageend319en
dcterms.bibliographicCitation.pagestart303en
dcterms.bibliographicCitation.proceedingstitleICFEM 2018: Formal Methods and Software Engineeringen
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
tub.series.issuenumber11232en
tub.series.nameLecture Notes in Computer Scienceen

Files

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