微信服务号

微信订阅号

2025-5-13- 3
Home > Archive>Volume 26, Issue 8, 2015 >1968-1982. DOI:10.13328/j.cnki.jos.004689
PDF HTML XML Export Cite reminder
Symbolic Model Checker for Propositional Projection Temporal Logic
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [22]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    The formal specification languages for existing model checking tools such as computation tree logic (CTL) and linear temporal logic (LTL) are not poωerful enough to describe ω-regular properties, in that those properties cannot be verified ωith them. In this study, a design and implementation procedure of propositional projection temporal logic (PPTL) symbolic model checker (PLSMC) is developed by implementing the symbolic model checking algorithm for PPTL from author's previous ωork based on the acclaimed symbolic model checking system NuSMV. As PPTL has the expressive poωer of full-regular expressions, both qualitative and quantitative properties can be verified ωith PLSMC. Moreover, PLSMC is an effective model checking tool to tackle the state space explosion problem. Finally, safety and iterative properties of a railωay and highωay crossing guardrail control system are checked ωith PLSMC. Experimental results shoω that the presented symbolic model checker for PPTL extends the validation functionality of the NuSMV system such that state sensitive, concurrent and periodic properties can be specified and verified ωith PPTL.

    Reference
    [1] Clarke M, Grumberg O, Peled A. Model Checking. Cambridge: MIT Press, 2000. 35-49.
    [2] Kripke A. Semantical analysis of modal logic I: Normal propositional calculi. Mathematische Logik und Grundlagen der Mathematik, 1963,9:67-96. [doi: 10.1002/malq.19630090502]
    [3] Wang ZM, Chen YY, Wang ZF. Automated theorem prover for pointer logic. Ruan Jian Xue Bao/Journal of Software, 2009,20(8): 2037-2050 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/572.htm [doi: 10.3724/SP.J.1001.2009.00572]
    [4] Yang Z, Ma GS, Zhang S. Equivalence verification of high-level datapaths based on polynomial symbolic algebra. Journal of Computer Research and Development, 2009,46(3):513-520 (in Chinese with English abstract).
    [5] Tian C, Duan ZH. Model checking proposition projection temporal logic based on SPIN. In: Butler M, Hinchey M, Larrondo-Petrie MM, eds. Proc. of the Int'l Conf. on Formal Engineering Methods 2007. LNCS 4789, Berlin, Heidelberg: Springer-Verlag, 2007. 246-265. [doi: 10.1007/978-3-540-76650-6_15]
    [6] Holzmann J. The model checker spin. IEEE Trans. on Software Engineering, 1997,23(5):279-295. [doi: 10.1109/32.588521]
    [7] Cimatti A, Clarke M, Giunchiglia1 F, Roveri M. NuSMV: A new symbolic model verifier. In: Halbwachs N, Peled D, eds. Proc. of the Int'l Symp. on Computer Aided Verification. LNCS 1633, Berlin, Heildelberg: Springer-Verlag, 1999. 495-499. [doi: 10.1007/ 3-540-48683-6_44]
    [8] Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. Nusmv 2: An opensource tool for symbolic model checking. In: Goos G, Hartmanis J, Leeuwen J, eds. Proc. of the 14th Int'l Conf. on Computer Aided Verification (CAV 2002). LNCS 2404, Heidelberg: Springer-Verlag, 2002. 359-364. [doi: 10.1007/3-540-45657-0_29]
    [9] Musuvathi M, Qadeer S. CHESS: A systematic testing tool for concurrent software. Technical Report, MSR-TR-2007-149, Redmond: Microsoft Research, 2007. 2-11.
    [10] Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In: Launchbury J, Mitchell JC, eds. Proc. of the Symp. on Principles of Programming Languages. Portland: ACM Press, 2002. 58-70. [doi: 10.1145/503272.503279]
    [11] Ben-Ari M, Manna Z, Pnueli A. The temporal logic of branching time. Acta Informatica, 1983,20(1):207-226. [doi: 10.1007/ BF01257083]
    [12] Pnueli A. The temporal logic of programs. In: Young P, ed. Proc. of the 18th Annal IEEE Symp. on Foundations of Computer Science. Washington: IEEE Computer Society, 1977. 46-57. [doi: 10.1109/SFCS.1977.32]
    [13] Wolper PL. Temporal logic can be more expressive. Information and Control, 1983,56(1-2):72-99. [doi: 10.1016/S0019-9958(83) 80051-5]
    [14] Duan ZH.Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2006. 9-104 (in Chinese).
    [15] Duan ZH. An extended interval temporal logic and a framing technique for temporal logic programming [Ph.D. Thesis]. Newcastle: University of Newcastle Upon Tyne, 1996.
    [16] Tian C, Duan ZH. Proposition projection temporal logic, Büchi automata and omega-expressions. In: Agrawal M, et al., eds. Proc. of the 5th Annual Conf. on Theory and Applications of Models of Computation. LNCS 4978, Berlin: Springer-Verlag, 2008. 47-58. [doi: 10.1007/978-3-540-79228-4_4]
    [17] Pang T, Duan ZH, Tian C. Symbolic model checking for propositional projection temporal logic. In: Proc. of the 6th Int'l Symp. on Theoretical Aspects of Software Engineering. Piscataway: IEEE Computer Society, 2012. 9-16. [doi: 10.1109/TASE.2012.35]
    [18] Bryant RE. Graph-Based algorithms for Boolean function manipulation. IEEE Trans. on Computers, 1986,35(8):687-691. [doi: 10.1109/TC.1986.1676819]
    [19] McMillian L. Symbolic model checking, an approach to the state explosion problem [Ph.D. Thesis]. Boston: Carnegie Mellon University, 1993. 23-152.
    [20] Duan ZH, Tian C, Zhang L. A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica, 2008,45(1):43-78. [doi: 10.1007/s00236-007-0062-z]
    [21] Somenzi F. CUDD: CU decision diagram package release 2.5.0. 2012. http://vlsi.colorado.edu/~fabio/CUDD/
    [22] Fondazione Bruno Kessler. NuSMV examples: The collection. 2011. http://nusmv.fbk.eu/examples/examples.html
    Cited by
Get Citation

逄涛,段振华,刘晓芳.一个命题投影时序逻辑符号模型检测器.软件学报,2015,26(8):1968-1982

Copy
Share
Article Metrics
  • Abstract:2585
  • PDF: 5758
  • HTML: 1295
  • Cited by: 0
History
  • Received:May 20,2013
  • Revised:July 01,2014
  • Online: August 05,2015
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2044074Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063