Study on Petri Net-aided Model Checking Techniques
碩士 === 國立交通大學 === 電機與控制工程系所 === 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....
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Others |
| Language: | en_US |
| Published: |
2007
|
| Online Access: | http://ndltd.ncl.edu.tw/handle/72134387198553549660 |
| Summary: | 碩士 === 國立交通大學 === 電機與控制工程系所 === 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.
|
|---|