基于UML的軟件系統(tǒng)的功能性驗(yàn)證和非功能性度量.pdf

1、隨著軟件系統(tǒng)的日益龐大,對(duì)軟件的要求也越來越高,對(duì)軟件模型的驗(yàn)證和性能的度量,受到前所未有的關(guān)注,同時(shí)基于統(tǒng)一建模語言(Unified ModelingLanguage,UML)[1][2]的軟件設(shè)計(jì)方法也日益成為一種行業(yè)標(biāo)準(zhǔn),因此從UML中獲得一些需求和性能的信息,分析并發(fā)現(xiàn)系統(tǒng)中潛在的漏洞和性能瓶頸,將成為一種優(yōu)秀的解決方法。
　　 UML是一種通用的可視化建模語言,它具有建模方法直觀、易于理解、便于表達(dá)和使用、代碼生成等優(yōu)

2、點(diǎn)。但是UML語言缺少精確的形式化描述。而Petri網(wǎng)則是一個(gè)側(cè)重描述動(dòng)態(tài)行為的形式化描述語言,尤其能很好的描述系統(tǒng)的并發(fā)和分布系統(tǒng)[3]。
　　 本文充分結(jié)合UML和Petri網(wǎng)這兩種建模語言,互相取長補(bǔ)短:一方面可以對(duì)軟件進(jìn)行直觀設(shè)計(jì),另一方面可以描述軟件的動(dòng)態(tài)行為。首先將系統(tǒng)用UML進(jìn)行描述,然后把帶有非功能信息的UML狀態(tài)圖轉(zhuǎn)換為Petri網(wǎng)模型,基于這個(gè)Petri網(wǎng)模型,我們可以驗(yàn)證功能性和對(duì)非功能性進(jìn)行度量。

3、　　 在功能性驗(yàn)證方面,過濾Petri網(wǎng)模型中的與非功能信息,通過定義轉(zhuǎn)換規(guī)則將Petri網(wǎng)轉(zhuǎn)到模型檢測(cè)工具SPIN的輸入語言-PROMELA語言,我們將所要檢查的功能用線性時(shí)序邏輯公式(LTL)表示。通過分析SPIN的運(yùn)行結(jié)果和系統(tǒng)的執(zhí)行路徑,我們可以判斷出該功能是否滿足系統(tǒng)。
　　 在非功能度量方面,我們將Petri網(wǎng)轉(zhuǎn)化為隨機(jī)Petri網(wǎng)(SPN),由于任何含有有窮個(gè)庫所、有窮個(gè)變遷的連續(xù)時(shí)間的SPN同構(gòu)于一個(gè)連續(xù)時(shí)間馬