Horst F. Wedde, Bodgan Korel und Dorota M. Huizinga
Formal Timing Analysis of Distributed Real-Time Programs
Real-Time Systems, Nr. 7, S. 57-90, Kluwer Academic Publishers, 1994
A static analysis method for verifying timing properties of real-time distributed programs is presented. The goal is to calculate the worst-case response time of concurrent tasks which run mainly independently but share, and may have to wait for, logical or physical devices. For such tasks, the determination of the worst-case waiting time is a crucial problem because of the unpredictable order of synchronization events. We investigate the class of distributed Client-Server programs in which independent, time-critical tasks (clients) are synchronized only through additional server tasks, playing the role of monitors or resource managers. This model follows well-known real-time design guidelines for distributed ADA programs proposed to enhance schedulability and synchronization analysis. Our formal analysis approach is flow graph oriented. It leads to generating reduced program paths each of which represents a sequence of ordered local and global operations, thus transforming and reducing the original problem of computing the worst-case waiting time of a concurrent task into a graph-theoretic problem of calculating the maximal blocking time for one of its corresponding program paths. While local operations are completely independent global operations require mutually exclusive access to shared resources. We prove that computing the worst-case blocking time for a program path is NP-complete. Even for a reduced problem solution—which would yield a good upper bound for the worst-case blocking time—there was a conjecture maintained over many years that this problem was NP-complete. A major result of this paper is to show that this is wrong. Instead, we construct a polynomial solution algorithm, and we prove its correctness. The effectiveness and complexity of our method are discussed, with particular emphasis on distributed real-time debugging.