Study on Petri Net-aided Model Checking Techniques

• Main Authors: Shih-Chieh Huang, 黃仕捷
• Other Authors: Lan-Rong Dung
• Format: Others
• Language: en_US
• Published: 2007
• Online Access: http://ndltd.ncl.edu.tw/handle/72134387198553549660

碩士 === 國立交通大學 === 電機與控制工程系所 === 95 === With the progress of semiconductor manufacturing techniques and the increasing of complexity of designs, to ensure the correctness of a design becomes a hard mission. To find out the bugs in a large and complex design is time consuming but significant works. The general verification method used by designers is simulation. The designers input appropriate signals to the design and observe if the outputs are correct to judge the correctness of the design. This verification method can not ensure that the design is completely conform to the specification. Clarke and Allen Emerson invented model checking techniques to recover the insufficiency of simulation based verification. In this paper, we propose a Petri net-aided model checking techniques to assist SMV model checker. In some cases, this technique can speed up the verification of EF and EX properties. We implement a simple program with C++ language to transfer a FSM (finite state machine) into a Petri net and verify the state machine. Then we show some examples to compare the verification time of PNV and SMV. Finally we make a conclusion that in some cases, PNV can reduce the verification time of EF and EX properties substantially.