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.

PDF
Restricted to UT campus only: Request a copy
83Kb

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
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/63330
Official URL:	http://doi.ieeecomputersociety.org/10.1109/DSN.2004.1311942
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page