UML活動(dòng)圖模型檢測(cè)方法的研究.pdf

1、隨著人們對(duì)軟件正確性和安全性的要求越來(lái)越高，高可信軟件工程技術(shù)得到了研究人員的廣泛關(guān)注。在高可信軟件工程中，模型檢測(cè)以其簡(jiǎn)潔明了和自動(dòng)化程度高而倍受矚目。模型檢測(cè)是一種重要的形式化自動(dòng)驗(yàn)證技術(shù)，其中SPIN是一種著名的分析驗(yàn)證系統(tǒng)邏輯一致性的模型檢測(cè)工具，輸入語(yǔ)言是PROMELA語(yǔ)言。
　　統(tǒng)一建模語(yǔ)言UML是一種半形式化建模語(yǔ)言，缺乏精確的語(yǔ)義描述。本文研究了UML活動(dòng)圖與模型檢測(cè)兩者之間的結(jié)合，主要研究?jī)?nèi)容包括以下幾點(diǎn)：

2、>　　1、在UML的各種圖形中，活動(dòng)圖易于理解，用于對(duì)系統(tǒng)的動(dòng)態(tài)行為建模。本文研究了活動(dòng)圖中的節(jié)點(diǎn)及語(yǔ)義，活動(dòng)圖由事件流將整個(gè)活動(dòng)過(guò)程串聯(lián)在一起的，消息的發(fā)送和接受是隨著事件流進(jìn)行的。
　　2、實(shí)現(xiàn)了UML活動(dòng)圖到PROMELA語(yǔ)言的轉(zhuǎn)換。首先將UML活動(dòng)圖轉(zhuǎn)換成XML語(yǔ)言，然后再將XML語(yǔ)言轉(zhuǎn)換成PROMELA語(yǔ)言，經(jīng)歷了這樣兩次轉(zhuǎn)換，其中第一次轉(zhuǎn)換：將UML語(yǔ)言轉(zhuǎn)換成XML使用建模工具StarUML來(lái)實(shí)現(xiàn)的，本文中用MFC實(shí)現(xiàn)

3、了將活動(dòng)圖的XML語(yǔ)言轉(zhuǎn)換成PROMELA語(yǔ)言的過(guò)程。
　　3、總結(jié)了PROMELA語(yǔ)言建模的一般規(guī)律，并在活動(dòng)圖模型檢測(cè)過(guò)程中實(shí)踐了這一規(guī)律。通過(guò)分析UML活動(dòng)圖的XML文件內(nèi)部表示形式，將活動(dòng)圖定義為一個(gè)五元組，A=，其中P:狀態(tài)的有限集合；M:事件流的有限集合；T:事件流的分類(lèi)，提出了將事件流分為common和special兩種形式，其中common指的是令牌為空的情況，special指的是令牌不為空的