Login | Register

Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL

Title:

Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL

Hasan, Osman and Tahar, Sofiène (2009) Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL. Journal of Automated Reasoning, 42 (1). pp. 1-33. ISSN 0168-7433

[thumbnail of performance_analysis_and_functional_verification.pdf]
Preview
Text (application/pdf)
performance_analysis_and_functional_verification.pdf - Accepted Version
323kB

Official URL: http://dx.doi.org/10.1007/s10817-008-9105-6

Abstract

Real-time systems usually involve a subtle interaction of a number of distributed components and have a high degree of parallelism, which makes their performance 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 (HOL) theorem proving for the performance analysis of real-time systems. The idea is to formalize the real-time system as a logical conjunction of HOL predicates, whereas each one of these predicates define an autonomous component or process of the given real-time system. The random or unpredictable behavior found in these components is modeled as random variables. This formal specification can then be used in a HOL theorem prover 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 protocol 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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Hasan, Osman and Tahar, Sofiène
Journal or Publication:Journal of Automated Reasoning
Date:2009
Digital Object Identifier (DOI):10.1007/s10817-008-9105-6
ID Code:974503
Deposited By: ANDREA MURRAY
Deposited On:31 Jul 2012 20:13
Last Modified:18 Jan 2018 17:38
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top