Model Sketching by Abstraction Refinement for Lifted Model Checking

被引:1
|
作者
Dimovski, Aleksandar S. [1 ]
机构
[1] Mother Teresa Univ, Fac Informat, Skopje, North Macedonia
关键词
Model sketching; Product-line (lifted) model checking;
D O I
10.1145/3477314.3507170
中图分类号
TP39 [计算机的应用];
学科分类号
081203 ; 0835 ;
摘要
In this work, we show how the use of verification and analysis techniques for model families (software product lines) with numerical features provides an interesting technique to synthesize complete models from sketches (i.e. partial models with holes). In particular, we present an approach for synthesizing Promela model sketches using variability-specific abstraction refinement for lifted (familybased) model checking.
引用
收藏
页码:1845 / 1848
页数:4
相关论文
共 50 条
  • [1] Abstraction and refinement in model checking
    Grumberg, Orna
    [J]. FORMAL METHODS FOR COMPONENTS AND OBJECTS, 2006, 4111 : 219 - 242
  • [2] 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
  • [3] 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
  • [4] Software model checking with abstraction refinement
    Podelski, A
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2003, 2575 : 1 - 3
  • [5] Abstraction refinement for bounded model checking
    Gupta, A
    Strichman, O
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2005, 3576 : 112 - 124
  • [6] A Multiple Refinement Approach in Abstraction Model Checking
    Nguyen, Phan T. H.
    Bui, Thang H.
    [J]. COMPUTER INFORMATION SYSTEMS AND INDUSTRIAL MANAGEMENT, CISIM 2014, 2014, 8838 : 433 - 444
  • [7] Relative completeness of abstraction refinement for software model checking
    Ball, T
    Podelski, A
    Rajamani, SK
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 158 - 172
  • [8] Integrating Evolutionary Computation with Abstraction Refinement for Model Checking
    He, Fei
    Song, Xiaoyu
    Hung, William N. N.
    Gu, Ming
    Sun, Jiaguang
    [J]. IEEE TRANSACTIONS ON COMPUTERS, 2010, 59 (01) : 116 - 126
  • [9] An efficient approach for abstraction-refinement in model checking
    Tian, Cong
    Duan, Zhenhua
    Zhang, Nan
    [J]. THEORETICAL COMPUTER SCIENCE, 2012, 461 : 76 - 85
  • [10] Combining abstraction refinement and SAT-Based model checking
    Amla, Nina
    McMillan, Kenneth L.
    [J]. Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, 2007, 4424 : 405 - 419