1、隨著計(jì)算機(jī)軟硬件系統(tǒng)日益復(fù)雜,如何保證其正確性和可靠性成為日益緊迫的問題。各國(guó)研究人員為解決這個(gè)問題付出了巨大的努力,并取得了很大的進(jìn)展。在提出的諸多理論和方法中,模型檢驗(yàn)以其簡(jiǎn)潔明了及自動(dòng)化程度高而引人注目。模型檢驗(yàn)利用面向系統(tǒng)的某類性質(zhì)來檢查它是否滿足規(guī)約,在系統(tǒng)不滿足所要求的規(guī)約條件時(shí),算法會(huì)產(chǎn)生一個(gè)反例說明不滿足的原因,它與測(cè)試有異曲同工之處。
　　論文針對(duì)狀態(tài)空間搜索,對(duì)模型檢驗(yàn)和測(cè)試相結(jié)合的方法進(jìn)行了深入研究,并提出了

2、相應(yīng)的改進(jìn)算法,通過這些算法不僅保證系統(tǒng)的正確性和可靠性,而且改進(jìn)了狀態(tài)空間復(fù)雜度問題。
　　論文的主要工作如下:
　　(1)結(jié)合模型檢驗(yàn)對(duì)測(cè)試技術(shù)進(jìn)行了研究,提出了測(cè)試結(jié)構(gòu)和產(chǎn)生測(cè)試用例的方法。通過它可進(jìn)一步保證系統(tǒng)的正確性和可靠性。
　　(2)根據(jù)符號(hào)化狀態(tài)圖的思想,對(duì)FSM轉(zhuǎn)化為OBDD的方法進(jìn)行了研究,提出了具體的轉(zhuǎn)化算法。
　　(3)對(duì)圖搜索的非啟發(fā)式和啟發(fā)式算法的復(fù)雜度及其相互關(guān)系進(jìn)行了深入研究,提出