Industrial-Strength Formal Specification Techniques, Workshop on (1995)
Boca Raton, Florida
Apr. 5, 1995 to Apr. 8, 1995
S. Campos , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
E. Clarke , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
W. Marrero , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
M. Minea , Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
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/sup 30/ states. To illustrate the usefulness of our method, we describe the timing analysis for a patient monitoring system with more than 10/sup 13/ 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.
real-time systems; formal specification; timing; formal verification; search problems; aircraft control; systems analysis; medical computing; timing analysis; industrial real-time systems; real-time systems modeling; exact bounds; delay; starting condition; ending condition; symbolic model checking; industrial designs; state spaces; search; patient monitoring system; timing verification; aircraft controller
S. Campos, M. Minea, W. Marrero and E. Clarke, "Timing analysis of industrial real-time systems," Industrial-Strength Formal Specification Techniques, Workshop on(WIFT), Boca Raton, Florida, 1995, pp. 97.