NuSMV模型檢測(cè)的研究及應(yīng)用.pdf

1、計(jì)算機(jī)軟硬件系統(tǒng)日益復(fù)雜，其正確性和可靠性已成為計(jì)算機(jī)領(lǐng)域中研究的熱點(diǎn)，在諸多方法和理論中，模型檢測(cè)以其簡(jiǎn)潔明了和自動(dòng)化程度高而倍受關(guān)注。模型檢測(cè)的關(guān)鍵問(wèn)題是狀態(tài)爆炸問(wèn)題，具體來(lái)說(shuō)就是如何使用精簡(jiǎn)方式描述系統(tǒng)，避免因?yàn)槟Ｐ蛷?fù)雜而引起狀態(tài)爆炸。
　　 模型檢測(cè)技術(shù)的成功應(yīng)用必須以有效驗(yàn)證工具為基礎(chǔ)，NuSMV作為一種有效的分析驗(yàn)證并發(fā)系統(tǒng)邏輯一致性的模型檢測(cè)工具得到了越來(lái)越廣泛的應(yīng)用。本文在闡述模型檢測(cè)形式化分析機(jī)理及時(shí)態(tài)邏輯性質(zhì)

2、的基礎(chǔ)上，詳細(xì)分析了NuSMV作為一個(gè)模型檢測(cè)器在PCI協(xié)議總線上的應(yīng)用。通過(guò)詳細(xì)分析PCI總線協(xié)議規(guī)約的要求，基于NuSMV對(duì)PCI總線協(xié)議的總線命令和總線信號(hào)及動(dòng)作進(jìn)行了建模，包括總線信號(hào)和命令的建模，主從設(shè)備讀/寫(xiě)transactions的建模及設(shè)備調(diào)度策略的建模。應(yīng)用NuSMV進(jìn)行了具體的實(shí)現(xiàn)并檢測(cè)了其屬性對(duì)規(guī)約的要求，結(jié)果表明：如果NuSMV檢測(cè)的結(jié)果是FALSE，則說(shuō)明屬性不滿足，且NuSMV可以給出其反例來(lái)詳細(xì)說(shuō)明違反屬性