Model checking of stochastic processes has been introduced to verify functional as well as performa- bility 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.

Model checking functional and performability properties of stochastic fluid models

GRIBAUDO, MARCO;
2005

Abstract

Model checking of stochastic processes has been introduced to verify functional as well as performa- bility 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.
Model checking, Probabilistic verification, Stochastic fluid models
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11311/1006450
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact