Implementing a Model Checker for Performability Behaviour

H. Hermanns, R. German (Editor), Joost P. Katoen, J. Meyer-Kayser

    Research output: Contribution to conferencePaperpeer-review

    24 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 verified are specified with the help of the action-based temporal logic aCSL. The technique is currently being implemented in our freely available prototype tool ETMCC.
    Original languageUndefined
    Pages110-114
    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

    • FMT-PA: PROCESS ALGEBRAS
    • FMT-PM: PROBABILISTIC METHODS
    • IR-66282
    • EWI-6518
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-TOOLS

    Cite this