Model checking dependabiliy attributes of wireless group communication

Mieke Massink, Joost-Pieter Katoen, Diego Latella

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    11 Citations (Scopus)
    25 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationInternational Conference on Dependable Systems and Networks, 2004
    Place of PublicationPiscataway, NJ
    PublisherIEEE
    Pages711-720
    Number of pages10
    ISBN (Print)0-7695-2052-9
    DOIs
    Publication statusPublished - 2004
    EventInternational Conference on Dependable Systems and Networks, DSN 2004 - Florence, Italy
    Duration: 28 Jun 20041 Jul 2004

    Conference

    ConferenceInternational Conference on Dependable Systems and Networks, DSN 2004
    Abbreviated titleDSN
    CountryItaly
    CityFlorence
    Period28/06/041/07/04

    Keywords

    • FMT-PM: PROBABILISTIC METHODS
    • FMT-MC: MODEL CHECKING
    • 0
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

    Fingerprint Dive into the research topics of 'Model checking dependabiliy attributes of wireless group communication'. Together they form a unique fingerprint.

    Cite this