Model-checking performability properties

Boudewijn R.H.M. Haverkort, L. Cloth, H. Hermanns, Joost P. Katoen, Christel Baier

    Research output: Contribution to conferencePaper

    14 Downloads (Pure)

    Abstract

    Model checking has been introduced as an automated technique to verify whether functional properties, expressed in a formal logic like computational tree logic (CTL), do hold in a formally-specified system. We present a number of computational procedures to perform model checking of continuous stochastic reward logic (CSRL) over finite Markov reward models, thereby stressing their computational complexity (time and space) and applicability from a practical point of view (accuracy, stability). A case study in the area of ad hoc mobile computing under power constraints shows the merits of CSRL and the new computational procedures.
    Original languageEnglish
    Pages103-112
    Number of pages10
    DOIs
    Publication statusPublished - 2002
    EventInternational Conference on Dependable Systems and Networks, DSN 2002 - Washington, United States
    Duration: 23 Jun 200226 Jun 2002

    Other

    OtherInternational Conference on Dependable Systems and Networks, DSN 2002
    Abbreviated titleDSN
    CountryUnited States
    CityWashington
    Period23/06/0226/06/02

      Fingerprint

    Keywords

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

    Cite this

    Haverkort, B. R. H. M., Cloth, L., Hermanns, H., Katoen, J. P., & Baier, C. (2002). Model-checking performability properties. 103-112. Paper presented at International Conference on Dependable Systems and Networks, DSN 2002, Washington, United States. https://doi.org/10.1109/DSN.2002.1028891