Implementing a Model Checker for Perfomability Behaviour

Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle

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

    5 Downloads (Pure)

    Abstract

    We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be veri#ed are speci#ed with the help of the action-based temporal logic aCSL.
    Original languageEnglish
    Title of host publicationProceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5)
    EditorsR. German, J. Lüthi, M. Telek
    Place of PublicationErlangen
    PublisherUniversity of Erlangen
    Number of pages5
    Publication statusPublished - 2001
    Event5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001 - Erlangen, Germany
    Duration: 15 Sep 200116 Sep 2001
    Conference number: 5

    Workshop

    Workshop5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001
    Abbreviated titlePMCCS
    CountryGermany
    CityErlangen
    Period15/09/0116/09/01

    Keywords

    • METIS-204450

    Fingerprint Dive into the research topics of 'Implementing a Model Checker for Perfomability Behaviour'. Together they form a unique fingerprint.

  • Cite this

    Hermanns, H., Katoen, J-P., Meyer-Kayser, J., & Siegle, M. (2001). Implementing a Model Checker for Perfomability Behaviour. In R. German, J. Lüthi, & M. Telek (Eds.), Proceedings of the Fifth International Workshop on Performability Modelling of Computer and Communication Systems (PMCCS 5) Erlangen: University of Erlangen.