loading...
Model Checking with Induction
Chicago, Illinois September 17-September 21
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/COMPSAC.2006.6030th Annual International Computer So ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Kuangnan Chang, Eastern Kentucky University, USA
David Kung, The University of Texas at Arlington, USA
We have proposed Inductive Model Checking (IMC) to alleviate the state explosion problem in model checking. IMC divides the whole verification tasks into several subtasks, and applies the three inductive steps (basis, hypothesis, and induction) to verify a system with model checking. In this paper, we continue our research by determining those temporal formulas, namely, persistent temporal formulas, which are verifiable with IMC. One important characteristic of a persistent temporal formula is that it contains a periodic temporal formula that must be held persistently. From the verification results of the periodic formula with different sequences of states, IMC concludes the verification of the persistent temporal formula.
Citation:
Kuangnan Chang, David Kung, "Model Checking with Induction," compsac, vol. 1, pp.143-149, 30th Annual International Computer Software and Applications Conference (COMPSAC'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.