摘要:UML是一種廣泛使用的面向?qū)ο蟮目梢暬y(tǒng)一建模語言,但UML缺乏精確的語義描速,難以對UML模型進(jìn)行分析驗(yàn)證以判斷設(shè)計(jì)規(guī)范是否滿足目標(biāo)需求。符號模型檢驗(yàn)是一種能夠有效保證系統(tǒng)可信性質(zhì)的自動檢驗(yàn)技術(shù)。為了檢驗(yàn)UML模型的正確性,在建模的基礎(chǔ)土把UML模型轉(zhuǎn)換為SMV模型,然后使用符號模型檢驗(yàn)器(SMV)對模型進(jìn)行檢驗(yàn),有利于在系統(tǒng)的設(shè)計(jì)早期發(fā)現(xiàn)系統(tǒng)的缺陷。
關(guān)鍵詞:UML;符號模型檢驗(yàn);SMV;模型轉(zhuǎn)換
中圖分類號:TN919—34 文獻(xiàn)標(biāo)識碼:A 文章編號:1004—373X(2011)06—0049—03