Please use this identifier to cite or link to this item:
For citation please use:
Main Title: Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages
Author(s): Berg, Nils
Göthel, Thomas
Danziger, Armin
Glesner, Sabine
Type: Conference Object
References: 10.14279/depositonce-7192
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.
Issue Date: 11-Oct-2018
Date Available: 9-Mar-2020
DDC Class: 005 Computerprogrammierung, Programme, Daten
Subject(s): unstructured code
liveness properties
handshake protocol
formal verification
Proceedings Title: ICFEM 2018: Formal Methods and Software Engineering
Publisher: Springer
Publisher Place: Cham
Publisher DOI: 10.1007/978-3-030-02450-5_18
Page Start: 303
Page End: 319
Series: Lecture Notes in Computer Science
Series Number: 11232
EISSN: 1611-3349
ISBN: 978-3-030-02449-9
ISSN: 0302-9743
Appears in Collections:FG Software and Embedded Systems Engineering » Publications

Files in This Item:

Accepted manuscript

Format: Adobe PDF | Size: 898.85 kB
DownloadShow Preview

Item Export Bar

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