Combining static worst-case timing analysis and program proof

R Chapman; A Burns; A Wellings

Combining static worst-case timing analysis and program proof

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English
Pages (from-to)	145-171
Number of pages	27
Journal	Real-Time Systems
Volume	11
Issue number	2
Publication status	Published - Sept 1996

Keywords

CASE EXECUTION TIMES
PROCESSORS

Cite this

@article{d407f1f6551844338a8e151b2a506607,

title = "Combining static worst-case timing analysis and program proof",

abstract = "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.",

keywords = "CASE EXECUTION TIMES, PROCESSORS",

author = "R Chapman and A Burns and A Wellings",

year = "1996",

month = sep,

language = "English",

volume = "11",

pages = "145--171",

journal = "Real-Time Systems",

issn = "0922-6443",

publisher = "Springer",

number = "2",

}

TY - JOUR

T1 - Combining static worst-case timing analysis and program proof

AU - Chapman, R

AU - Burns, A

AU - Wellings, A

PY - 1996/9

Y1 - 1996/9

N2 - 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.

AB - 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.

KW - CASE EXECUTION TIMES

KW - PROCESSORS

M3 - Article

SN - 0922-6443

VL - 11

SP - 145

EP - 171

JO - Real-Time Systems

JF - Real-Time Systems

IS - 2

ER -