|
|
|
symbolic model checking APSL |
Wanwei LIU( ), Ji WANG(), Huowang CHEN, Xiaodong MA, Zhaofei WANG |
| National Laboratory for Parallel and Distributed Processing, School of Computer, National University of Defense Technology, Changsha 410073, China |
|
|
|
|
Abstract Property specification language (PSL) is a specification language which has been accepted as an industrial standard. In PSL, SEREs are used as additional formula constructs. In this paper, we present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. Then, we extend the LTL symbolic model checking algorithm to that of APSL, and then present a tableau based APSL verification technique, which can be easily implemented via the BDD based symbolic approach. Moreover, we implement an extension of NuSMV, and this adapted version supports symbolic model checking of APSL. Experimental results show that this variant of PSL can be efficiently verified. Henceforth, symbolic model checking PSL can be carried out by a transformation from PSL to APSL and symbolic model checking APSL.
|
| Keywords
property specification language
symbolic model checking
tableau approach
extended NuSMV
|
|
Corresponding Author(s):
LIU Wanwei,Email:{wwliu,wj}@nudt.edu.cn; WANG Ji,Email:{wwliu,wj}@nudt.edu.cn
|
|
Issue Date: 05 March 2009
|
|
| 1 |
Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers , 1986, C-35(8): 677-691
doi: 10.1109/TC.1986.1676819
|
| 2 |
McMillan K L. Symbolic Model Checking, An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, Kluwer Academic Publishers , 1993
|
| 3 |
Accellera. Accellera property languages reference manual. http: //www.eda.org/vfv/docs/PSL-v1.1.pdf, 2004
|
| 4 |
Bloem R, Galler S, Jobstmann B, . Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science , 2007, 190(4): 3-16
doi: 10.1016/j.entcs.2007.09.004
|
| 5 |
Boule M, Zilic Z. Efficient automata-based assersion-checker Synthesis of SEREs for hardware emulation. In: Proceedings of 12th Conference on Asia South Pacific Design Automation. IEEE , 2007
|
| 6 |
Vardi M Y. Branching vs. linear time: Final showdown. In: Proceeding of International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Berlin: Springer, 2001, LNCS, 2031: 1-22
|
| 7 |
Bustan D, Fisman D, Havlicek J. Automata construction for PSL. Technical Report MCS05-04, IBM Haifa Research Lab , 2005
|
| 8 |
Ruah S, Fisman D, Ben-David S. Automata construction for on-the-fly model checking PSL safety simple subset. Technical Report H0234, IBM Haifa Research Lab , 2005
|
| 9 |
Jin N, Shen C. Dynamic verifying the properties of the simple subset of PSL. In: Proceedings of 1st IEEE Symposium of Theoretical Aspects on Software Engineering , 2007, 173-182
|
| 10 |
Clarke EM, Grumberg O, Hamaguchi K. Another Look at LTLModel Checking. In: Proceedings of the 6th Conference on Computer Aided verification . Berlin: Springer-Verlag, 1994, LNCS, 818: 415-427
|
| 11 |
Cimatti A, Clarke E, Giunchiglia F, . NuSMV: A New Symbolic Model Verifier. In: Proceedings of the 11th Conference on Computer Aided Verification . Berlin: Springer, 1999, LNCS, 1633: 495-499
|
| 12 |
Pnueli A, Zaks A. PSL model checking and runtime verification via testers. In: Misra J, Nipkow T, Sekerinski E, eds. Proceedings of the 14th International Symposium on Formal Methods . Berlin: Springer-Verlag, 2006, LNCS, 4085: 573-586
|
| 13 |
Martin A J. The design of a self-timed circuit for distributed mutual exclusion. In: Fuchs H, ed. Proceedings of the 1985 Chapel Hill Conference on Very Large Scale Integration , 1985.
|
| 14 |
Wolper P. Temporal logic can be more expressive. Information and Control , 1983, 56(1-2): 72-99
doi: 10.1016/S0019-9958(83)80051-5
|
| 15 |
Vardi M Y, Wolper P. Reasoning about Infinite Computations. Information and Computation , 1994, 115(1): 1-37
doi: 10.1006/inco.1994.1092
|
| 16 |
Armoni R, Fix L, Flaisher A, . The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In: Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Berlin: Springer, 2002, LNCS, 2280: 296-311
|
| 17 |
Beer I, Ben-David S, Eisner C, . RuleBase: an industry-oriented formal verification tool. In: Proceedings of 33rd Design Automation Conference , ACM Press, 1996, 655-660
|
| 18 |
Ben-David S, Embedding Finite Automata within Regular Expressions. Theoretical Computer Science , 2008, 404: 202-218
doi: 10.1016/j.tcs.2008.03.011
|
| 19 |
Tuerk T, Schneider K, Gordon M. Haifa Verification Conference. In: Proceedings of Haifa Verification Conference . Berlin: Springer, 2007, LNCS, 4383: 1-15
|
| 20 |
Liu W, Wang J, Chen H, . Symbolic model checking apsl. In: Davies J, Li X, ed. Proceedings of Second IEEE International Symposium on Theoretical Aspects of Software Engineering , 2008, 39-46
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
