Symbolic model checking APSL

被引：0
|
作者：
Liu, Wanwei [1 ]
Wang, Ji [1 ]
Chen, Huowang [1 ]
Ma, Xiaodong [1 ]
机构：
[1] Natl Univ Def Technol, Sch Comp, Natl Lab Parallel & Distributed Proc, Hunan, Peoples R China
来源：
TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS | 2008年
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
PSL is a kind of temporal logic which uses SEREs as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. In this paper we extend the LTL symbolic model checking algorithm to that of APSL, and present a tableau based APSL verification approach. Moreover we show how to implement this algorithm via the BDD based symbolic approach.
引用
收藏
页码：39 / 46
页数：8
相关论文
共 50 条
  • [41] GENERATING BDDS FOR SYMBOLIC MODEL CHECKING IN CCS
    ENDERS, R
    FILKORN, T
    TAUBNER, D
    DISTRIBUTED COMPUTING, 1993, 6 (03) : 155 - 164
  • [42] Verification of CTLBDI Properties by Symbolic Model Checking
    Chen, Ran
    Zhang, Wenhui
    2019 26TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), 2019, : 102 - 109
  • [43] MOXI: An Intermediate Language for Symbolic Model Checking
    Rozier, Kristin Yvonne
    Dureja, Rohit
    Irfan, Ahmed
    Johannsen, Chris
    Nukala, Karthik
    Shankar, Natarajan
    Tinelli, Cesare
    Vardi, Moshe Y.
    MODEL CHECKING SOFTWARE, SPIN 2024, 2025, 14624 : 26 - 46
  • [44] Generalized symbolic execution for model checking and testing
    Khurshid, S
    Pasareanu, CS
    Visser, W
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2003, 2619 : 553 - 568
  • [45] Approximate symbolic model checking for incomplete designs
    Nopper, T
    Scholl, C
    FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2004, 3312 : 290 - 305
  • [46] Symbolic model checking with fewer fixpoint computations
    Déharbe, D
    Moreira, AM
    FM'99-FORMAL METHODS, 1999, 1708 : 272 - 288
  • [47] Symbolic Model Checking Using Intervals of Vectors
    Morard, Damien
    Donati, Lucas
    Buchs, Didier
    APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2024, 2024, 14628 : 269 - 290
  • [48] Adaptive variable reordering for symbolic model checking
    Kamhi, G
    Fix, L
    1998 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN: DIGEST OF TECHNICAL PAPERS, 1998, : 359 - 365
  • [49] Symbolic partial model checking for security analysis
    Martinelli, F
    COMPUTER NETWORK SECURITY, 2003, 2776 : 122 - 134
  • [50] Conformant planning via symbolic model checking
    Cimatti, A
    Roveri, M
    JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2000, 13 : 305 - 338
12345