Worst-Case Timing Analysis Via Finding Longest Paths In Spark ADA . . .

The SPARK Proof and Timing System (SPATS) is a collection of software tools developed to assist the static analysis of safetycritical and hard real-time software. SPATS integrates both classical program proof and worst-case execution time analysis through analysis of a program's basic-path control-flow graph. A new algorithm has been developed that transforms a cyclic basicpath graph into a path-expression that can be evaluated for worst-case timing assuming suitable bounds on each loop are available. This pape