Model-checking performability properties

Boudewijn Haverkort, Lucia Cloth, Holger Hermanns, Joost P. Katoen, Christel Baier

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

    59 Citations (Scopus)
    18 Downloads (Pure)

    Abstract

    Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.
    Original languageEnglish
    Title of host publicationProceedings International Conference on Dependable Systems and Networks (DSN)
    Subtitle of host publication23-26 June 2002, Washington, D.C., USA
    PublisherIEEE
    Pages103-112
    Number of pages10
    ISBN (Electronic)0-7695-1599-1
    ISBN (Print)0-7695-1597-5, 0-7695-1598-3
    DOIs
    Publication statusPublished - 2002
    EventInternational Conference on Dependable Systems and Networks, DSN 2002 - Washington, United States
    Duration: 23 Jun 200226 Jun 2002

    Other

    OtherInternational Conference on Dependable Systems and Networks, DSN 2002
    Abbreviated titleDSN
    Country/TerritoryUnited States
    CityWashington
    Period23/06/0226/06/02

    Keywords

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

    Fingerprint

    Dive into the research topics of 'Model-checking performability properties'. Together they form a unique fingerprint.

    Cite this