On the Use of Formal Techniques for Analyzing Dependable Real-Time Protocols

The e ective design of composite dependable and real-time protocols entails demonstrating their proof of correctness and, in practice, the e cient delivery of services. We focus on these aspects of correctness and e ciency, speci cally 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 realtime protocols. We present our perspectives in utilizing FM's in developing exact case analyses of faulttolerant and real-time protocols. We discuss the insights obtained and aws identi ed in the hand analysis over the process of formally analyzing and verifying the correctness of an existing fault-tolerant real-time scheduling protocol.

• Type: Conference
• Year: 1999
• Where: RTSS
• Authors: Purnendu Sinha, Neeraj Suri
• Keywords: Control Systems, Correctness, Real-time Protocols, Real-time Protocols Entails, RTSS 1999