Timing analysis of industrial real-time systems

We describe a formal method for modelling real-time systems and a procedure to compute the model´s timing characteristics automatically. We present algorithms that compute exact bounds on the delay between two specified events. We also describe an algorithm to count the minimum and maximum number of times an event occurs between a given starting condition and an ending condition. These algorithms are based on symbolic model checking techniques which have been successfully used to find bugs in several industrial designs. Such techniques can be used to search exhaustively state spaces with up to 10³⁰ states. To illustrate the usefulness of our method, we describe the timing analysis for a patient monitoring system with more than 10¹³ states. We also present the timing analysis and verification for an aircraft controller. The sizes of the examples we verify demonstrate that our tool can be applied to realistic industrial designs