(Division of Computer Science Xi’an Research Institution of Hi-Technology Xi’an, China, 710025)
Abstract—SAT-based bounded model checking (BMC) is introduced as an important complementary technique to OBDD-based symbolic model checking, and is an efficient verification method for parallel and reactive systems. However, until now the properties verified by bounded model checking are very finite. Temporal logic PSL is a property specification language (IEEE-1850) describing parallel systems and is divided into two parts, i.e. the linear time logic FL and the branch time logic OBE. In this paper, the specification checked by BMC is extended to PSL and its algorithm is also proposed. Firstly, define the bounded semantics of PSL, and then reduce the bounded semantics into SAT by translating PSL specification formula and the state transition relation of the system to the propositional formula A and B, respectively. Finally, verify the satisfiability of the conjunction propositional formula of A and B. The algorithm results in the translation of the existential model checking of the temporal logic PSL into the satisfiability problem of propositional formula. An example of a queue controlling circuit is used to interpret detailedly the executing procedure of the algorithm.
Keywords-PSL(property specification language); BMC(bounded model checking); SAT(propositional satisfiability)
References
Formal semantics of Accellera property specification language (Appendix B),http://www.eda.org/vfv/docs/PSL-v1.1.pdf
Accellea. Property specification language referencemanual,http://www.haifa.il.ibm.com/projects/verification/sugar
Beer I，Ben-David S, Eisner C, Fisman D, Gringauze A, Rodeh Y: The temporal logic Sugar.In:Conference on Computer Aided Verification (CAV).LNCS,vol.2102, pp.363-367,Springer(2001)
Clarke EM,Grumber O,Peled DA: Model Checking. MIT Press,Cambridge(2000)
Ben-Ari M,Manna A,Pnueli:The temporal logic of branching time. Acta Information.20, 207-226 (1983)
Automata construction for PSL,http://www.wisdom.weizmann.ac.il/~dana/publicat/automata_constructionTR.pdf
S.Ben-David, R.Bloem, D. Fisman, A.Griesmayer, I.Pill.S.Ruah:Automata ConstructionAlgorithms Optimized for PSL.Technical Report,(2005)
K.Heljanko,T.Junttila,M.Kein nen,M.Lange, T.Latvala: Bounded Model Checking for WeakAlternating Büchi Automata. In: CAV’06.LNCS, vol.4144,pp. 96-108,Springer, Seattle(2006)
A.Cimatti, M.Roveri, S.Semprini, S.Tonetta: From PSL to NBA: a Modular Symbolic Encoding.In: FMCAD’06(2006)
Biere A,Cimatti A,Clarke E M,Zhu Y:Symbolic model checking without BDDs. In: Tool andAlgorithms for the Analysis and Construction of Systems(TACAS’99).LNCS, vol.1597,pp. 193-207,Springer(1999)
Latvala T,Biere A,Heljanko K,Junttila T.Simple is better: Efficient Bounded Model Checkingfor Past LTL.In:VMCAI’2005.LNCS,vol.3385,pp. 380-395,Springer(2005)
Penczek W,Wozna B,Zbrzezny A:Bounded Model Checking for the Universal Fragment ofCTL. Fundamental Informaticae 51, 135-156(2002)
Wozna B:ACTL* properties and bounded model checking. Fundamental Informaticae.62, 1-23(2004)
LUO X.Y., SU K.L.,YANG J.J.:Bounded Model Checking for Temporal Epistemic Logic inSynchronous Muti-Agent Systems. Journal of Software.17, 2485-2498(2006)
Zhi-Hong Tao,Cong-Hua Zhou，Zhong Chen，Li-Fu Wang: Bounded Model Checking ofCTL*. Journal of Comput. Sci.& Technol.22, 39-43 (2007)
Wenhui Zhang. Verification of ACTL Properties by Bounded ModelChecking.In:EUROCAST’2007.LNCS,vol.4739,pp. 556-563,Springer(2007)
Latvala T,Biere A,Heljanko K,Junttila T: Simple Bounded LTL ModelChecking.In:FMCAD’2004.LNCS,vol.3312,pp. 186-200,Springer(2004)
第一作者簡介：
虞蕾（1978—）女，浙江浦江人，講師，博士后，主要研究方向為模型檢驗和航跡規劃。
YU Lei: female, was born in Pu Jiang county in Zhe Jiang province in 1978. She is now a university lecturer and a postdoctor, and her main research fields include model checking and route planning.
