Symbolic Timing Analysis of Real-Time Systems

Abstract

<p>Timing analysis of a real-time control program is often required to verify that the system meets timing requirements. For example, if a real-time control program responds too slowly or too quickly, then the system may become unstable and fail. Traditional methods to determine timing bound estimates are often restrictive, labour-intensive, and error-prone. This thesis proposes an automated method of obtaining best- and worst-case timing bounds on unstructured assembly code without the need for manual annotation of loop or recursive call bounds. A prototype tool suite takes an assembly program as input and then generates the static control-flow graph. The generated static control-flow graph is then automatically translated into a timed automata model that models instruction processing times and adds variables to model the processor state. The resulting timed automata's transition relation represents the dynamic control-flow graph of the program. Fastest and slowest trace algorithms in recent prototype versions of UPPAAL, a timed automata model checker, are then used to extract tight best- and worst-case execution times of the program. The method is applied to code examples for two different low-end (i.e., no cache or pipeline) 8 and 16-bit microcontroller architectures, the PIC and IBM1800.</p>