VERIFYING AUTOMATA SPECIFICATIONS OF PROBABILISTIC REAL-TIME SYSTEMS

被引:0
|
作者
ALUR, R
COURCOUBETIS, C
DILL, D
机构
[1] AT&T BELL LABS,MURRAY HILL,NJ 07974
[2] UNIV CRETE,DEPT COMP SCI,IRAKLION,GREECE
[3] FORTH,INST COMP SCI,GR-71110 IRAKLION,GREECE
[4] STANFORD UNIV,DEPT COMP SCI,STANFORD,CA 94305
关键词
REAL-TIME; PROBABILISTIC SYSTEMS; AUTOMATIC VERIFICATION;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We present a model-checking algorithm for a system presented as a generalized semi-Markov process and a specification given as a deterministic timed automaton. This leads to a method for automatic verification of timing properties of finite-state probabilistic real-time systems.
引用
收藏
页码:28 / 44
页数:17
相关论文
共 50 条
  • [1] Verifying automata specification of distributed probabilistic real-time systems
    Luo Tiegeng
    Chen Huowang
    Wang Bingshan
    Wang Ji
    Gong Zhenghu
    Qi Zhichang
    [J]. Journal of Computer Science and Technology, 1998, 13 (6): : 588 - 596
  • [2] Verifying Automata Specification ofDistributed Probabilistic Real-Time Systems
    罗铁庚
    陈火旺
    王兵山
    王戟
    龚正虎
    齐治昌
    [J]. Journal of Computer Science & Technology, 1998, (06) : 588 - 596
  • [3] A note on the verification of automata specifications of probabilistic real-time systems
    Moura, AV
    Pinto, GA
    [J]. INFORMATION PROCESSING LETTERS, 2002, 82 (05) : 223 - 228
  • [4] VERIFYING PROPERTIES OF HMS MACHINE SPECIFICATIONS OF REAL-TIME SYSTEMS
    GABRIELIAN, A
    IYER, R
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 575 : 421 - 431
  • [5] Verifying Linear Real-Time Logic specifications
    Andrei, Stefan
    Cheng, Albert M. K.
    [J]. RTSS 2007: 28TH IEEE INTERNATIONAL REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2007, : 333 - +
  • [6] Towards Verifying Safety Properties of Real-Time Probabilistic Systems
    Han, Fenglin
    Blech, Jan Olaf
    Herrmann, Peter
    Schmidt, Heinz
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (147): : 1 - 15
  • [7] COMPILING REAL-TIME SPECIFICATIONS INTO EXTENDED AUTOMATA
    NICOLLIN, X
    SIFAKIS, J
    YOVINE, S
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1992, 18 (09) : 794 - 804
  • [8] A timed automata semantics for real-time UML specifications
    Toetenel, H
    Roubtsova, E
    van Katwijk, J
    [J]. IEEE SYMPOSIA ON HUMAN-CENTRIC COMPUTING LANGUAGES AND ENVIRONMENTS, PROCEEDINGS, 2001, : 88 - 95
  • [9] Online Induction of Probabilistic Real-Time Automata
    Jana Schmidt
    Stefan Kramer
    [J]. Journal of Computer Science and Technology, 2014, 29 : 345 - 360
  • [10] Online Induction of Probabilistic Real-Time Automata
    Schmidt, Jana
    Kramer, Stefan
    [J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2014, 29 (03): : 345 - 360