Performance and reliability model checking and model construction

H. Hermanns

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    Abstract

    Continuous-time Markov chains (CTMCs) are widely used to describe stochastic phenomena in many diverse areas. They are used to estimate performance and reliability characteristics of various nature, for instance to quantify throughputs of manufacturing systems, to locate bottlenecks in communication systems, or to estimate reliability in aerospace systems. CTMCs are the underlying semantic model of major high level performance modelling formalisms such as stochastic Petri nets, stochastic process algebras, and Markovian queueing networks. Model checking is a very successful technique to establish correctness of systems from very similar application domains, usually described in terms of a nondeterministic finite-state model. One of the major reasons for the success of model checking tools in practice is the efficient way to cope with the state-space explosion problem, using symbolic (BDD-based) techniques. In this talk, I will introduce CTMCs and discuss the use of model checking to assess performance and reliability properties of CTMCs. With this approach, properties-of-interest are expressed as formulas of a stochastic extension of the logic CTL and interpreted over CTMCs. Model checking this logic requires the solution of linear systems of equations and of systems of Volterra integral equations. I will outline approximate techniques for solving the equation systems, and present a JAVA implementation of a Markov chain model checker. My introduction to CTMC model checking will be complemented with a discussion of CTMC model construction techniques. I will survey formal methods that facilitate the construction of large CTMC models. In particular I will focus on high-level formalisms supporting a modern, hierarchical and compositional design methodology. Existing tool support, as well as techniques to combat the state space explosion problem will be discussed.
    Original languageEnglish
    Title of host publication5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000
    EditorsStefania Gnesi, Ina Schieferdecker, Axel Rennoch
    PublisherG.M.D.
    Pages11-27
    Number of pages17
    Publication statusPublished - 2000
    Event5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000 - Berlin, Germany
    Duration: 3 Apr 20004 Apr 2000
    Conference number: 5
    https://fmics.inria.fr/workshop-5/

    Publication series

    NameGMD Report
    PublisherGMD
    Volume91
    ISSN (Print)1435-2702

    Workshop

    Workshop5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000
    Abbreviated titleFMICS
    CountryGermany
    CityBerlin
    Period3/04/004/04/00
    Internet address

    Fingerprint

    Model checking
    Markov processes
    Explosions
    Queueing networks
    Formal methods
    Random processes
    Petri nets
    Algebra
    Integral equations
    Linear systems
    Communication systems
    Semantics
    Throughput

    Keywords

    • EWI-6444

    Cite this

    Hermanns, H. (2000). Performance and reliability model checking and model construction. In S. Gnesi, I. Schieferdecker, & A. Rennoch (Eds.), 5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000 (pp. 11-27). (GMD Report; Vol. 91). G.M.D..
    Hermanns, H. / Performance and reliability model checking and model construction. 5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000. editor / Stefania Gnesi ; Ina Schieferdecker ; Axel Rennoch. G.M.D., 2000. pp. 11-27 (GMD Report).
    @inproceedings{a0fe8103446646c08c1aef6fe29f4d7d,
    title = "Performance and reliability model checking and model construction",
    abstract = "Continuous-time Markov chains (CTMCs) are widely used to describe stochastic phenomena in many diverse areas. They are used to estimate performance and reliability characteristics of various nature, for instance to quantify throughputs of manufacturing systems, to locate bottlenecks in communication systems, or to estimate reliability in aerospace systems. CTMCs are the underlying semantic model of major high level performance modelling formalisms such as stochastic Petri nets, stochastic process algebras, and Markovian queueing networks. Model checking is a very successful technique to establish correctness of systems from very similar application domains, usually described in terms of a nondeterministic finite-state model. One of the major reasons for the success of model checking tools in practice is the efficient way to cope with the state-space explosion problem, using symbolic (BDD-based) techniques. In this talk, I will introduce CTMCs and discuss the use of model checking to assess performance and reliability properties of CTMCs. With this approach, properties-of-interest are expressed as formulas of a stochastic extension of the logic CTL and interpreted over CTMCs. Model checking this logic requires the solution of linear systems of equations and of systems of Volterra integral equations. I will outline approximate techniques for solving the equation systems, and present a JAVA implementation of a Markov chain model checker. My introduction to CTMC model checking will be complemented with a discussion of CTMC model construction techniques. I will survey formal methods that facilitate the construction of large CTMC models. In particular I will focus on high-level formalisms supporting a modern, hierarchical and compositional design methodology. Existing tool support, as well as techniques to combat the state space explosion problem will be discussed.",
    keywords = "EWI-6444",
    author = "H. Hermanns",
    year = "2000",
    language = "English",
    series = "GMD Report",
    publisher = "G.M.D.",
    pages = "11--27",
    editor = "Stefania Gnesi and Ina Schieferdecker and Axel Rennoch",
    booktitle = "5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000",

    }

    Hermanns, H 2000, Performance and reliability model checking and model construction. in S Gnesi, I Schieferdecker & A Rennoch (eds), 5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000. GMD Report, vol. 91, G.M.D., pp. 11-27, 5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000, Berlin, Germany, 3/04/00.

    Performance and reliability model checking and model construction. / Hermanns, H.

    5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000. ed. / Stefania Gnesi; Ina Schieferdecker; Axel Rennoch. G.M.D., 2000. p. 11-27 (GMD Report; Vol. 91).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    TY - GEN

    T1 - Performance and reliability model checking and model construction

    AU - Hermanns, H.

    PY - 2000

    Y1 - 2000

    N2 - Continuous-time Markov chains (CTMCs) are widely used to describe stochastic phenomena in many diverse areas. They are used to estimate performance and reliability characteristics of various nature, for instance to quantify throughputs of manufacturing systems, to locate bottlenecks in communication systems, or to estimate reliability in aerospace systems. CTMCs are the underlying semantic model of major high level performance modelling formalisms such as stochastic Petri nets, stochastic process algebras, and Markovian queueing networks. Model checking is a very successful technique to establish correctness of systems from very similar application domains, usually described in terms of a nondeterministic finite-state model. One of the major reasons for the success of model checking tools in practice is the efficient way to cope with the state-space explosion problem, using symbolic (BDD-based) techniques. In this talk, I will introduce CTMCs and discuss the use of model checking to assess performance and reliability properties of CTMCs. With this approach, properties-of-interest are expressed as formulas of a stochastic extension of the logic CTL and interpreted over CTMCs. Model checking this logic requires the solution of linear systems of equations and of systems of Volterra integral equations. I will outline approximate techniques for solving the equation systems, and present a JAVA implementation of a Markov chain model checker. My introduction to CTMC model checking will be complemented with a discussion of CTMC model construction techniques. I will survey formal methods that facilitate the construction of large CTMC models. In particular I will focus on high-level formalisms supporting a modern, hierarchical and compositional design methodology. Existing tool support, as well as techniques to combat the state space explosion problem will be discussed.

    AB - Continuous-time Markov chains (CTMCs) are widely used to describe stochastic phenomena in many diverse areas. They are used to estimate performance and reliability characteristics of various nature, for instance to quantify throughputs of manufacturing systems, to locate bottlenecks in communication systems, or to estimate reliability in aerospace systems. CTMCs are the underlying semantic model of major high level performance modelling formalisms such as stochastic Petri nets, stochastic process algebras, and Markovian queueing networks. Model checking is a very successful technique to establish correctness of systems from very similar application domains, usually described in terms of a nondeterministic finite-state model. One of the major reasons for the success of model checking tools in practice is the efficient way to cope with the state-space explosion problem, using symbolic (BDD-based) techniques. In this talk, I will introduce CTMCs and discuss the use of model checking to assess performance and reliability properties of CTMCs. With this approach, properties-of-interest are expressed as formulas of a stochastic extension of the logic CTL and interpreted over CTMCs. Model checking this logic requires the solution of linear systems of equations and of systems of Volterra integral equations. I will outline approximate techniques for solving the equation systems, and present a JAVA implementation of a Markov chain model checker. My introduction to CTMC model checking will be complemented with a discussion of CTMC model construction techniques. I will survey formal methods that facilitate the construction of large CTMC models. In particular I will focus on high-level formalisms supporting a modern, hierarchical and compositional design methodology. Existing tool support, as well as techniques to combat the state space explosion problem will be discussed.

    KW - EWI-6444

    M3 - Conference contribution

    T3 - GMD Report

    SP - 11

    EP - 27

    BT - 5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000

    A2 - Gnesi, Stefania

    A2 - Schieferdecker, Ina

    A2 - Rennoch, Axel

    PB - G.M.D.

    ER -

    Hermanns H. Performance and reliability model checking and model construction. In Gnesi S, Schieferdecker I, Rennoch A, editors, 5th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2000. G.M.D. 2000. p. 11-27. (GMD Report).