Model checking dependability attributes of wireless group communication.

Models used for the analysis of dependability and perfor- mance 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 cor- rectness and dependability attributes. We illustrate this by revisiting a dependability analysis [8] of a variant of the central access protocol of the IEEE 802.11 standard for wireless local area networks. This variant has been devel- oped to support real-time group communication between autonomous mobile stations. Correctness and dependabil- ity properties are formally characterised using Continu- ous Stochastic Logic and are automatically verified by the ETMCC model checker. The models used are specified as Stochastic Activity Nets.