Automatic abstraction for verification of timed circuits and systems

被引：0
|
作者：
Zheng, H [1 ]
Mercer, E [1 ]
Myers, C [1 ]
机构：
[1] Univ Utah, Salt Lake City, UT 84112 USA
来源：
COMPUTER AIDED VERIFICATION, PROCEEDINGS | 2001年 / 2102卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper presents a new approach for verification of asynchronous circuits by using automatic abstraction. It attacks the state explosion problem by avoiding the generation of a flat state space for the whole design. Instead, it breaks the design into blocks and conducts verification on each of them. Using this approach, the speed of verification improves dramatically.
引用
收藏
页码：182 / 193
页数：12
相关论文
共 50 条
  • [31] Specification and verification of timed lazy systems
    Corradini, F
    Pistore, M
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1996, 1996, 1113 : 279 - 290
  • [32] Verification of timed systems using POSETs
    Belluomini, W
    Myers, CJ
    COMPUTER AIDED VERIFICATION, 1998, 1427 : 403 - 415
  • [33] Compositional Verification of Parameterised Timed Systems
    Astefanoaei, Lacramioara
    Ben Rayana, Souha
    Bensalem, Saddek
    Bozga, Marius
    Combaz, Jacques
    NASA FORMAL METHODS (NFM 2015), 2015, 9058 : 66 - 81
  • [34] Automatic Verification of Golog Programs via Predicate Abstraction
    Mo, Peiming
    Li, Naiqi
    Liu, Yongmei
    ECAI 2016: 22ND EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2016, 285 : 760 - 768
  • [35] Automatic Verification of RMA Programs via Abstraction Extrapolation
    Baumann, Cedric
    Dan, Andrei Marian
    Meshman, Yuri
    Hoefler, Torsten
    Vechev, Martin
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2018), 2018, 10747 : 47 - 70
  • [36] Abstraction techniques to improve scalability of equivalence verification for NCL circuits
    Wijayasekara, V. M.
    Rollie, A. T., II
    Hodges, R. G.
    Srinivasan, S. K.
    Smith, S. C.
    ELECTRONICS LETTERS, 2016, 52 (19) : 1594 - 1596
  • [37] Automatic synthesis of schedulers in timed systems
    Krishnan, Padmanabhan
    Electronic Notes in Theoretical Computer Science, 2000, 31 : 118 - 131
  • [38] Scaling up UPPAAL - Automatic verification of real-time systems using compositionality and abstraction
    Jensen, HE
    Larsen, KG
    Skou, A
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, PROCEEDINGS, 2000, 1926 : 19 - 30
  • [39] Symbolic verification and analysis of discrete timed systems
    Ruf, J
    Kropf, T
    FORMAL METHODS IN SYSTEM DESIGN, 2003, 23 (01) : 67 - 108
  • [40] Automatic verification of multi-queue discrete timed automata
    San Pietro, P
    Dang, Z
    COMPUTING AND COMBINATORICS, PROCEEDINGS, 2003, 2697 : 159 - 171
12345