Compositional Design of Distributed Real-time Protocols

The problem of designing a correct real-time protocol is a challenging task and has led researchers to develop compositional techniques for designing protocols. The service specification ss(P ) of a protocol P defines the services provided by the protocol and its protocol specification ps(P ) specifies the rules of message exchange to ensure the service. A number of techniques have been proposed to compose protocol specifications in which given two component protocols, P and Q, of a complex protocol R, ps(P ) and ps(Q) are first combined to obtain ps(R), and then inference rules are used to derive ss(R). In this paper, we explore an alternative technique for real-time protocols in which ss(P ) and ss(Q) are first combined to obtain ss(R), and analyzed for potential deadline violations. Given ss(R), we provide an algorithm to mechanically combine ps(P ) and ps(Q) to obtain ps(R). We show that analysis of ss(R) is sufficient to ensure certain real-time properties of ps(R). This results in efficient validation as state space of ss(R) is typically significantly smaller than that of ps(R)