基于模型驗(yàn)證的故障定位方法研究.pdf

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

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

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