Timing Analysis of Assembler Code Control-Flow Paths
Lecture notes in computer science, (2002)http://www.springerlink.com/content/g95lwpppvy5rdpcu/.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 constraints 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 postcondition semantics. However, despite the formalism’s simplicity, it is shown that complex timing behaviour associated with instruction pipelining and iterative code can be modelled accurately.
