FG Software and Embedded Systems Engineering

3 Items

Recent Submissions
Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages

Berg, Nils ; Göthel, Thomas ; Danziger, Armin ; Glesner, Sabine (2018-10-11)

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 fo...

Formal Verification of Low-Level Code in a Model-Based Refinement Process (Technical Report: Isabelle/HOL formalization)

Berg, Nils ; Bartels, Björn ; Danziger, Armin ; Grochau Azzi, Guilherme ; Bentert, Matthias (2019-09)

This is the technical report for the Isabelle/HOL formalization accompanying the dissertation of Nils Berg. For explanations with regard to content please refer to the dissertation. The intention of this document is to give a mapping from the formalization in the dissertation to the formalization in Isabelle/HOL. Formalized are the parts where user interaction is required, i.e., the first part ...

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

Berg, Nils ; Göthel, Thomas ; Danziger, Armin ; Glesner, Sabine (2020)

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 ...