符號模型檢測反例的研究.pdf

1、計算機的使用越來越普及，人們對計算機的依賴程度也越來越高。計算機軟硬件系統(tǒng)規(guī)模也隨之日益復(fù)雜，如何保證其正確性和可靠性，逐漸成為當(dāng)前理論界和產(chǎn)業(yè)界共同關(guān)心的重要問題。因此，形式化方法中的模型檢測以其高效、自動化的優(yōu)點使其在越來越多的領(lǐng)域中被運用。與其他形式化驗證方法相比，模型檢測的特點在于：第一，模型檢測是基于模型而不是基于演繹推理的；第二，模型檢測方法不需要激勵碼，能夠自動完成驗證工作；第三，模型檢測是屬性驗證過程，當(dāng)系統(tǒng)模型不滿足屬

2、性時，模型檢測方法能夠給出反例，以說明其原因。反例為診斷和修復(fù)系統(tǒng)模型的錯誤提供了依據(jù)。從測試的角度，模型檢測自動生成反例，可以用于實現(xiàn)測試用例自動化生成。
　　 然而，由于復(fù)雜系統(tǒng)的反例通常很長而且難以理解，需要花費很長的時間檢查大量的變量和事件，才能夠找到錯誤的真正原因。這就影響了模型檢測的效率。在反例構(gòu)造測試用例時，一個反例可能對應(yīng)多個屬性的違背。因此，產(chǎn)生的測試集往往存在大量冗余的和不必要的測試用例，從而降低了測試執(zhí)行的

3、效率。
　　 針對上述問題，本文主要的工作及創(chuàng)新點在于：
　　 1、傳統(tǒng)的算法是通過窮盡的搜索來找到反例，通過分析傳統(tǒng)的算法，本文提出一種改進(jìn)的算法，該算法將反例中的狀態(tài)擴展為一個狀態(tài)集，使用ZBDD來存儲所求出的狀態(tài)集。刪除了系統(tǒng)中無關(guān)的變量，保留相關(guān)的變量。實驗分析的結(jié)果表明了算法的有效性。
　　 2、由于冗余測試用例的存在會增加測試的成本，現(xiàn)有的化簡方法或在測試集產(chǎn)生后在進(jìn)行化簡，或改變和擴展模型檢測器使新