Noname manuscript No. (will be inserted by the editor) Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL

Abstract Real-time systems usually involve a subtle interaction of a number of dis-tributed components and have a high degree of parallelism, which makes their perfor-mance analysis quite complex. Thus, traditional techniques, such as simulation, or the state-based formal methods usually fail to produce reasonable results. In this paper, we propose to use higher-order-logic theorem proving for the performance analysis of real-time systems. The idea is to formalize the real-time system as a logical conjunc-tion of higher-order-logic predicates, whereas each one of these predicates define an autonomous component or process of the given real-time system. The random or un-predictable behavior found in these components is modeled as random variables. This formal specification can then be used in a higher-order-logic theorem prover (HOL) to reason about both functional and performance related properties of the given real-time system. In order to illustrate the practical effectiveness of our approach, we present the analysis of the Stop-and-Wait protocol, which is a classical example of real-time systems. The functional correctness of the protocol is verified by proving that the pro-tocol ensures reliable data transfers. Whereas, the average message delay relation is verified in HOL for the sake of performance analysis. The paper includes the protocol’s formalization details along with the HOL proof sketches for the major theorems