符號(hào)模型檢測(cè)反例的研究.pdf

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

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

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