基于UML的建模及模型檢驗(yàn)研究
2011-04-12 00:00:00吳曉丹寧濱
現(xiàn)代電子技術(shù) 2011年6期
摘要：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
