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
  • Mieke Massink; Joost P. Katoen; Diego Latella (2004)
    Model checking dependability attributes of wireless group communication.
    in 2004 International Conference on Dependable Systems and Networks, Florence
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Mieke Massink; Joost P. Katoen; Diego Latella (literal)
Pagina inizio
  • 711 (literal)
Pagina fine
  • 720 (literal)
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
  • 0-7695-2052-9 (literal)
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
data.CNR.it