Please use this identifier to cite or link to this item:
For citation please use:
Main Title: Refinement-Based Verification of Communicating Unstructured Code
Author(s): Jähnig, Nils
Göthel, Thomas
Glesner, Sabine
Type: Conference Object
Language Code: en
Abstract: Formal model refinement aims at preserving safety and liveness properties of models. However, there is usually a verification gap between model and executed code, especially if concurrent processes are involved. The reason for this is that a manual implementation and further code optimizations can introduce implementation errors. In this paper, we present a framework that allows for formally proving a failures refinement between a CSP specification and its low-level implementation. The implementation is given in a generic unstructured language with gotos and an abstract communication instruction. We provide a failures-based denotational semantics of it with an appropriate Hoare calculus. Since failures-based refinement is compositional w.r.t. parallel composition of concurrent components and preserves safety and liveness properties, this contributes to reducing the verification gap between high-level specifications and their low-level implementations.
Issue Date: 23-Jun-2016
Date Available: 9-Mar-2020
DDC Class: 005 Computerprogrammierung, Programme, Daten
Subject(s): gotos
unstructured code
formal semantics
Hoare calculus
failures refinement
Sponsor/Funder: 9763
Proceedings Title: SEFM 2016: Software Engineering and Formal Methods
Publisher: Springer
Publisher Place: Cham
Publisher DOI: 10.1007/978-3-319-41591-8_5
Page Start: 61
Page End: 75
Series: Lecture Notes in Computer Science
EISSN: 1611-3349
ISBN: 978-3-319-41590-1
ISSN: 0302-9743
Appears in Collections:Inst. Softwaretechnik und Theoretische Informatik » Publications

Files in This Item:

Accepted manuscript

Format: Adobe PDF | Size: 820.98 kB
DownloadShow Preview

Item Export Bar

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