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 条
  • [41] Planning in Real-Time Domains with Timed CTL Goals via Symbolic Model Checking
    Stoehr, Daniel
    Glesner, Sabine
    2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2013, : 7 - 14
  • [42] A symbolic model checking approach in formal verification of distributed systems
    Souri, Alireza
    Rahmani, Amir Masoud
    Navimipour, Nima Jafari
    Rezaei, Reza
    HUMAN-CENTRIC COMPUTING AND INFORMATION SCIENCES, 2019, 9 (01):
  • [43] Symbolic model checking for discrete real-time systems
    Xiangyu LUO
    Lijun WU
    Qingliang CHEN
    Haibo LI
    Lixiao ZHENG
    Zuxi CHEN
    Science China(Information Sciences), 2018, 61 (05) : 203 - 225
  • [44] Symbolic model checking for discrete real-time systems
    Xiangyu Luo
    Lijun Wu
    Qingliang Chen
    Haibo Li
    Lixiao Zheng
    Zuxi Chen
    Science China Information Sciences, 2018, 61
  • [45] A finite union of DFAs in symbolic model checking of infinite systems
    Roy, Suman
    Chakraborty, Bhaskar
    IMPLEMENTATION AND APPLICATION OF AUTOMATA, 2006, 4094 : 277 - 278
  • [46] Optimized Symbolic Model Checking for Component-based Systems
    Zhang, Lianyi
    Meng, Qingdi
    Luo, Guiming
    2014 IEEE 13TH INTERNATIONAL CONFERENCE ON COGNITIVE INFORMATICS & COGNITIVE COMPUTING (ICCI-CC), 2014, : 373 - 378
  • [47] Symbolic model checking of hybrid systems using template polyhedra
    Sankaranarayanan, Sriram
    Dang, Thao
    Ivancic, Franjo
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 188 - +
  • [48] Symbolic model checking for discrete real-time systems
    Luo, Xiangyu
    Wu, Lijun
    Chen, Qingliang
    Li, Haibo
    Zheng, Lixiao
    Chen, Zuxi
    SCIENCE CHINA-INFORMATION SCIENCES, 2018, 61 (05)
  • [49] A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking
    Jacobsen, Lasse
    Jacobsen, Morten
    Moller, Mikael H.
    Srba, Jiri
    COMPUTER PERFORMANCE ENGINEERING, 2010, 6342 : 83 - 98
  • [50] Interpolants and symbolic model checking
    McMillan, K. L.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2007, 4349 : 89 - 90
12345