On the Use of Model Checking Techniques for Quantitative Dependability Evaluation

    Research output: Contribution to conferencePaperAcademicpeer-review

    39 Downloads (Pure)

    Abstract

    Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras, or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.
    Original languageUndefined
    Pages228-237
    Number of pages10
    DOIs
    Publication statusPublished - 2000

    Keywords

    • IR-63278
    • EWI-6443
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-PM: PROBABILISTIC METHODS
    • FMT-MC: MODEL CHECKING

    Cite this

    @conference{06d0b473dd5e4e478c0a95653e8c7568,
    title = "On the Use of Model Checking Techniques for Quantitative Dependability Evaluation",
    abstract = "Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras, or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.",
    keywords = "IR-63278, EWI-6443, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-PM: PROBABILISTIC METHODS, FMT-MC: MODEL CHECKING",
    author = "Haverkort, {Boudewijn R.H.M.} and H. Hermanns and Katoen, {Joost P.}",
    year = "2000",
    doi = "10.1109/RELDI.2000.885410",
    language = "Undefined",
    pages = "228--237",

    }

    On the Use of Model Checking Techniques for Quantitative Dependability Evaluation. / Haverkort, Boudewijn R.H.M.; Hermanns, H.; Katoen, Joost P.

    2000. 228-237.

    Research output: Contribution to conferencePaperAcademicpeer-review

    TY - CONF

    T1 - On the Use of Model Checking Techniques for Quantitative Dependability Evaluation

    AU - Haverkort, Boudewijn R.H.M.

    AU - Hermanns, H.

    AU - Katoen, Joost P.

    PY - 2000

    Y1 - 2000

    N2 - Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras, or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.

    AB - Over the last two decades, many techniques have been developed to specify and evaluate Markovian dependability models. Most often, these Markovian models are automatically derived from stochastic Petri nets, stochastic process algebras, or stochastic activity networks. However, whereas the model specification has become very comfortable, the specification of the dependability measures of interest most often has remained cumbersome. In this paper, we show that our recently introduced logic CSL (continuous stochastic logic) provides ample means to specify state- as well as path-based dependability measures in a compact and flexible way. Moreover, due to the formal syntax and semantics of CSL, we can exploit the structure of CSL-specified dependability measures in the dependability evaluation process. Typically, the underlying Markov chains that need to be evaluated can be reduced considerably in size by this structure exploitation.

    KW - IR-63278

    KW - EWI-6443

    KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

    KW - FMT-PM: PROBABILISTIC METHODS

    KW - FMT-MC: MODEL CHECKING

    U2 - 10.1109/RELDI.2000.885410

    DO - 10.1109/RELDI.2000.885410

    M3 - Paper

    SP - 228

    EP - 237

    ER -