基于模型驗證的故障定位方法研究.pdf

1、軟件運行出現(xiàn)故障之后，軟件故障定位非常困難。傳統(tǒng)的軟件定位方法主要是結(jié)合測試技術(shù)，使用有針對性的測試，發(fā)現(xiàn)軟件中存在的特定缺陷，再利用其他輔助技術(shù)找出故障原因并定位故障，這些定位方法主要依賴于開發(fā)者的經(jīng)驗，存在過程復雜、依賴性強和通用性不高等缺陷，不能滿足軟件故障自動定位的要求。形式化方法是軟件故障自動定位方法研究的基礎(chǔ)，形式化方法中模型驗證以其高效、自動化的優(yōu)點使其在越來越多的領(lǐng)域中被運用。
　　 模型驗證是一種對有限狀態(tài)遷移

2、系統(tǒng)驗證其時態(tài)邏輯性質(zhì)的重要方法，由于模型驗證過程完全自動化，所以非常適合于驗證復雜系統(tǒng)性質(zhì)的要求。如果能夠?qū)⒛Ｐ万炞C技術(shù)運用在故障定位技術(shù)中，則可在一定程度上支持軟件故障自動定位研究，從而成為一個提高軟件可靠性的重要手段。
　　 本文針對軟件故障自動定位研究的需要，提出了一種基于模型驗證的軟件故障定位方法，并在此方法的基礎(chǔ)之上給出了一個故障定位原型系統(tǒng)框架并部分實現(xiàn)了自動化。經(jīng)實驗表明，該方法能大大減少在故障定位過程中代碼審查

3、的范圍，能快速有效地定位軟件故障，從而為軟件故障定位提供了一種新途徑。
　　 本文的主要工作包括以下幾個部分：
　　 1)建立支持軟件故障定位的形式模型。研究了軟件模型驗證的基本過程，完成了從軟件源代碼到軟件形式模型的建立，詳細設(shè)計了建模過程中涉及的數(shù)據(jù)結(jié)構(gòu)和算法，并對算法進行了性能分析。
　　 2)基于模型驗證的故障定位方法研究。在模型建立的基礎(chǔ)之上，建立了建?！炞C—定位過程的故障定位系統(tǒng)的框架，結(jié)合模型驗證