Symbolic model checking for simply-timed systems

被引：0
|
作者：
Markey, N
Schnoebelen, P
机构：
[1] Free Univ Brussels, Dept Informat, Brussels, Belgium
[2] ENS Cachan, Lab Specificat & Verificat, Cachan, France
[3] CNRS, UMR 8643, Cachan, France
来源：
FORMAL TECHNIQUES, MODELLING AND ANALYSIS OF TIMED AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS | 2004年 / 3253卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We describe OBDD-based symbolic model checking algorithms for simply-timed systems, i.e. finite state graphs where transitions carry a duration. These durations can be arbitrary natural numbers. A simple and natural semantics for these systems opens the way for improved efficiency. Our algorithms have been implemented in NuSMV and perform well in practice (on standard case studies).
引用
收藏
页码：102 / 117
页数：16
相关论文
共 50 条
  • [1] Symbolic model checking for probabilistic timed automata
    Kwiatkowska, M
    Norman, G
    Sproston, J
    Wang, FZ
    FORMAL TECHNIQUES, MODELLING AND ANALYSIS OF TIMED AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2004, 3253 : 293 - 308
  • [2] Symbolic model checking for probabilistic timed automata
    Kwiatkowska, Marta
    Norman, Gethin
    Sproston, Jeremy
    Wang, Fuzhi
    INFORMATION AND COMPUTATION, 2007, 205 (07) : 1027 - 1077
  • [3] RTL verification of timed asynchronous and heterogeneous systems using symbolic model checking
    Vakilotojar, V
    Beerel, PA
    INTEGRATION-THE VLSI JOURNAL, 1997, 24 (01) : 19 - 35
  • [4] RTL verification of timed asynchronous and heterogeneous systems using symbolic model checking
    Vakilotojar, V
    Beerel, PA
    PROCEEDINGS OF THE ASP-DAC '97 - ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE 1997, 1996, : 181 - 188
  • [5] Symbolic model checking of finite precision timed automata
    Yan, RJ
    Li, GY
    Tang, ZS
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2005, 2005, 3722 : 272 - 287
  • [6] Using MTBDDs for discrete timed symbolic model checking
    Kropf, T
    Ruf, J
    EUROPEAN DESIGN & TEST CONFERENCE - ED&TC 97, PROCEEDINGS, 1997, : 182 - 187
  • [7] A new algorithm for discrete timed symbolic model checking
    Ruf, J
    Kropf, T
    HYBRID AND REAL-TIME SYSTEMS, 1997, 1201 : 18 - 32
  • [8] Model checking timed systems with urgencies
    Hsiung, Pao-Ann
    Lin, Shang-Wei
    Chen, Yean-Ru
    Huang, Chun-Hsian
    Yeh, Jia-Jen
    Sun, Hong-Yu
    Lin, Chao-Sheng
    Liao, Hsiao-Win
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2006, 4218 : 67 - 81
  • [9] Bounded model checking for timed systems
    Audemard, G
    Cimatti, A
    Kornilowicz, A
    Sebastiani, R
    FORMAL TECHNIQUE FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2002, PROCEEDINGS, 2002, 2529 : 243 - 259
  • [10] Model Checking Prioritized Timed Systems
    Lin, Shang-Wei
    Hsiung, Pao-Ann
    IEEE TRANSACTIONS ON COMPUTERS, 2012, 61 (06) : 843 - 856
12345