Model Checking Functional and Performability Properties of
Stochastic Fluid Models
Marco Gribaudo - András Horváth
Abstract:
Model checking of stochastic processes has been introduced to verify
functional as well as performability properties of formally specified
systems. In this paper, model checking for a wide class of stochastic fluid
models (SFMs) is considered. We present a branching time temporal logic,
which is similar to the continuous stochastic logic (CSL), for expressing
real-time probabilistic properties of SFMs. The model checking problem for
this logic can be tackled through repetitive application of transient and
steady state analysis of a modified version of the SFM under study. The
complexity of the analysis techniques developed for SFMs depends on the
size of the state space. We present techniques that allow to reduce the
state space in the solution of model checking problems. A case study
illustrates the logic and the model checking procedure.
Postscript
András Horváth, 2008-06-25