Model checking dependabiliy attributes of wireless group communication


Massink, M. and Katoen, J.P. and Latella, D. (2004) Model checking dependabiliy attributes of wireless group communication. In: Dependable Systems and Networks - Performance and Dependability Symposium (DSN 2003), 28 June - 1 July 2004, Florence, Italy (pp. pp. 711-720).

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract: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 [Analysis and estimation of the quality of service of group communication protocols] 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.
Item Type:Conference or Workshop Item
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page