Title :
SAT-based Bounded Model Checking for SE-LTL
Author :
Conghua, Zhou ; Shiguang, Ju
Author_Institution :
Jiangsu Univ., Nanjing
fDate :
July 30 2007-Aug. 1 2007
Abstract :
For concurrent software systems state/event linear temporal logic SE-LTL is a specification language with high expressive power and the ability to reason about both states and events. Until now, SE-LTL model checking algorithm is still explicit. We introduce a bounded model checking procedure for SE-LTL which reduces model checking to propositional satisfiability. This new technique avoids the space blow up of BDDs, generates counterexamples much faster, and sometimes speeds up the verification. For SE-LTL-x we further show how to integrate the procedure and stuttering equivalent technique. The experiment result shows that the integration can reduce the verification time very much.
Keywords :
concurrent engineering; formal verification; specification languages; temporal logic; BDD; SAT-based bounded model checking; SE-LTL; concurrent software systems; propositional satisfiability; specification language; state-event linear temporal logic; Artificial intelligence; Boolean functions; Computer science; Data structures; Distributed computing; Logic; Power engineering and energy; Power system modeling; Software engineering; Software systems;
Conference_Titel :
Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing, 2007. SNPD 2007. Eighth ACIS International Conference on
Conference_Location :
Qingdao
Print_ISBN :
978-0-7695-2909-7
DOI :
10.1109/SNPD.2007.242