跳到主要內容

臺灣博碩士論文加值系統

(35.172.136.29) 您好!臺灣時間:2021/08/02 05:02
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:黃仕捷
研究生(外文):Shih-Chieh Huang
論文名稱:派屈網輔助邏輯電路模型檢查技術之研究
論文名稱(外文):Study on Petri Net-aided Model Checking Techniques
指導教授:董蘭榮董蘭榮引用關係
指導教授(外文):Lan-Rong Dung
學位類別:碩士
校院名稱:國立交通大學
系所名稱:電機與控制工程系所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2007
畢業學年度:95
語文別:英文
論文頁數:67
中文關鍵詞:派屈網模型檢查
外文關鍵詞:Petri netmodel checking
相關次數:
  • 被引用被引用:0
  • 點閱點閱:107
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
隨著半導體製程的進步和電路系統設計的複雜度不斷增加,驗證這樣的系統以確保此設計正確無誤變成了一項困難的任務。要在這樣大又複雜的設計中找出問題變成了一項耗時卻又不可忽略的一個步驟。一般最常使用的驗證方法就是以模擬(simulation)的方式,設計者輸入適當的測試訊號,接著觀察輸出訊號是否正確來判斷設計的正確與否。這樣的驗證方式無法確保整個設計已經完全符合當初設計的規格沒有任何錯誤。Clarke和Allen Emerson發明了邏輯電路模型檢查(Model checking)技術,彌補了以模擬來驗證的不足之處。在這篇論文中,我們提出了一種以派屈網(Petri Net)輔助SMV model checker做邏輯電路模型檢查。利用派屈網的一些特性,加速對於運算樹狀邏輯(Computational tree logic, CTL)中的EF和EX類的特性(properties)的驗證速度。我們以C++實現了一個簡單的程式將有限狀態機(Finite state machine)轉換成派屈網並對其做驗證。在這篇論文中,我們展示了一些簡單的範例,比較PNV (Petri net verification)與SMV的驗證時間。我們下了一個結論:在部份情況下,PNV可以大幅降低驗證EF及EX所花費的時間。
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.
CHAPTER 1 INTRODUCTION 1
CHAPTER 2 BACKGROUND 4
2.1 MODEL CHECKING 4
2.2 SMV MODEL CHECKER 6
2.3 COMPUTATIONAL TREE LOGIC 7
2.4 PETRI NET 8
2.4.1 Basic Definition 8
2.4.2 Marking, State and Reachability 10
2.4.3 Matrix Equations 12
CHAPTER 3 MODEL CHECKING WITH PETRI NET 15
3.1 VERIFICATION FLOW 16
3.2 TRANSFORMATION FROM FSM INTO PETRI NET 17
3.2.1 Transformation of Places and Transitions 17
3.2.2 Transformation of Multiple Modules 22
3.3 MARKING GENERATOR 24
3.4 REACHABILITY CHECKING 26
3.4.1 Ranks are Equal to the No. of Transitions 28
3.4.2 Ranks are Less Than the No. of Transitions 30
3.4.3 Summary 33
CHAPTER 4 IMPLEMENTATION 35
4.1 INPUT CODING RULES 35
4.2 DATA STRUCTURE OF PNV 37
4.3 PROPERTY TO MARKING 40
4.4 VERIFICATION CORE 41
4.4.1 Elimination Methods 42
CHAPTER 5 EXPERIMENTAL RESULTS 47
5.1 COUNTER 47
5.2 GREATEST COMMON DIVISOR 51
5.3 AMBA 53
5.4 TRAFFIC LIGHT CONTROLLER 57
5.5 WIZARD’S REGISTRATION FLOW 59
CHAPTER 6 CONCLUSION AND FUTURE WORK 61
6.1 CONCLUSION 61
6.2 FUTURE WORK 62
REFERENCES 63
[1] James L. Peterson, PETRI NET THEORY AND THE MODELING OF SYSTEMS, Prentice-Hall, Inc. 1981
[2] Bruce Wile, john C. Goss, Wolfgang Roesner, COMPREHENSIVE FUNCTIONAL VERIFICATION THE COMPLETE INDUSTRY CYCLE, Elsevier Inc. 2005
[3] Edmund M. Clarke, Bernd-Holger Schlingloff, HANDBOOK OF AUTOMATED RESONING, Elsevier Science Publishers B.V. 2001
[4] Giovanni De Micheli, SYNTHESIS AND OPTIMIZATION OF DIGITAL CIRCUITS, McGraw-Hill, Inc. 1994
[5] Varea M., Al-Hashimi B.M., Cortes L.A., Eles P., Zebo Peng, “Symbolic model checking of dual transition Petri Nets”, Hardware/Software Codesign, CODES, pp.43 – 48, May 2002
[6] Zhenyu Chen, Conghua Zhou, Decheng Ding, “Automatic abstraction refinement for Petri nets verification”, IEEE Int. High-Level Design Validation and Test Workshop, pp.168 – 174, Dec. 2005
[7] Karlsson, D., Eles, P., Zebo Peng, “Formal verification in a component-based reuse methodology”, System Synthesis, 15th International Symposium, pp.156 – 161, 2002
[8] Weng X., Litz L., “Verification of logic control design using SIPN and model checking: methods and case study”, American Control Conference, vol.6, pp.4072 - 4076, June 2000
[9] Cortadella J., “Combining structural and symbolic methods for the verification of concurrent systems”, Application of Concurrency to System Design Int., pp. 2 – 7, March 1998
[10] Rodrigues C.L., Guerrero D.D.S., de Figueiredo J.C.A., “Model checking in object-oriented Petri nets”, IEEE Int. Systems, Man and Cybernetics, Vol 5, pp.4977 - 4982, Oct. 2004
[11] Pastor E., Cortadella J., Roig O., “Symbolic analysis of bounded Petri nets”, IEEE Trans. Computers, Vol 50, No. 5, pp.432 – 448, May 2001
[12] Wang J., Deng Y., Xu G., “Reachability analysis of real-time systems using time Petri nets”, IEEE Trans. Systems, Man and Cybernetics, Part B, Vol. 30, No. 5, pp.725 – 736, Oct. 2000
[13] Tsai J.J.P., Jennhwa Yang S., Yao-Hsiung Chang, “Timing constraint Petri nets and their application to schedulability analysis of real-time system specifications”, IEEE Trans. Software Engineering, Vol 21, No. 1, pp.32 – 49, Jan. 1995
[14] Jiang J., Azzopardi D., Holding D.J., Carpenter G.F., Sagoo J.G., “Real-time synchronisation of multiaxis high-speed machines, from SFC specification to Petri net verification”, IEEE Control Theory and Applications, Vol 143, No. 2, pp.164 – 170, March 1996
[15] Tsung-Hsi Chiang, Lan-Rong Dung, Ming-Feng Yaung, “Modeling and formal verification of dataflow graph in system-level design using Petri net”, IEEE Int. ISCAS, Vol. 6, pp.5674 - 5677, May 2005
[16] Berthomieu B., Diaz M., “Modeling and verification of time dependent systems using time Petri nets”, IEEE Trans. Software Engineering, Vol. 17, No. 3, pp.259 – 273, March 1991
[17] Castelnuovo A., Ferrarini L., Piroddi L., “An incremental Petri net approach to production sequence modeling”, IEEE Int. Automation Science and Engineering, pp.333 – 338, Aug. 2005
[18] Wang J., Deng Y., Zhou M., “Compositional time Petri nets and reduction rules”, IEEE Trans. Systems, Man and Cybernetics, Part B, Vol. 30, No. 4, pp.562 – 572, Aug. 2000
[19] Zurawski R., “Petri net models, functional abstractions, and reduction techniques: applications to the design of automated manufacturing systems”, IEEE Trans. Industrial Electronics, Vol. 52, No. 2, pp.595 – 609, April 2005
[20] Hadjidj R., Boucheneb H., “On-the-fly TCTL model checking for Time Petri Nets using state class graphs”, ACSD Int. Application of Concurrency to System Design, pp.111 – 122, June 2006
[21] Yang S.J.H., Chu W., Lin S., Lee J., “Specifying and verifying temporal behavior of high assurance systems using reachability tree logic”, IEEE Int. High-Assurance Systems Engineering Symposium, pp.150 – 156, Nov. 1998
[22] Emerson, E.A.; Namjoshi, K.S., “On model checking for non-deterministic infinite-state systems”, IEEE Sym. Logic in Computer Science, pp.70 – 80, June 1998
[23] NuSMV source code, http://nusmv.irst.itc.it/
[24] SMV source code and execution file, Model Checking Group in Specification and Verification Center at CMU, http://www.cs.cmu.edu/~modelcheck/smv.html
[25] Cadence SMV model checker, Cadence Berkeley Labs, http://www.kenmcmil.com/smv.html
[26] J. R. Burch, E. M. Clarke, D. E. Long, “Symbolic model checking with partitioned transition relations”, In VLSI 91, Edinburgh, Scotland, 1990.
[27] J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential circuit verification using symbolic model checking”, In 27th ACM/IEEE Design Automation Conference, 1990.
[28] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang, “Symbolic model checking: 10E20 states and beyond”, In LICS, 1990.
[29] K. L. McMillan, “Symbolic model checking - an approach to the state explosion problem” PhD thesis, SCS, Carnegie Mellon University, 1992.
[30] E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, L. A. Ness, “Verification of the Futurebus+ cache coherence protocol”, In L. Claesen, Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications. North-Holland, April 1993.
[31] E. M. Clarke, O. Grumberg, D. E. Long, “Model checking and abstract”, ACM Symposium on Principles of Programming Languages, January 1992.
[32] E. M. Clarke, E. A. Emerson and A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications”, In ACM Trans. on Programming Languages and Systems, 8(2):244--263, 1986.
[33] Getting start with SMV tutorial, K. L. McMillan, Cadence Berkeley Labs 2001, http://www.cs.indiana.edu/classes/p515/readings/smv/CadenceSMV-docs/smv/tutorial/tutorial.html
[34] Steven J. Leon, LINEAR ALGEBRA WITH APPLICATIONS, Prentice Hall, 2002
[35] William Ford, William Topp, DATA STRUCTURES with C++ using STL, Prentice Hall, 2002
[36] E. M. Clarke and E. A. Emerson, Synthesis of synchronization skeletons for branching time temporal logic, In Logic of Programs: Workshop, Yorktown Heights, NT, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1981
[37] E. A. Emerson and J. Y. Halpern, “Sometimes” and “Not Never” revisited: On branching time versus linear time, Journal of the ACM, 33:151-178, 1986
[38] 洪維恩, C++教學手冊(第二版), 博碩文化, April 2006
[39] 洪錦魁, 精通C語言, 文魁資訊股份有限公司, March 2002
[40] Advanced Microcontroller Bus Architecture Specification
[41] Bloem R., Ravi K., Somenz F., “Symbolic guided search for CTL model checking”, Design Automation Conference, pp.:29 – 34, June 2000
[42] ARM Powered Training documentation
[43] .NET Framework Developer Center, ASP.NET Technical Articles, Finite State Machines, Wizards, and the Web http://msdn2.microsoft.com/en-us/library/aa478972.aspx
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top