Analyzing Embedded Systems Code for Mixed-Critical Systems Using Hybrid Memory Representations
This paper presents a low-level memory and
hardware model suitable for analyzing embedded systems
software written in high-level languages such as C. The key
feature of this approach is that it combines information that
can be discovered from the C code itself with information
from the executable binary program. Further, it also integrates
effects caused through hardware dependencies. We describe
the benefits of this model by showing its applicability to the
verification of properties related to software partitioning, which
is crucial for systems of mixed criticality. Furthermore, we
demonstrate that our model can easily be integrated into
abstract interpretation frameworks for high-level languages so
as to increase analysis precision.
Eva Beckschulze, Jörg Brauer, Andre Stollenwerk, Stefan Kowalewski