WORST-CASE TIMING ANALYSIS VIA FINDING LONGEST

PATHS IN SPARK ADA BASIC-PATH GRAPHS

Roderick Chapman

The British Aerospace Dependable Computing Systems Centre,
Department of Computer Science,
University of York,
Heslington,
York YO1 5DD

27th October 1994

ABSTRACT

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.