Model Checking Functional and Performability Properties of Stochastic Fluid Models

被引:2
作者
Gribaudo, Marco [1 ]
Horvath, Andras [1 ]
机构
[1] Univ Torino, Dipartimento Informat, Turin, Italy
关键词
Model checking; probabilistic verification; stochastic fluid models;
D O I
10.1016/j.entcs.2005.04.018
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:295 / 310
页数:16
相关论文
共 18 条
  • [1] A THEORY OF TIMED AUTOMATA
    ALUR, R
    DILL, DL
    [J]. THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) : 183 - 235
  • [2] Alur R., 1990, LICS, P414
  • [3] Alur R., 1992, LECTURE NOTES COMPUT, V736, P209, DOI DOI 10.1007/3-540-57318-6_30
  • [4] Aziz Adnan, 2000, ACM T COMPUT LOG, V1, P162, DOI [10.1145/343369.343402, DOI 10.1145/343369.343402]
  • [5] Baier C, 2000, LECT NOTES COMPUT SC, V1853, P780
  • [6] BAIER C, 2000, LNCS, V1855, P358
  • [7] Discrete-event simulation of fluid stochastic Petri nets
    Ciardo, G
    Nicol, DM
    Trivedi, KS
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1999, 25 (02) : 207 - 217
  • [8] AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS
    CLARKE, EM
    EMERSON, EA
    SISTLA, AP
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02): : 244 - 263
  • [9] USING BRANCHING TIME TEMPORAL LOGIC TO SYNTHESIZE SYNCHRONIZATION SKELETONS
    EMERSON, EA
    CLARKE, EM
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 1982, 2 (03) : 241 - 266
  • [10] Fluid Petri Nets and hybrid model-checking:: a comparative case study
    Gribaudo, M
    Horváth, A
    Bobbio, A
    Tronci, E
    Ciancamerla, E
    Minichino, M
    [J]. RELIABILITY ENGINEERING & SYSTEM SAFETY, 2003, 81 (03) : 239 - 257