Tearing based automatic abstraction for CTL model checking

被引:0
|
作者
Lee, W
Pardo, A
Jang, JY
Hachtel, G
Somenzi, F
机构
关键词
D O I
暂无
中图分类号
T [工业技术];
学科分类号
08 ;
摘要
In this paper we present the tearing paradigm as a way to automatically abstract behavior to obtain upper and lower bound approximations of a reactive system. We present algorithms that exploit the bounds to perform conservative ECTL and ACTL model checking. We also give an algorithm for false negative (or false positive) resolution for verification based on a theory of lattice of approximations. We show that there exists a bipartition of the lattice set based on positive versus negative verification results. Our resolution methods are based on determining a pseudo-optimal shortest path from a given, possibly coarse but tractable approximation, to a nearest point on the contour separating one set of the bipartition from the other.
引用
收藏
页码:76 / 81
页数:6
相关论文
共 50 条
  • [1] Formula-dependent abstraction for CTL model checking
    Qian, Junyan
    Zhao, Lingzhong
    Cai, Guoyong
    Gu, Tianlong
    [J]. COMPUTATIONAL SCIENCE AND ITS APPLICATIONS - ICCSA 2008, PT 2, PROCEEDINGS, 2008, 5073 : 1035 - 1048
  • [2] Variability Abstraction and Refinement for Game-Based Lifted Model Checking of Full CTL
    Dimovski, Aleksandar S.
    Legay, Axel
    Wasowski, Andrzej
    [J]. FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2019), 2019, 11424 : 192 - 209
  • [3] Generalized abstraction-refinement for game-based CTL lifted model checking
    Dimovski, Aleksandar S.
    Legay, Axel
    Wasowski, Andrzej
    [J]. THEORETICAL COMPUTER SCIENCE, 2020, 837 (837) : 181 - 206
  • [4] CTL Model Checking based on Giraph
    Duan, Tingyin
    Zhou, Qinglei
    Pan, Shan
    Zhu, Weijun
    [J]. PROCEEDINGS OF THE 2016 5TH INTERNATIONAL CONFERENCE ON ADVANCED MATERIALS AND COMPUTER SCIENCE, 2016, 80 : 652 - 657
  • [5] Automatic abstraction techniques for propositional μ-calculus model checking
    Pardo, A
    Hachtel, GD
    [J]. COMPUTER AIDED VERIFICATION, 1997, 1254 : 12 - 23
  • [6] CTL Model Checking based on Probe Machine
    Zhu, Weijun
    Liu, Yichen
    Li, En
    [J]. PROCEEDINGS OF 2019 IEEE 10TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS 2019), 2019, : 518 - 522
  • [7] Bounded Saturation Based CTL Model Checking
    Voeroes, Andras
    Darvas, Daniel
    Bartha, Tamas
    [J]. 12TH SYMPOSIUM ON PROGRAMMING LANGUAGES AND SOFTWARE TOOLS, SPLST' 11, 2011, : 149 - 160
  • [8] Abstraction-based model checking programs
    Qian, Junyan
    Xu, Baowen
    Zhang, Yingzhou
    [J]. Journal of Computational Information Systems, 2007, 3 (02): : 675 - 682
  • [9] MODEL CHECKING AND ABSTRACTION
    CLARKE, EM
    GRUMBERG, O
    LONG, DE
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1994, 16 (05): : 1512 - 1542
  • [10] Assumption-based distribution of CTL model checking
    Brim L.
    Yorav K.
    Žídková J.
    [J]. International Journal on Software Tools for Technology Transfer, 2005, 7 (1) : 61 - 73