Implementing a Model Checker for Performability Behaviour

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

    Research output: Contribution to conferencePaper

    15 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

    Hermanns, H., German, R. (Ed.), Katoen, J. P., & Meyer-Kayser, J. (2001). Implementing a Model Checker for Performability Behaviour. 110-114. Paper presented at 5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001, Erlangen, Germany.
    Hermanns, H. ; German, R. (Editor) ; Katoen, Joost P. ; Meyer-Kayser, J. / Implementing a Model Checker for Performability Behaviour. Paper presented at 5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001, Erlangen, Germany.5 p.
    @conference{8f73beba0c974faf84b000816db0e109,
    title = "Implementing a Model Checker for Performability Behaviour",
    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.",
    keywords = "FMT-PA: PROCESS ALGEBRAS, FMT-PM: PROBABILISTIC METHODS, IR-66282, EWI-6518, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-TOOLS",
    author = "H. Hermanns and R. German and Katoen, {Joost P.} and J. Meyer-Kayser",
    year = "2001",
    language = "Undefined",
    pages = "110--114",
    note = "null ; Conference date: 15-09-2001 Through 16-09-2001",

    }

    Hermanns, H, German, R (ed.), Katoen, JP & Meyer-Kayser, J 2001, 'Implementing a Model Checker for Performability Behaviour' Paper presented at 5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001, Erlangen, Germany, 15/09/01 - 16/09/01, pp. 110-114.

    Implementing a Model Checker for Performability Behaviour. / Hermanns, H.; German, R. (Editor); Katoen, Joost P.; Meyer-Kayser, J.

    2001. 110-114 Paper presented at 5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001, Erlangen, Germany.

    Research output: Contribution to conferencePaper

    TY - CONF

    T1 - Implementing a Model Checker for Performability Behaviour

    AU - Hermanns, H.

    AU - Katoen, Joost P.

    AU - Meyer-Kayser, J.

    A2 - German, R.

    PY - 2001

    Y1 - 2001

    N2 - 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.

    AB - 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.

    KW - FMT-PA: PROCESS ALGEBRAS

    KW - FMT-PM: PROBABILISTIC METHODS

    KW - IR-66282

    KW - EWI-6518

    KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

    KW - FMT-TOOLS

    M3 - Paper

    SP - 110

    EP - 114

    ER -

    Hermanns H, German R, (ed.), Katoen JP, Meyer-Kayser J. Implementing a Model Checker for Performability Behaviour. 2001. Paper presented at 5th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2001, Erlangen, Germany.