跳到主要內容

臺灣博碩士論文加值系統

(18.97.9.169) 您好!臺灣時間:2025/02/16 07:55
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:邱彥凱
研究生(外文):Yen-Kai Chiu
論文名稱:正規模型的最佳化:以Wifidog進行實驗
論文名稱(外文):Optimization of Formal Model : An Experiment with Wifidog
指導教授:王凡
指導教授(外文):Farn Wang
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:電機工程學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2005
畢業學年度:93
語文別:英文
論文頁數:58
中文關鍵詞:驗證模型檢驗
外文關鍵詞:verificationmodel checking
相關次數:
  • 被引用被引用:0
  • 點閱點閱:400
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
隨著程式變得越來越複雜,對於程式設計師來說,除錯也越來越困難,因此我們需要一個更有效率的驗證方法。模型檢驗由於可以自動化的方式完成,算是較好的方法。然而此方法亦會受狀態空間爆炸所限制。這項問題可能是由於自動化的過程中,產生了許多多餘的狀態空間。此外,大多數的敘述句可以在單一轉換中完成。我們將展示使用一些技巧來縮減這些狀態。我們將此方法實作於一個將C翻譯成RED此種正規描述的程式上。
While the programs become larger and larger, the task of debugging is very difficult for programmer. We want a more efficient way of verification. Model checking is a better choice because it can be done automatically. However, state space explosion limits the applicability of it. This problem may result from the process of translation, which generate some redundant states. On the other hand, most of the expressions are able to be merged to a transition. We show the consequence that using some techniques to reduce state spaces. We will present our implementation of aprogram that translates from C programs to the formal description of RED
1 Introduction 1
1.1 Motivation . . . 1
1.2 Model checking . . . 2
1.3 Wifdog . . . 3
2 RED 5
2.1 Defnition of CTRS . . . 5
2.2 RED input file structure . . . 8
2.3 Modelling CSMA/CD protocol . . .13
3 Implementation 16
3.1 Parsing tree . . . 17
3.2 Data structure which used in parsing tree . . . 17
3.3 Recursion detection . . . 19
3.4 Redundant state . . . 22
3.5 The algorithm of optimization . . . 24
3.6 Optimization . . . 28
4 Experiment 29
4.1 Wifdog . . . 29
4.2 Translation and Optimization . . . 30
5 Conclusions and future works 33
A The grammar rules of C programming language 35
Bibliography 47
[1] John R. Levine, Tony Mason, Doug Brown. Lex & yacc 2/e, 1992
[2] R. Alur, D.L. Dill. Automata for modelling real-time systems. ICALP'' 1990, LNCS 443, Springer-Verlag, pp.322-335.
[3] R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems. IEEE LICS, 1990.
[4] C. Colby, P. Godefroid, L.J. Jagadeesan. Automatically Closing Open Reactive Programs. in Proceedings of ACM SIGPLAN Conference on Programming Lan-guage Design and Implementation, 1998.
[5] A. Engels, L. Feijs, S. Mauw. Test Generation for Intelligent Networks using Model Checking. TACAS''97, Enschede, the Netherlands. in LNCS 1217. Springer-Verlag.
[6] E.A. Emerson, C.-L. Lei. Modalities for Model Checking: Branching Time Logic Strikes Back, Science of Computer Programming 8 (1987), pp.275-306, Elsevier
Science Publishers B.V. (North-Holland).
[7] E.M. Clarke, O. Grumberg, D.A. Peled Model Checking. MIT Press, 2000, ISBN 0-262-03270-8.
[8] D Minoli Hotspot Networks: Wi-Fi for Public Access Locations McGraw-Hill,2003, ISBN 0071409785.
[9] R. Alur, D.L. Dill. Automata for modelling real-time systems. ICALP'' 1990, LNCS 443, Springer-Verlag, pp.322-335.ISBN:0071409785
[10] N. Sidorova, M. Ste®en. Embedding Chaos. In Proceedings of 8th International Static Analysis Symposium, SAS 2001, Paris, France, 2001.
[11] http://www.ilesansfl.org/wiki/WiFiDog
[12] http://www.jiwire.com/
[13] F. Wang. E±cient Data-Structure for Fully Symbolic Verifcation of Real- Time Software Systems. TACAS''2000, March, Berlin, Germany. in LNCS 1785, Springer-Verlag.
[14] F. Wang. Symbolic Veri‾cation of Complex Real-Time Systems with Clock-Restriction Diagram. FORTE''2001, Kluwer; August 2001, Cheju Island, Korea.
[15] F. Wang. Efficient Verifcation of Timed Automata with BDD-like Data-Structures. special issue of STTT (Software Tools for Technology Transfer), Springer-Verlag for VMCAI''2003
[16] F. Wang. E±cient Veri‾cation of Timed Automata with BDD-like Data-Structures, STTT (Jouranl of Software Tools for Technology Transfer), Vol. 6, Nr. 1, June 2004, Springer-Verlag; Special issue for VMCAI''2003, LNCS 2575, Springer-Verlag.
[17] F. Wang. Symbolic Parametric Analysis of Linear Hybrid Systems with BDD-like Data-Structures. IEEE Transactions on Software Engineering, January 2005 (Vol.31, No. 1), p.38-51. A preliminary version of the paper also appears in proceedings of CAV 2004, LNCS 3114, Springer-Verlag.
[18] F. Wang, G.-D. Huang, F. Yu. TCTL Inevitability Analysis of Dense-Time Systems, in proceedings of the 8th International Conference on Implementation and Application of Automata (CIAA), LNCS 2759, Springer-Verlag, July 2003, Santa Barbara, CA, USA.
[19] S. Yovine. Kronos: A Verifcation Tool for Real-Time Systems. International Jour-nal of Software Tools for Technology Transfer, Vol. 1, Nr. 1/2, October 1997.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top