ACTL* properties and bounded model checking

被引：0
|
作者：
Wozna, B
机构：
[1] Pedagogical Univ Czestochowa, Inst Math & Comp Sci, PL-42200 Czestochowa, Poland
[2] Kings Coll London, Dept Comp Sci, London WC2R 2LS, England
来源：
FUNDAMENTA INFORMATICAE | 2004年 / 63卷 / 01期
关键词：
bounded model checking; logic ACTL* (ECTL*); bounded semantics; translation to SAT;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The main contribution of the paper consists in showing that the bounded model checking (BMC) method is feasible for ACTL* (the universal fragment of CTL*) which subsumes both ACTL and LTL. The extension to ACTL* is obtained by redefining the function returning the sufficient number of executions over which an ACTL* formula is checked, and then combining the two known translations to SAT for ACTL and LTL formulas. The proposed translation of ACTL* formulas is essentially different from the existing translations of both ACTL and LTL formulas. Moreover, the formal treatment is the basis for the implementation of the technique in the symbolic model checker Verics.
引用
收藏
页码：65 / 87
页数：23
相关论文
共 50 条
  • [1] Verification of ACTL properties by bounded model checking
    Zhang, Wenhui
    COMPUTER AIDED SYSTEMS THEORY- EUROCAST 2007, 2007, 4739 : 556 - 563
  • [2] Bounded Model Checking of ACTL formulae
    Chen, Wei
    Zhang, Wenhui
    THIRD INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2009, : 90 - 99
  • [3] Checking ACTL* properties of discrete timed automata via bounded model checking
    Wozna, B
    Zbrzezny, A
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2003, 2791 : 18 - 33
  • [4] Evaluation of SAT-based bounded model checking of ACTL properties
    Xu, Yanyan
    Chen, Wei
    Xu, Liang
    Zhang, Wenhui
    TASE 2007: FIRST JOINT IEEE/IFIP SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2007, : 339 - +
  • [5] Model checking ACTL constrained processes
    Chen, XJ
    FRONTIERS OF COMBINING SYSTEMS, 1996, 3 : 377 - 388
  • [6] Proving more properties with bounded model checking
    Awedh, M
    Somenzi, F
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 96 - 108
  • [7] Accelerating bounded model checking of safety properties
    Strichman, O
    FORMAL METHODS IN SYSTEM DESIGN, 2004, 24 (01) : 5 - 24
  • [8] Bounded Model Checking for All Regular Properties
    Jehle, Markus
    Johannsen, Jan
    Lange, Martin
    Rachinsky, Nicolas
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (01) : 3 - 18
  • [9] Accelerating Bounded Model Checking of Safety Properties
    Ofer Strichman
    Formal Methods in System Design, 2004, 24 : 5 - 24
  • [10] Checking nested properties using bounded model checking and sequential ATPG
    Qiang, Q
    Saab, DG
    Abraham, JA
    19TH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 2005, : 225 - 230
12345