Timing analysis of assembler code control-flow paths

Abstract

Timing analysis of assembler code is essential to achieve the strongest possible guarantee of correctness for safety-critical, real-time software. Previous work has shown how timing constrain ts on control flow paths through high-level language programs can be formalised using the semantics of the statements comprising the path. We extend these results to assembler-level code where it becomes possible to not only determine timing constraints, but also to verify them against the known execution times for each instruction. A minimal formal model is developed with both a weakest liberal precondition and a strongest post condition semantics. However, despite the formalism’s simplicity, it is shown that complex timing behaviour associated with instruction pipe lining and iterative code can be modelled accurately.