WORST-CASE TIMING ANALYSIS VIA FINDING LONGEST
PATHS IN SPARK ADA BASIC-PATH GRAPHS
The British Aerospace Dependable Computing Systems Centre,
Department of Computer Science,
University of York,
York YO1 5DD
27th October 1994
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 worstcase
timing assuming suitable bounds on each loop are available.
This paper describes and offers a proof of the new algorithm,
followed by examples of its application.
Keywords: path expression, longest path, worst-case timing
analysis, hard real-time, safety-critical, Ada.