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 条
  • [31] TLA+ Model Checking Made Symbolic
    Konnov, Igor
    Kukovec, Jure
    Tran, Thanh-Hai
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (OOPSLA):
  • [32] Symbolic model checking of UML activity diagrams
    Eshuis, R
    ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2006, 15 (01) : 1 - 38
  • [33] Approximate symbolic model checking for incomplete designs
    Nopper, T
    Scholl, C
    FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2004, 3312 : 290 - 305
  • [34] Symbolic model checking for asynchronous Boolean programs
    Cook, B
    Kroening, D
    Sharygina, N
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2005, 3639 : 75 - 90
  • [35] Symbolic model checking of public announcement protocols
    Charrier, Tristan
    Pinchinat, Sophie
    Schwarzentruber, Francois
    JOURNAL OF LOGIC AND COMPUTATION, 2019, 29 (08) : 1211 - 1249
  • [36] Efficient Symbolic Model Checking for Process Algebras
    Vander Meulen, Jose
    Pecheur, Charles
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2009, 5596 : 69 - 84
  • [37] Advances in Symbolic Probabilistic Model Checking with PRISM
    Klein, Joachim
    Baier, Christel
    Chrszon, Philipp
    Daum, Marcus
    Dubslaff, Clemens
    Klueppelholz, Sascha
    Maercker, Steffen
    Mueller, David
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016), 2016, 9636 : 349 - 366
  • [38] Symbolic Model Checking for Factored Probabilistic Models
    Deininger, David
    Dimitrova, Rayna
    Majumdar, Rupak
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 : 444 - 460
  • [39] Symbolic model checking for probabilistic timed automata
    Kwiatkowska, Marta
    Norman, Gethin
    Sproston, Jeremy
    Wang, Fuzhi
    INFORMATION AND COMPUTATION, 2007, 205 (07) : 1027 - 1077
  • [40] An optimized symbolic bounded model checking engine
    Tzoref, R
    Matusevich, M
    Berger, E
    Beer, I
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 141 - 149
12345