Verifying Safety-Critical Timing and Memory-Usage Properties of Embedded Software by Abstract Interpretation

TL;DR

This paper presents a static analysis approach using abstract interpretation to verify safety-critical timing and memory properties of embedded software, enhancing reliability in safety-critical systems.

Contribution

It introduces a method that combines value analysis with advanced analyses to accurately verify timing and memory safety properties of embedded software.

Findings

Effective verification of timing properties

Accurate memory usage analysis

Improved safety assurance for embedded systems

Abstract

Static program analysis by abstract interpretation is an efficient method to determine properties of embedded software. One example is value analysis, which determines the values stored in the processor registers. Its results are used as input to more advanced analyses, which ultimately yield information about the stack usage and the timing behavior of embedded software.