跳到主要內容

臺灣博碩士論文加值系統

(44.213.63.130) 您好!臺灣時間:2023/02/03 14:20
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:邱冠綸
研究生(外文):Kuan-lun Chiu
論文名稱:一個適用於模型檢驗上有效率的涵輔v評估方法
論文名稱(外文):An Efficient Coverage Estimation Methodology for Model Checking
指導教授:熊博安熊博安引用關係
指導教授(外文):Pao-Ann Hsiung
學位類別:碩士
校院名稱:國立中正大學
系所名稱:資訊工程所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
畢業學年度:93
語文別:英文
論文頁數:52
中文關鍵詞:模型檢驗涵輔v評估真時自動機有時間性的分時邏輯特性
外文關鍵詞:Timed AutomataTCTL PropertiesCoverage EstimationModel Checking
相關次數:
  • 被引用被引用:0
  • 點閱點閱:139
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
先前所提出的適用於模型檢驗上的涵輔v評估方法使用了六個變異模型來幫助評估其涵輔v。不過當一個系統模型變得複雜且龐大時,它便需要耗費相當長的時間來完成涵輔v的評估,例如一個建築物門禁系統便需要10個小時以上的評估時間。然而如此長的評估時間在此流程中是不容易被接受的。因為在整個流程中,當我們發覺系統規格對於系統模型的涵輔v太低時,便需要對規格或模型做改進,進而重新評估涵輔v,重覆直到涵輔v達到我們的標準為止。
而在涵輔v評估的過程中,模型檢驗是時間耗費上一個相當大的瓶頸。因此我們提出了一個更有效率的涵輔v評估方法,利用一重新貼標籤決策表來幫助我們在模型檢驗過程中,如果變異模型的應用可能會使變異的系統模型不滿足原本的系統規格,則需要重新貼標籤,意即重新檢查變異的系統模型是否滿足某些系統規格,若否,則不需要重新貼標籤,藉此來縮短檢驗時間。
A previously proposed coverage estimation methodology for model checking uses six mutation models to estimate the coverage, but it requires a lot of time to evaluate the result when a system model becomes complex and large. For example, it takes more than 10 hours to estimate the coverage of a system model like a simple AMBA architecture or an entrance guard system that describes a guard system for controlling the entrance of a building. However, such a lengthy estimation time is not acceptable by the designers in the verification flow. After coverage estimation we may find that our system model is not covered very well by the specifications, so we might need to refine the system model or the speci¯cations and estimate again until we get a good coverage value (above 90% or more). The main bottleneck in coverage estimation is the large amount of time spent in repeated model checking. Hence in this work, we propose an approach to evaluate the coverage estimation for the verification of a system design more efficiently. We propose a re-labelling decision table to record if a state still satisfies a property after a mutation is applied to a system model. Referring to the decision table, we can decrease the coverage estimation time by as much as 25%. This is possible because we avoid the actions of clearing previously marked labels and of redoing the labelling for the property-mutation combination in the decision table that states the property is still satisfied after mutation. We use some real cases to show that we can save the estimation time because of some properties that do not need to be checked again.
1 Introduction 5
1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
1.2 Proposed Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.3 Thesis Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2 Related Work 12
3 The System Model and Speci¯cation 17
3.1 System Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2 Speci¯cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
3.3 Mutation Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
4 The E®ective Coverage Estimation Methodology 25
4.1 Re-labelling Decision Table . . . . . . . . . . . . . . . . . . . . . . . . 26
4.2 Proof of the Re-labelling Decision Table . . . . . . . . . . . . . . . . 28
4.3 Counter Examples of the Re-labelling Decision Table . . . . . . . . . 31
4.4 Program Flow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5 Experimental Results 46
6 Conclusions and Future Work 49
[1] Accellera OVL Technical Committee. http://www.eda.org/ovl/.
[2] AMBA 2.0 Speci¯cation. http://www.arm.com/products/solutions/AMBA_Spec.html.
[3] The Accellera Formal Verification Technical Committee (FVTC). http://www.eda.org/vfv/.
[4] R. Alur and D. L. Dill. A theory of timed automata. In Proceedings of the International Conference on Theoretical Computer Science, 126:183-235, 1994.
[5] H. Chockler, O. Kupferman, R. P. Kurshan, and Vardi. M. Y. A Practical Approach to Coverage in Model Checking. In Proceedings of the International Conference on Computer Aided Verification (CAV'01), Lecture Notes in Computer Science 2102, pages 66-78. Springer-Verlag, July 2001.
[6] H. Chockler, O. Kupferman, and M. Y. Vardi. Coverage Metrics for Temporal Logic Model Checking. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 2031, pages 528-542. Springer-Verlag, April 2001.
[7] H. Chockler, O. Kupferman, and M. Y. Vardi. Coverage Metrics for Formal Verification. In Proceedings of the International Conference on Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 2860, pages 111-125. Springer-Verlag, October 2003.
[8] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. In Proceedings of ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244-263, April 1986.
[9] E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.
[10] F. Fummi, G. Pravadelli, A. Fedeli, U. Rossi, and F. Toto. On the Use of a High-Level Fault Model to Check Properties Incompleteness. In Proceedings of the First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE'03), pages 145-152. IEEE Computer Society, June 2003.
[11] T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-Time Systems. In Proceedings of the IEEE International Conference on Logics in Computer Science (LICS'92), pages 394-406, June 1992.
[12] Y. Hoskote, T. Kam, P.-H. Ho, and X. Zhao. Coverage Estimation for Symbolic Model Checking. In Proceedings of the International Design Automation Conference, pages 300-305, June 1999.
[13] P.-A. Hsiung and F. Wang. A State Graph Manipulator Tool for Real-Time System Specification and Veri¯cation. In Proceedings of 4th International Conference on Real-Time Computing Systems and Applications (RTCSA'98), pages 181-188, October 1998.
[14] N. Jayakumar, M. Purandare, and F. Somenzi. Dos and don'ts of CTL state coverage estimation. In Proceedings of the International Conference on Design Automation Conference (DAC'03), pages 292-295. ACM, June 2003.
[15] T.-C. Lee. Mutation Coverage Estimation for Symbolic Model Checking. Master's Thesis, Dept. of Computer Science & Information Engineering, National Chung Cheng University, July 2004.
[16] T.-C. Lee and P.-A. Hsiung. Mutation Coverage Estimation for Model Checking. In Proceedings of the International Conference on Automated Technology for Verification and Analysis (ATVA'04), pages 354-368. Springer-Verlag, October 2004.
[17] F. Wang, Hwang G.-D., and Yu F. Numerical Coverage Estimation for the Symbolic Simulation of Real-Time Systems. In Proceedings of the International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'03), pages 160-176. Springer-Verlag, September 2003.
[18] M. R. Woodward. Mutation Testing - an Evolving Technique. In Proceedings of IEE Colloquium on Software Testing for Critical Systems, pages 3/1-3/6, June 1990.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top