PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Massink M., Katoen J., Latella D. Model Checking Dependability Attributes of Wireless Group Communication. In: International Conference on Dependable Systems and Networks (Florence, June 28 - July 2004). Proceedings, pp. 711 - 720. IEEE Computer Society Press, 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 dependability 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 Stochastic Model Checking
Formal Methods
Wireless
D.2.4. Software/Program Verification
G.3. Probability and statistics


Icona documento 1) Download Document PDF


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