Annotate once — analyze anywhere: Context-aware WCET analysis by user-defined abstractions

Abstract:

The widespread adoption of cyber-physical systems in the safety-critical (hard real-time) domain is accompanied by a rising degree of code-reuse up to actual software product lines spanning different hardware platforms. Nevertheless, the dominant tools for static worst-case execution-time (WCET) analysis operate on individual, specific system instances at the binary level, further depending on machine-code–level annotations for precise analysis. Thus, this timing verification is neither portable nor reusable. PragMetis addresses this schism by providing an expressive source-level annotation language that enables to express context dependence at the library level using user-defined abstractions. These abstractions allow users to generically annotate context-dependent flow facts down to the granularity of individual loop contexts. We then use control-flow–relation graphs to transfer these facts to machine-code level for specific instances, even in the presence of certain compiler optimizations, thus achieving portability. Our evaluation results based on TACLeBench confirm that PragMetis's powerful expressions yield more accurate WCET bounds.