Model checking performability properties

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

Full description

Saved in:
Bibliographic Details
Main Authors: Haverkort, B., Cloth, L., Hermanns, H., Katoen, J.-P., Baier, C.
Format: Conference Proceeding
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Area measurement
Automatic logic units
Computational modeling
Computer science
Computer science
control theory
systems
Context modeling
Costs
Exact sciences and technology
Mobile computing
Performance evaluation
Steady-state
Stochastic processes
Theoretical computing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
DOI:10.1109/DSN.2002.1028891