使用分歧模擬技術的狀態轉換系統之錯誤定位

Fault Localization of State Transition Systems with Branching Simulation

王映智(Ying-Chih Wang)

指導教授 ： 王凡

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2008年)

https://doi.org/10.6342/NTU.2008.02072

摘要

為了使系統符合安全性質還有我們所期望的行為，我們提出一個演算法，根據系統必須分歧模擬一個下限 Kripke structure(KLB) 且必須被一個上限Kripke structure(KUB)所分歧模擬的規格，在表示成防護命令的狀態轉換系統中定位錯誤。我們演算法是一個兩階段的分歧與限制演算法。第一個階段中，在一些防護命令中的變數被當成是可疑的，然後這些防護命令會被停用，再加入所有可疑變數組合產生所產生的一組新的防護命令。這個階段會一直反覆執行直到系統的Kripke structure能夠分歧模擬KLB。第二個階段中，那些被加入的防護指令會一次次地被拿掉直到系統符合規格或是所有可能的指令的組合都嘗試過了。若是找不到符合規格的系統，那這兩個階段會反覆執行直到找到一個能夠符合規格的系統。一旦找到一個符合規格的系統，這些在防護指令中可疑的變數就被當成是錯誤並且回傳給使用者。除此之外我們還會討論幾項會影響我們系統效能或是找到錯誤的品質的因素。

關鍵字

除錯 ； 錯誤定位 ； 分歧模擬

並列摘要

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.

並列關鍵字

debugging ； fault localization ； branching simulation

參考文獻

[1] R. Alur, C. Courcoubetis, and D.L. Dill. Model Checking for Real-Time Systems, IEEE LICS, 1990.

[3] E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking, pages 171-176, The MIT Press, 1999.

[5] R. J. van Glabbeek and W. P. Weijland. In Journal of the ACM, 43(3):pages 555-600, ACM, May 1996

[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

[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.