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

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:葉家蓁
研究生(外文):Jia-jen Yeh
論文名稱:一個適用於模型檢驗上有效率的涵輔v評估方法
論文名稱(外文):An Efficient Coverage Estimation Methodology for Model Checking
指導教授:熊博安熊博安引用關係
指導教授(外文):Pao-Ann Hsiung
學位類別:碩士
校院名稱:國立中正大學
系所名稱:資訊工程所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:2006
畢業學年度:94
語文別:英文
論文頁數:70
中文關鍵詞:部分模型檢驗涵輔v評估
外文關鍵詞:partial model checkingcoverage estimation
相關次數:
  • 被引用被引用:0
  • 點閱點閱:177
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
在一個系統模型通過模型檢驗後,我們會評估涵輔v以得知多少部分的系統模型被檢驗過。前人所提出的一個涵輔v評估方法為: (1)將系統模型做些微改變(變異)後,(2)對此變異的系統模型做模型檢驗,(3)再將變異的系統模型還原;重複循環以上三個步驟,最後以步驟(2)中多次模型檢驗通過與否的結果來計算涵輔v。當我們對一個複雜且龐大的系統模型評估其涵輔v時,此涵輔v評估方法需要耗費相當長的時間。然而如此長的評估時間是不容易被接受的。
在此涵輔v評估的方法中,多次的模型檢驗在時間耗費上是一個相當大的瓶頸。因此,我們提出了一個部分模型檢驗方法,取代步驟(2)所用的模型檢驗方法以增進效率。過去模型檢驗方法是對系統所有的系統狀態重新貼標籤,在這篇論文中所提的部分模型檢驗方法則會保留在涵輔v評估前的模型檢驗所貼之標籤,接著從有變異的系統狀態開始,只重貼被變異所影響到的系統狀態之標籤,藉此來縮短貼標籤所耗費的時間。最後,我們證明了此部份模型檢驗方法之正確性以及用多個實例驗證我們所提的部份模型檢驗之效率。
The mutation based coverage
estimation methodology for model checking applies mutations to a system model
to obtain the mutated system models and re-performs model checking on the
mutated system models. The coverage is evaluated according to the model
checking results of the mutated system models. A previously proposed mutation
based coverage estimation methodology requires a lot of time to calculate the
coverage when a system model is complex and large. For example, it takes 15
hours to estimate the coverage of an entrance guard system. Such a lengthy
estimation time is not acceptable by the designers. The main bottleneck in
coverage estimation is the large amount of time spent in repeated model
checking. In this work, we propose a partial model checking algorithm to
improve the previously proposed coverage estimation methodology to be more
efficient. The partial model checking algorithm re-labels from the point where
the mutation occurs, and it only re-labels on the modes which are affected by
the mutation rather than the whole modes. By applying the partial model
checking algorithm, we can decrease the coverage estimation time by about
23%~46% by means of avoiding the actions of clearing previously marked
labels and of redoing the labelling for the modes that are still satisfies the
properties after mutation.
1 Introduction
1.1 Motivation 1.2 Proposed Method 1.3 Thesis Organization 2 Related Work System Model, Specification, and Mutation Types 3.1 System Model
3.2 Specification 3.3 Mutations 3.3.1 Delayed Transition
3.3.2 Stuttering Mode 3.3.3 Skipped Mode 3.3.4 Removed Transition 3.3.5 Mutated Invariant 4 Eficient Coverage Estimation Methodology
4.1 Coverage Estimation Methodology for Symbolic Model Checking
4.2 The Accelerated Coverage Estimation Methodology
4.2.1 An Example 5 Experiment Results 6 Conclusions and Future Work
[1] Accellera OVL Technical Committee. http://www.eda.org/ovl/.
[2] PSL Sugar Consortium. http://www.pslsugar.org/.
[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 In-ternational Conference on Theoretical Computer Science, 126(2):183{235, April 1994.
[5] K.-T. Cheng and A. Krishnakumar. Automatic Functional Test Generation Using
the Extended Finite State Machine Model. In Proceedings of the IEEE/ACM
Design Automation Conference, pages 86{91, June 1993.
[6] H. Chockler, O. Kupferman, R. Kurshan, and M. Vardi. 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
Volume 2102, pages 66{78. Springer-Verlag, July 2001.
[7] 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 Volume 2031, pages 528{542. Springer-Verlag, April 2001.
[8] 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 Volume
2860, pages 111{125. Springer-Verlag, October 2003.
[9] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244{263, April
1986.
[10] E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. The MIT
Press, 1999.
[11] E. A. Emerson and E. M. Clarke. Using branching time logic to synthesize
synchronization skeletons. Science of Computer Programming, 2(3):241{266,
September 1982.
[12] 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 Mod-
els for Co-Design (MEMOCODE'03), pages 145{152. IEEE Computer Society
Press, June 2003.
[13] F. Fummi, G. Pravadelli, and F. Toto. Coverage of Formal Properties based on
a High-Level Fault Model and Functional ATPG. In Proceedings of the European
Test Symposium (ETS05), pages 162{167, May 2005.
[14] Y. Hoskote, T. Kam, P.-H. Ho, and X. Zhao. Coverage Estimation for Sym-
bolic Model Checking. In Proceedings of the IEEE/ACM Design Automation
Conference, pages 300{305. ACM Press, June 1999.
[15] P.-A. Hsiung and F. Wang. A State Graph Manipulator Tool for Real-Time
System Specification and Verification. In Proceedings of 4th International Conference on Real-Time Computing Systems and Applications (RTCSA'98), pages
181{188. IEEE Computer Society Press, October 1998.
[16] N. Jayakumar, M. Purandare, and F. Somenzi. Do's and don'ts of CTL state
coverage estimation. In Proceedings of the IEEE/ACM Design Automation Con-
ference (DAC'03), pages 292{295. ACM Press, June 2003.
[17] M. Kantrowitz and L. Noack. Im Done Simulating: Now What? Verification
Coverage Analysis and Correctness Checking of the DEC chip 21164 ALPHA
Microprocessor. In Proceedings of the IEEE/ACM Design Automation Confer-
ence, pages 325{330, June 1996.
[18] T.-C. Lee. Mutation Coverage Estimation for Symbolic Model Checking. Mas-
ter's Thesis, Dept. of Computer Science & Information Engineering, National
Chung Cheng University, Chiayi, Taiwan, July 2004.
[19] 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.
[20] W.-S. Liao and P.-A. Hsiung. Modeling Hardware Systems with Complex Clock
Synchronizations in the SGM Formal Verifier. In Proceedings of 14th VLSI Design / CAD Symposium, pages 177{180, August 2003.
[21] J-P. Queille and J. Sifakis. Specification and verification of concurrent systems
in CESAR. In Proceedings of 5th Colloquium on International Symposium on
Programming, pages 337{351, April 1982.
[22] E. Rodriguez, M. B. Dwyer, J. Hatcli®, and Robby. A Flexible Framework for
the Estimation of Coverage Metrics in Explicit State Software Model Check-
ing. In Proceedings of the International Workshop on Construction and Analy-
sis of Safe, Secure, and Interoperable Smart Devices (CASSIS), pages 210{228.
Springer Berlin / Heidelberg, March 2004.
[23] Robert E. Tarjan. Depth-first search and linear graph algorithms. Society for Industrial and Applied Mathematics (SIAM) Journal on Computing, pages 146{
160, January.
[24] F.Wang and P.-A. Hsiung. E±cient and User-Friendly Verification. IEEE Transactions on Computers, 51(1):61{83, January 2002.
[25] F. Wang, G.-D. Hwang, and F. Yu. Numerical Coverage Estimation for the
Symbolic Simulation of Real-Time Systems. In Proceedings of the Interna-
tional Conference on Formal Techniques for Networked and Distributed Systems
(FORTE'03), LNCS 2767, pages 160{176. Springer-Verlag, September 2003.
[26] 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.
[27] Xingwen Xu, Shinji Kimura, Kazunari Horikawa, and Takehiko Tsuchiya.
Transition-Based Coverage Estimation for Symbolic Model Checking. In Proceedings of the Asia South Pacific Design Automation Conference (ASPDAC),
pages 1{6. ACM Press, January 2006.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關論文
 
1. 黃程貫,我國勞動法發展趨勢之觀察與展望,月旦法學雜誌,第100期,頁91-106,民國92年9月。
2. 黃程貫,德國勞工派遣關係之法律結構,政大法學評論,第60期,頁271-301,民國87年12月。
3. 黃立,契約自由的限制,月旦法學,第125期,頁5-22,民國94年10月。
4. 盛惠煜,加強非典型僱佣型態勞動者之勞動條件保護研究,臺灣銀行季刊,第55卷第4期,頁227-261,民國93年12月。
5. 陳金泉,職業災害補償實務爭議案例解析,政大勞動學報,第12期,頁425-455,民國91年7月。
6. 邱駿彥,勞動契約關係存否之法律上判斷標準(以特別看護與醫院間之勞動契約為例),政大法學評論,第63期,頁359-372,民國89年6月。
7. 邱駿彥,勞動派遣之法律關係探討,萬國法律,第138期,頁50-66,民國93年12月。
8. 邱祈豪,派遣勞工職業能力開發及評價制度之探討,萬國法律,第138期,頁67-81,民國93年12月。
9. 吳若萱,派遣勞動如何重塑僱傭關係與企業用人政策,勞工行政,第147期,頁34-41,民國89年7月。
10. 吳全成,青少年部分工時人力運用兼論我國工讀生問題,勞工研究,第134期,頁1-9,民國88年1月。
11. 李來希,談派遣勞動之立法規範,勞工行政,第87期,頁52-56,民國84年7月。
12. 李來希,三角習題 兩岸頻傳 談派遣勞動之立法規範,實用稅務,第246期,頁85-89,民國84年6月。
13. 成之約,「派遣勞動」及其發展的探討:工會觀點,萬國法律,第138期,頁2-14,民國93年12月。
14. 成之約,部分時間工作發展與所得分配問題,國家政策論壇季刊,春季號,頁221-237,民國93年1月。
15. 成之約、莊美娟,資訊科技運用對勞資關係影響之初探,經社法制論叢,第26期,頁167-193,民國89年7月。
 
系統版面圖檔 系統版面圖檔