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

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

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