http://www.cnr.it/ontology/cnr/individuo/prodotto/ID91086
Model checking dependability attributes of wireless group communication. (Contributo in atti di convegno)
- Type
- Label
- Model checking dependability attributes of wireless group communication. (Contributo in atti di convegno) (literal)
- Anno
- 2004-01-01T00:00:00+01:00 (literal)
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#doi
- 10.1109/DSN.2004.1311942 (literal)
- Alternative label
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
- Mieke Massink; Joost P. Katoen; Diego Latella (literal)
- Pagina inizio
- Pagina fine
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#titoloVolume
- Proceedings of the 2004 International Conference on Dependable Systems and Networks (literal)
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#note
- (Italy, June 28-July 1, 2004). Proceedings, pp. 711-720. IEEE, 2004. (literal)
- Note
- ISI Web of Science (WOS) (literal)
- Scopu (literal)
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
- C.N.R.-ISTI, Via Moruzzi 1, I-56124 Pisa, Italy;
Dept. of Comp. Science, Univ. of Twente, P.O. Box 217, 7500 AE Enschede, The Netherlands;
C.N.R.-ISTI, Via Moruzzi 1, I-56124 Pisa, Italy; (literal)
- Titolo
- Model checking dependability attributes of wireless group communication. (literal)
- Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#isbn
- Abstract
- 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. (literal)
- Editore
- Prodotto di
- Autore CNR
- Insieme di parole chiave
Incoming links:
- Autore CNR di
- Prodotto
- Editore di
- Insieme di parole chiave di