請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/37012
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 王凡(Farn Wang) | |
dc.contributor.author | Ying-Chih Wang | en |
dc.contributor.author | 王映智 | zh_TW |
dc.date.accessioned | 2021-06-13T15:17:52Z | - |
dc.date.available | 2009-07-27 | |
dc.date.copyright | 2008-07-27 | |
dc.date.issued | 2008 | |
dc.date.submitted | 2008-07-25 | |
dc.identifier.citation | [1] R. Alur, C. Courcoubetis, and D.L. Dill. Model Checking for Real-Time Systems, IEEE LICS, 1990.
[2] T. Ball, M. Naik, and S. K. Rajamani, From symptom to cause: Localizing errors in counterexample traces. In 30th Symposium on Principles of Programming Languages(POPL 2003), pages 97-105, January 2003. [3] E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking, pages 171-176, The MIT Press, 1999. [4] K. Etessami, T. Wilke, and R. A. Schuller. Fair Simulation Relations, Parity Games, and State Space Reduction for Buchi Automata. In Proceedings of the 28th International Colloquium on Automata, Languages and Programming, pages 694-707, Springer-Verlag , 2001, LNCS2076. [5] R. J. van Glabbeek and W. P. Weijland. In Journal of the ACM, 43(3):pages 555-600, ACM, May 1996 [6] A. Groce and W Visser. What when wrong: Explaining counterexamples. In Model Checking of Software: 10th International SPIN Workshop, pages 121-135, Springer-Verlag, May 2003. LNCS2648. [7] A. Groce. Error explanation with distance metrics. In 10th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’04), pages 108-122, Springer-Verlag, 2004. LNCS2988 [8] A. Griesmayer, R. Bloem, and B Cook. Repair of boolean programs with an application to C. In 18th Conference on Computer Aided Verification(CAV’06), pages 358-371, Springer-Verlag, 2006, LNCS4144. [9] A. Griesmayer, S. Staber, and R. Bloem. Automated Fault Localization for C Programs. In Proceedings of the Workshop on Verification and Debugging 2006, pages 95-111, Elsevier Science Publishers, May 2007. ENTCS174. [10] T. A. Henzinger, R. Jhala, R. Majumdar and G. Sutre. Lazy abstraction. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pages 58-70, 2002. [11] H. Jin, K. Ravi, and F. Somenzi. Fate and free will in error traces. In International Journal on Software Tools for Technology Transfer, 6(2):102-116, Springer-Verlag, August 2004. [12] B. Jobstmann, A. Griesmayer, and R. Bloem. Program repair as a game. In 17th Conference on Computer Aided Verification(CAV’05), pages 226-238. Springer-Verlag, 2005, LNCS3576. [13] G. J. Myers, C. Sandler, T. Badgett and T. M. Thomas. The Art of Software Testing. Wiley, 2004. [14] G. Katz and D. Peled. Model Checking-Based Genetic Programming with an Application to Mutual Exclusion. In 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08), pages 141-156, Springer-Verlag, 2008. LNCS4963 [15] M. Renieris and S. P. Reiss. Fault localization with nearest neighbor queries. In International Conference on Automated Software Engineering, pages 30-39, Montreal, Canada, October 2003. [16] A. Silberschatz, P. B. Galvin and G. Gagne. Operating System Principles. Wiley, 2007 [17] F. Wang. Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’00), pages 157-171, Springer-Verlag, LNCS1785. [18] F. Wang. Efficient Verification of Timed Automata with BDD-like Data-Structures, In Journal of Software Tools for Technology Transfer, Vol. 6, Nr. 1, June 2004, Springer-Verlag; Special issue for VMCAI2003, LNCS 2575, Springer-Verlag [19] 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. [20] F. Wang. REDLIB for the Formal Verification of Embedded Systems. In Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), pages 341-346. 2006. [21] F. Wang, G. Huang, F. Yu. TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering. In IEEE Transactions on Software Engineering, Vol.32, No. 7 IEEE Computer Society, July 2006. [22] F. Wang, C. Cheng. Model Repair with an Automata-Theoretical Approach with a Cost Concept. In 1st Workshop on Omega-Automata (Omega 2007) [23] A. Zeller. Isolating cause-effect chains from computer programs. In 10th International Symposium on the Foundations of Software Engineering (FES-10), pages 1-10, November 2002. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/37012 | - |
dc.description.abstract | 為了使系統符合安全性質還有我們所期望的行為,我們提出一個演算法,根據系統必須分歧模擬一個下限 Kripke structure(KLB) 且必須被一個上限Kripke structure(KUB)所分歧模擬的規格,在表示成防護命令的狀態轉換系統中定位錯誤。我們演算法是一個兩階段的分歧與限制演算法。第一個階段中,在一些防護命令中的變數被當成是可疑的,然後這些防護命令會被停用,再加入所有可疑變數組合產生所產生的一組新的防護命令。這個階段會一直反覆執行直到系統的Kripke structure能夠分歧模擬KLB。第二個階段中,那些被加入的防護指令會一次次地被拿掉直到系統符合規格或是所有可能的指令的組合都嘗試過了。若是找不到符合規格的系統,那這兩個階段會反覆執行直到找到一個能夠符合規格的系統。一旦找到一個符合規格的系統,這些在防護指令中可疑的變數就被當成是錯誤並且回傳給使用者。除此之外我們還會討論幾項會影響我們系統效能或是找到錯誤的品質的因素。 | zh_TW |
dc.description.abstract | We propose an algorithm that localizes faults in a state transition system represented
by a set of guarded commands with respect to safety properties and desired system scenarios represented by a specification that the system should branching simulate a lower-bound Kripke structure KLB and should be branching simulated by an upper-bound Kripke structure KUB. Our algorithm is a branch-and-bound algorithm with two phases. In the first phase, certain sets of suspicious variable occurrences in some guarded commands are iteratively chosen, and those guarded commands with occurrences of suspicious variables are suspended and then all combinations of suspicious variable occurrences in those guarded commands are added to the system. This phase is looped until the modified system simulates KLB. In the second phase, those guarded commands which are added to the system are iteratively removed until the modified system satisfies the specification or all possible systems are tested. If no system which satisfies the specification is found, the two phases will iterate again and again until the system satisfies the specification. Once a modified system satisfies the specification, the set of suspicious variable occurrences in the guarded commands is returned to the user as the faults. Moreover, several factors that affect the performance of our algorithm and the quality of found solutions are discussed. | en |
dc.description.provenance | Made available in DSpace on 2021-06-13T15:17:52Z (GMT). No. of bitstreams: 1 ntu-97-R95943071-1.pdf: 681838 bytes, checksum: adf7a2ab6b869a81638f4da72452c80b (MD5) Previous issue date: 2008 | en |
dc.description.tableofcontents | Contents i
List of Figures iii Acknowledgements v 1 Introduction 1 2 Related Work 4 3 Preliminaries 7 3.1 Kripke structure . . . . . . . . . . . . . . . . 7 3.2 Simulation . . . . . . . . . . . . . . . . . . . 8 3.3 Branching Simulation . . . . . . . . . . . . . 10 3.4 RED and REDLIB . . . . . . . . . . . . . . . . 12 4 Fault Localization with Branching Simulation 13 4.1 System Description . . . . . . . . .. . . . . . 13 4.2 Specification . . . . . . . . . . . . . . . . . 15 4.3 Fault Model . . . . . . . . . . . . . . .. . . .17 4.4 Notations . . . . . . . . . . . . . . . . . . . 17 4.5 Problem Definition . . . . . . . . . . . . . . 18 4.6 Algorithm . . . . . . . . . . . . . . . . . . . 19 4.6.1 An Exhaustive Search Algorithm . . . . . . . 19 4.6.2 A Branch-and-Bound algorithm . . . . . . . . 21 5 Implementation 25 5.1 Libraries . . . . . . . . . . . . . . . . . .. 25 5.2 Classes . . . . . . . . . . . . . . . . . . . . 26 5.3 Representation of Possible Models . . . . . . . 27 5.4 Representation of Suspicious Variables . .. . . 27 5.5 Input Format . . . . . .. . . . . . . . . . . . 28 6 Experiment 29 6.1 Case Study: Peterson’s Algorithm . . . . . . 33 6.2 Case Study: Solution of Reader-Writer Problem . 36 6.3 Discussion . . . . . . . . . . . . . . . . . . 39 7 Conclusions and Future Directions 40 Bibliography 41 A Partial Interface of REDLIB 44 B A Sample Model File of REDLIB 46 C A Sample Input File of Our Tool 49 D A sample specification for Peterson’s algorithm 51 | |
dc.language.iso | en | |
dc.title | 使用分歧模擬技術的狀態轉換系統之錯誤定位 | zh_TW |
dc.title | Fault Localization of State Transition Systems with Branching Simulation | en |
dc.type | Thesis | |
dc.date.schoolyear | 96-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 雷欽隆(Chin-Laung Lei),江介宏(Jie-Hong Roland Jiang),黃鐘揚(Chung-Yang Huang),張耿銘 | |
dc.subject.keyword | 除錯,錯誤定位,分歧模擬, | zh_TW |
dc.subject.keyword | debugging,fault localization,branching simulation, | en |
dc.relation.page | 52 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2008-07-25 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 電子工程學研究所 | zh_TW |
顯示於系所單位: | 電子工程學研究所 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
ntu-97-1.pdf 目前未授權公開取用 | 665.86 kB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。