PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Massink M., Katoen J., Latella D. Model Checking Dependability Attributes of Wireless Group Communication. Full Version. The document has been submitted to Conference: Accepted for publication at DSN-PDS 2004. Performance and Dependability Symposium, Florence, IT, June 2004, Technical report, 2004.
 
 
Abstract
(English)
Models used for the analysis of dependability and performance attributes of communication protocols often abstract considerably from the details of the actual protocol. These models often consist of concurrent sub-models and this may make it hard to judge whether their behaviour is faithfully reflecting the protocol. In this paper, we show how model checking of continuous-time Markov chains, generated from high-level specifications, facilitates the analysis of both correctness and dependability attributes. We illustrate this by revisiting a performance analysis of a variant of the central access protocol of the IEEE 802.11 standard for wireless local area networks. This variant has been developed to support real-time group communication between autonomous mobile stations. Correctness and dependability properties are formally characterised using Continuous Stochastic Logic and are automatically verified by the ETMCC model checker. The models used are specified as Stochastic Activity Nets.
Subject Wireless Protocols
Stochastic Activity Nets
Stochastic Model Checking
D.2.4. Software/Program Verification
G.3 PROBABILITY AND STATISTICS
68N30 Mathematical aspects of software engineering


Icona documento 1) Download Document PS


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional