Integrated program proof and worst-case timing analysis of SPARK Ada.

. This paper describes work in progress at the University of York on worst-case timing analysis of software for hard real-time and safety-critical systems. We are pursuing a programming environment that combines the technologies of program proof and timing analysis. In short, the analytical power afforded by a classical program proof tool is ideal for the high-level analysis of timing properties. The main thrust of our work, then, has been to investigate how these technologies can be integrated to their mutual benefit. This paper describes our current ideas and results in this field. 1. Introduction The need for static timing analysis of software for hard real-time systems is well-known. 1-3 Static timing analysis is important for system design and testing and is a prerequisite for static schedulability analysis. This work is also motivated by the needs of safety-critical systems, and through direct collaboration with industry. During case studies of typical hard real-time and critic..