基于UML的系統(tǒng)需求形式化分析方法.pdf

1、Unified Modeling Language（UML，建模語(yǔ)言或標(biāo)準(zhǔn)建模語(yǔ)言）始于1997年的一個(gè)OMG（Object Management Group，對(duì)象管理組織）標(biāo)準(zhǔn)，是一個(gè)支持模型化和軟件系統(tǒng)開(kāi)發(fā)的圖形化語(yǔ)言，為軟件開(kāi)發(fā)的所有階段提供模型化和可視化支持，包括由需求分析到規(guī)格，到構(gòu)造和配置。UML允許添加類(lèi)級(jí)和系統(tǒng)級(jí)約束，但其中并沒(méi)有定義如何檢查這些約束的正確性。大多數(shù)UML規(guī)范是描述性的，容易理解，但由于不是形式化的描述語(yǔ)

2、言缺乏精確的語(yǔ)義，這使得對(duì)其中的約束進(jìn)行正確性檢驗(yàn)十分的困難。為保證系統(tǒng)的正確性并降低其開(kāi)發(fā)的成本和之后的運(yùn)行風(fēng)險(xiǎn)，盡早對(duì)系統(tǒng)進(jìn)行安全驗(yàn)證就顯得尤為重要。特別是需求規(guī)范中如存有潛在缺陷，會(huì)對(duì)系統(tǒng)的開(kāi)發(fā)過(guò)程帶來(lái)重大的影響，如果在系統(tǒng)開(kāi)發(fā)階段不能及時(shí)發(fā)現(xiàn)，很可能會(huì)導(dǎo)致系統(tǒng)在運(yùn)行階段失效從而帶來(lái)災(zāi)難性的后果。
　　本文主要探討系統(tǒng)需求分析階段的形式化分析方法，通過(guò)模型檢測(cè)來(lái)驗(yàn)證UML規(guī)范的約束，并給出了一個(gè)實(shí)例的規(guī)范及轉(zhuǎn)換驗(yàn)證UML規(guī)范

3、的過(guò)程。通過(guò)對(duì)需求階段實(shí)例進(jìn)行分析得到需求的UML建模模型，選取模型中的類(lèi)圖、狀態(tài)圖和順序圖，設(shè)計(jì)了將UML模型圖例轉(zhuǎn)換為SMV（Symbolic Model Verifier，符號(hào)模型檢驗(yàn)器）描述的轉(zhuǎn)換規(guī)則和對(duì)轉(zhuǎn)換規(guī)則進(jìn)行代碼實(shí)現(xiàn)后的具體化工具，使得轉(zhuǎn)換后的UML模型可以被符號(hào)模型檢驗(yàn)器NuSMV(New Symbolic Model Verifier，新型符號(hào)模型檢驗(yàn)器)接受以驗(yàn)證系統(tǒng)的性能，并可查看到驗(yàn)證返回的反例和驗(yàn)證過(guò)程中檢測(cè)