Analyzing Embedded Systems Code for Mixed-Critical Systems Using Hybrid Memory Representations
Eva Beckschulze, Jörg Bräuer, André Stollenwerk, Stefan Kowalewski · 2011
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.