Automated performance and dependability evaluation using model checking

Christel Baier, Boudewijn Haverkort, Holger Hermanns, Joost-Pieter Katoen

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    21 Citations (Scopus)
    96 Downloads (Pure)

    Abstract

    Markov chains (and their extensions with rewards) have been widely used to determine performance, dependability and performability characteristics of computer communication systems, such as throughput, delay, mean time to failure, or the probability to accumulate at least a certain amount of reward in a given time. Due to the rapidly increasing size and complexity of systems, Markov chains and Markov reward models are difficult and cumbersome to specify by hand at the state-space level. Therefore, various specification formalisms, such as stochastic Petri nets and stochastic process algebras, have been developed to facilitate the specification of these models at a higher level of abstraction. Up till now, however, the specification of the measure-of-interest is often done in an informal and relatively unstructured way. Furthermore, some measures-of-interest can not be expressed conveniently at all. In this tutorial paper, we present a logic-based specification technique to specify performance, dependability and performability measures-of-interest and show how for a given finite Markov chain (or Markov reward model) such measures can be evaluated in a fully automated way. Particular emphasis will be given to so-called path-based measures and hierarchically-specified measures. For this purpose, we extend so-called model checking techniques to reason about discrete- and continuous-time Markov chains and their rewards. We also report on the use of techniques such as (compositional) model reduction and measure-driven state-space generation to combat the infamous state space explosion problem.
    Original languageEnglish
    Title of host publicationPerformance Evaluation of Complex Systems: Techniques and Tools
    Subtitle of host publicationPerformance 2002 Tutorial Lectures
    EditorsMariacarla Calzarossa, Salvatore Tucci
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages261-289
    Number of pages29
    ISBN (Electronic)978-3-540-45798-5
    ISBN (Print)978-3-540-44252-3
    DOIs
    Publication statusPublished - 2002
    EventIFIP WG 7.3 International Symposium on Computer Modeling, Measurement, and Evaluation, Performance 2002 - Rome, Italy
    Duration: 23 Sep 200227 Sep 2002

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume2459
    ISSN (Print)0302-9743

    Conference

    ConferenceIFIP WG 7.3 International Symposium on Computer Modeling, Measurement, and Evaluation, Performance 2002
    CountryItaly
    CityRome
    Period23/09/0227/09/02

    Keywords

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

    Fingerprint

    Dive into the research topics of 'Automated performance and dependability evaluation using model checking'. Together they form a unique fingerprint.

    Cite this