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 条
  • [1] Symbolic model checking APSL
    Wanwei Liu
    Ji Wang
    Huowang Chen
    Xiaodong Ma
    Zhaofei Wang
    Frontiers of Computer Science in China, 2009, 3 : 130 - 141
  • [2] Symbolic model checking APSL
    Liu, Wanwei
    Wang, Ji
    Chen, Huowang
    Ma, Xiaodong
    Wang, Zhaofei
    FRONTIERS OF COMPUTER SCIENCE IN CHINA, 2009, 3 (01): : 130 - 141
  • [3] Symbolic model checking
    McMillan, KL
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
  • [4] Interpolants and symbolic model checking
    McMillan, K. L.
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2007, 4349 : 89 - 90
  • [5] On partitioning and symbolic model checking
    Iyer, S
    Sahoo, D
    Emerson, EA
    Jain, J
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2005, 25 (05) : 780 - 788
  • [6] On partitioning and symbolic model checking
    Iyer, S
    Sahoo, D
    Emerson, EA
    Jain, J
    FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 497 - 511
  • [7] Lazy symbolic model checking
    Yang, J
    Tiemeyer, A
    37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000, 2000, : 35 - 38
  • [8] Symbolic Causality Checking Using Bounded Model Checking
    Beer, Adrian
    Heidinger, Stephan
    Kuehne, Uwe
    Leitner-Fischer, Florian
    Leue, Stefan
    MODEL CHECKING SOFTWARE, SPIN 2015, 2015, 9232 : 203 - 221
  • [9] Unit checking: Symbolic model checking for a unit of code
    Gunter, E
    Peled, D
    VERIFICATION: THEORY AND PRACTICE: ESSAYS DEDICATED TO ZHOAR MANNA ON THE OCCASION OF HIS 64TH BIRTHDAY, 2003, 2772 : 548 - 567
  • [10] Symbolic model checking for probabilistic processes
    Baier, C
    Clarke, EM
    Hartonas-Garmhausen, V
    Kwiatkowska, M
    Ryan, M
    AUTOMATA, LANGUAGES AND PROGRAMMING, 1997, 1256 : 430 - 440
12345