A PSL Bounded Model Checking; Method
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.
PSL(property specification language) BMC(bounded model checking) SAT(propositional satisfiability)
YU Lei ZHAO Zongtao
Division of Computer Science Xi”an Research Institution of Hi-Technology Xi”an,China,710025
国内会议
北京
英文
79-90
2012-05-01（万方平台首次上网日期，不代表论文的发表时间）