Model checking procedures for infinite state systems

被引：1
|
作者：
Bogunovic, Nikola [1 ]
Pek, Edgar [1 ]
机构：
[1] Univ Zagreb, Fac Elect & Comp Engn, Unska 3, Zagreb 1000, Croatia
来源：
13TH ANNUAL IEEE INTERNATIONAL SYMPOSIUM AND WORKSHOP ON ENGINEERING OF COMPUTER BASED SYSTEMS, PROCEEDINGS: MASTERING THE COMPLEXITY OF COMPUTER-BASED SYSTEMS | 2006年
关键词：
D O I：
10.1109/ECBS.2006.46
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
The paper depicts experiments and results with predicate abstraction based verification applied to infinite state systems. Predicate abstraction is a method for automatic construction of abstract state space that can be used by any common finite state model checking tool, such as NuSMV We have used abstract state space and NuSMV tool to verify safety properties of infinite state mutual exclusion protocols. Even though predicate abstraction allows model checking against a restricted class of temporal logic formulas, we have shown that the restricted class is expressive enough to specify basic safety properties. Our experiments were conducted on Bakery and Fischer mutual exclusion protocols.
引用
收藏
页码：419 / +
页数：2
相关论文
共 50 条
  • [1] Bounded model checking of infinite state systems
    Tobias Schuele
    Klaus Schneider
    Formal Methods in System Design, 2007, 30 : 51 - 81
  • [2] Bounded model checking of infinite state systems
    Schuele, Tobias
    Schneider, Klaus
    FORMAL METHODS IN SYSTEM DESIGN, 2007, 30 (01) : 51 - 81
  • [3] Verification of infinite state systems by compositional model checking
    McMillan, KL
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 : 219 - 233
  • [4] A Decidability Result for the Model Checking of Infinite-State Systems
    Daniele Zucchelli
    Enrica Nicolini
    Journal of Automated Reasoning, 2012, 48 : 1 - 42
  • [5] Decidability of model checking for infinite-state concurrent systems
    Javier Esparza
    Acta Informatica, 1997, 34 : 85 - 107
  • [6] A Decidability Result for the Model Checking of Infinite-State Systems
    Zucchelli, Daniele
    Nicolini, Enrica
    JOURNAL OF AUTOMATED REASONING, 2012, 48 (01) : 1 - 42
  • [7] Global model-checking of infinite-state systems
    Piterman, N
    Vardi, MY
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 387 - 400
  • [8] Decidability of model checking for infinite-state concurrent systems
    Esparza, J
    ACTA INFORMATICA, 1997, 34 (02) : 85 - 107
  • [9] On model checking for non-deterministic infinite-state systems
    Emerson, EA
    Namjoshi, KS
    THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1998, : 70 - 80
  • [10] Bounded model checking of infinite state systems: Exploiting the automata hierarchy
    Schuele, T
    Schneider, K
    SECOND ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2004, : 17 - 26
12345