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 条
  • [21] Model checking of systems with many identical timed processes
    Abdulla, PA
    Jonsson, B
    THEORETICAL COMPUTER SCIENCE, 2003, 290 (01) : 241 - 264
  • [22] Checking EMTLK Properties of Timed Interpreted Systems Via Bounded Model Checking
    Bożena Woźna-Szcześniak
    Andrzej Zbrzezny
    Studia Logica, 2016, 104 : 641 - 678
  • [23] Checking EMTLK Properties of Timed Interpreted Systems Via Bounded Model Checking
    Wozna-Szczesniak, Bozena
    Zbrzezny, Andrzej
    STUDIA LOGICA, 2016, 104 (04) : 641 - 678
  • [24] Checking EMTLK Properties of Timed Interpreted Systems via Bounded Model Checking
    Wozna-Szczesniak, Bozena
    AAMAS'14: PROCEEDINGS OF THE 2014 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2014, : 1477 - 1478
  • [25] Structural symbolic CTL model checking of asynchronous systems
    Ciardo, G
    Siminiceanu, R
    COMPUTER AIDED VERIFICATION, 2003, 2725 : 40 - 53
  • [26] Symbolic model checking of real-time systems
    Logothetis, G
    Schneider, K
    EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2001, : 214 - 223
  • [27] Forward symbolic model checking for real time systems
    Logothetis, Georgios
    ASP-DAC 2005: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2005, : 1043 - 1046
  • [28] Testing distributed systems through symbolic model checking
    Kalyon, Gabriel
    Massart, Thierry
    Meuter, Cedric
    Van Begin, Laurent
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2007, 2007, 4574 : 263 - +
  • [29] SYMBOLIC MODEL CHECKING FOR REAL-TIME SYSTEMS
    HENZINGER, TA
    NICOLLIN, X
    SIFAKIS, J
    YOVINE, S
    INFORMATION AND COMPUTATION, 1994, 111 (02) : 193 - 244
  • [30] Symbolic model checking of stochastic systems: Theory and implementation
    Kuntz, M
    Siegle, M
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2006, 3925 : 89 - 107
12345