On the use of formal techniques for analyzing dependable real-time protocols

The effective design of composite dependable and real-time protocols entails demonstrating their proof of correctness and, in practice, the efficient delivery of services. We focus on these aspects of correctness and efficiency, specifically considering the real-time aspects where the need is to ensure satisfaction of stringent timing and operational constraints. In this paper we establish the use of mathematically rigorous techniques such as formal methods (FM's) in not only providing for their traditional usage in establishing correctness checks, but also for their capability of assessing and analyzing timing requirements in dependable real-time protocols. We present our perspectives in utilizing FM's in developing exact case analyses of fault-tolerant and real-time protocols. We discuss the insights obtained and flaws identified in the hand analysis over the process of formally analyzing and verifying the correctness of an existing fault-tolerant real-time scheduling protocol