Login | Register

Probabilistic Analysis of Wireless Systems Using Theorem Proving


Probabilistic Analysis of Wireless Systems Using Theorem Proving

Hasan, Osman and Tahar, Sofiène (2009) Probabilistic Analysis of Wireless Systems Using Theorem Proving. Electronic Notes in Theoretical Computer Science, 242 (2). pp. 43-58. ISSN 15710661

[thumbnail of probabilistic_analysis_of_wireless_systems.pdf]
Text (application/pdf)
probabilistic_analysis_of_wireless_systems.pdf - Accepted Version

Official URL: http://dx.doi.org/10.1016/j.entcs.2009.06.022


Probabilistic techniques play a major role in the design and analysis of wirelesssystems as they contain a significant amount of random or unpredictable components. Traditionally, computer simulation techniques are used to perform probabilisticanalysis of wirelesssystems but they provide inaccurate results and usually require enormous amount of CPU time in order to attain reasonable estimates. To overcome these limitations, we propose to use a higher-order-logic theorem prover (HOL) for the analysis of wirelesssystems. The paper presents a concise description of the formal foundations required to conduct the analysis of a wirelesssystem in a theorem prover, such as the higher-order-logic modeling of random variables and the verification of their corresponding probabilistic and statistical properties in a theorem prover. In order to illustrate the utilization and effectiveness of the proposed idea for handling real-world wirelesssystemanalysis problems, we present an analysis of the automated repeat request (ARQ) mechanism at the logic link control (LLC) layer of the General Packet Radio Service (GPRS), which is a packet oriented mobile data service available to the users of Global System for Mobile Communications (GSM).

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Authors:Hasan, Osman and Tahar, Sofiène
Journal or Publication:Electronic Notes in Theoretical Computer Science
Digital Object Identifier (DOI):10.1016/j.entcs.2009.06.022
ID Code:974504
Deposited On:31 Jul 2012 20:16
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