A model checker for performance and dependability properties

H. Hermanns, F. Karelse (Editor), Joost P. Katoen, J. Meyer-Kayser, M. Siegle

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

    14 Downloads (Pure)

    Abstract

    Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [8] and the continuous time setting [1], [3]. In this short paper, we describe the prototype model checker $E \vdash M C^2$ for discrete and continuous-time Markov chains, where properties are expressed in appropriate extensions of CTL.We illustrate the general benefits of this approach and discuss the structure of the tool.
    Original languageEnglish
    Title of host publicationProceedings of the 2nd PROGRESS Workshop on Embedded Systems 2001
    Place of PublicationVeldhoven, the Netherlands
    PublisherSTW
    Pages83-88
    Number of pages6
    ISBN (Print)90-73461-27-X
    Publication statusPublished - 2001
    Event2nd PROGRESS Workshop on Embedded Systems 2001 - Veldhoven, Netherlands
    Duration: 18 Oct 200118 Oct 2001
    Conference number: 2

    Workshop

    Workshop2nd PROGRESS Workshop on Embedded Systems 2001
    Abbreviated titlePROGRESS
    CountryNetherlands
    CityVeldhoven
    Period18/10/0118/10/01

      Fingerprint

    Keywords

    • FMT-PM: PROBABILISTIC METHODS
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-MC: MODEL CHECKING
    • FMT-TOOLS
    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

    Cite this

    Hermanns, H., Karelse, F. (Ed.), Katoen, J. P., Meyer-Kayser, J., & Siegle, M. (2001). A model checker for performance and dependability properties. In Proceedings of the 2nd PROGRESS Workshop on Embedded Systems 2001 (pp. 83-88). Veldhoven, the Netherlands: STW.