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.