Combining static worst-case timing analysis and program proof

R Chapman, A Burns, A Wellings

Research output: Contribution to journalArticlepeer-review


This paper describes SPATS-a new toolset for the development of safety-critical and hard real-time systems. SPATS integrates the analyses traditionally offered by program proof and static timing analysis tools through analysis of program basic-path graphs. This paper concentrates on SPATS' facilities for high-level static timing analysis and analysis of worst-case stack usage. The integration of timing analysis and program proof allows timing analysis to be performed where worst-case execution time (WCET) depends on a program's input data, and allows timing annotations to be formally verified. The approach is developed and illustrated with a worked example. The implementation and experimental application of SPATS to realistic industrial case-studies are also described. We conclude that SPATS offers a novel new approach to static timing analysis, offers several new analyses not seen in previous systems, and can be implemented in a useful and efficient toolset.

Original languageEnglish
Pages (from-to)145-171
Number of pages27
JournalReal-Time Systems
Issue number2
Publication statusPublished - Sept 1996



Cite this