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

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

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