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

Abstract

為了使系統符合安全性質還有我們所期望的行為，我們提出一個演算法，根據系統必須分歧模擬一個下限 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.