微信服务号

微信订阅号

2025-4-9- 16
Home > Archive>Volume 20, Issue 8, 2009 >2015-2025
PDF HTML XML Export Cite reminder
Symbolic Model Checking of ETL
Author:
Affiliation:

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

    To make symbolic model checking approach applicable to all ω-regular properties, this paper studies symbolic model checking for ETL (extended temporal logic). First, the Tableau approach for LTL (linear temporal logic) is extended to that of ETL, and then the BDD (binary decision diagram)-based encodings of this technique is given. Moreover, the model checking tool ENuSMV is implemented based on NuSMV, which allows users to customize temporal connectives, and hence all ω-regular properties can be verified. Experimental results show that ETL can also be efficiently verified by the symbolic approach.

    Reference
    [1]Pnueli A. The temporal logic of programs. In: Young P, ed. Proc. of the 18th IEEE Symp. on Foundation of Computer Science. Providence: IEEE Computer Society, 1977. 46-57.
    [2]Emerson EA, Clarke EM. Characterizing correctness properties of parallel programs using fixpoints. In: Bakker JW, Leeuween J, eds. Int’l Colloquium on Automata, Languages and Programming. LNCS 85, Berlin, Heildelberg: Springer-Verlag,1980.169-181.
    [3]Vardi MY. Linear vs. branching time: A complexity-theoretic perspective. In: Pratt V, ed. Proc. of the 13th Annual IEEE Symp. of Logic in Computer Science. Indianapolis: IEEE Computer Society, 1998. 394-405.
    [4]Vardi MY. Branching vs. linear time: Final showdown. In: Margaria T, Wang Y, eds. Proc. of the 7th Int’l Conf. of Tools and Algorithms for the Construction and Analysis of Systems. LNCS 2031, Berlin, Heidelberg: Springer-Verlag, 2001. 1-22.
    [5]Nain S, Vardi MY. Branching vs. linear time: Semantical perspective. In: Namjoshi KS, Yoneda T, Higashino T, Okamura Y, eds. Int’l Symp. on Automated Technology on Verification and Analysis. LNCS 4762, Berlin, Heidelberg: Springer-Verlag, 2007. 19-34.
    [6]McMillian KL. Symbolic model checking, an approach to the state explosion problem [Ph.D. Thesis]. Boston: Carnegie Mellon University, 1993.
    [7]Clarke EM, Grumberg O, Hamaguchi K. Another look at LTL model checking. In: Dill D, ed. Proc. of the 6th Int’l Conf. on Computer-Aided Verification. LNCS 818, Berlin, Heidelberg: Springer-Verlag, 1994. 415-427.
    [8]Cimatti A, Clarke EM, Giunchiglia1 F, Roveri M. NuSMV: A new symbolic model verifier. In: Halbwachs N, Peled D, eds. Int’l Symp. on Computer Aided Verification. LNCS 1633, Berlin, Heildelberg: Springer-Verlag, 1999. 495-499.
    [9]Wolper P. Temporal logic can be more expressive. Information and Control, 1983,56(1-2):72-99.
    [10]Lichtenstein S, Pnueli A, Zuck L. The glory of past. In: Parikh R, ed. Workshop on Logic of Programs. LNCS 193, Berlin, Heildelberg: Springer-Verlag, 1985. 196-218.
    [11]Accellera. Accellera property languages reference manual. 2004. http://www.eda.org/vfv/docs/PSL-v1.1.pdf
    [12]Armoni R, Fix L, Flaisher A, Gerth R, Ginsburg B, Kanza T, Landver A, Mador-Haim S, Singerman E, Tiemeyer A, Vardi MY, Zbar Y. The ForSpec temporal logic: A new temporal property-specification language. In: Katoen JP, Stevens P, eds. Proc. of the 8th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 2280, Berlin, Heidelberg: Springer-Verlag, 2002. 296-311.
    [13]Vardi MY, Wolper P. Reasoning about infinite computations. Information and Computation, 1994,115(1):1-37.
    [14]Piterman N. Extending temporal logic with ?-automata [MS. Thesis]. Rehovot: School of the Weizmann Institute of Science, 2000.
    [15]Kupferman O, Piterman N, Vardi MY. Extended temporal logic revisit. In: Larsen KG, Nielsen M, eds. Proc. of the 12th Int’l Conf. on Concurrency Theory. LNCS 2154, Berlin, Heidelberg: Springer-Verlag, 2001. 519-535.
    [16]Su KL, Luo XY, Lu GF. Symbolic model checking of CTL*. Chinese Journal of Computers, 2005,28(11):1798-1806 (in Chinese with English abstract).
    [17]Bloem R, Galler S, Jobstmann B, Piterman N, Pnueli A, Weiglhofer M. Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science, 2007,190(4):3-16.
    [18]Boule M, Zilic Z. Efficient automata-based assertion-checker synthesis of SEREs for hardware emulation. In: Onodera H, Matsunaga Y, eds. Proc. of the 12th Conf. on Asia South Pacific Design Automation. Yokohama: IEEE Society, 2007. 324-329.
    [19]Jin NY, Shen CJ. Dynamic verifying the properties of the simple subset of PSL. In: Zhu HB, ed. IEEE Symp. of Theoretical Aspects on Software Engineering. Shanghai: IEEE Society, 2007. 173-182.
    [20]Cavada R, Cimatti A, Jochim CA, Keighren G, Olivetti E, Pistore M, Roveri M, Tchaltsev A. NuSMV 2.4 User Manual. 2007. http://nusmv.fbk.eu/NuSMV/userman/v24/nusmv.pdf
    [21]Guttman J, Herzog A, Ramsdell J. Slat: Information flow analysis of security enhanced Linux. 2005. http://www.nsa.gov/SELinux
    [22]Liu WW, Wang J, Dong W, Chen HW. Axiomatizing extended temporal logic fragments via instantiation. In: Jones CB, Liu ZM, Woodcock J, eds. Int’l Colloquium on Theoretical Aspects of Computing. LNCS 4711, Berlin, Heidelberg: Springer-Verlag, 2007. 322-336.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

刘万伟,王戟,王昭飞. ETL的符号化模型检验.软件学报,2009,20(8):2015-2025

Copy
Share
Article Metrics
  • Abstract:5789
  • PDF: 7337
  • HTML: 0
  • Cited by: 0
History
  • Revised:August 11,2008
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034140Visitors
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