FG Software and Embedded Systems Engineering

4 Items

Recent Submissions
Information flow analysis of discrete embedded control system models

Mikulcak, Marcus (2020)

Embedded systems used in safety-critical domains have to uphold strict safety and security requirements. At the same time, their complexity has been strongly increasing across application domains. To manage this rise in complexity, manufacturers have shifted towards model-driven development methodologies. While successful in managing the complexity in the development of large, interconnected sy...

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