本文關(guān)鍵詞：使用UML和Event-B構(gòu)建基于云平臺的應(yīng)用軟件模型，由筆耕文化傳播整理發(fā)布。

【摘要】：軟件工程實踐中廣泛采用UML(Unified Modeling Language)作為建模語言,UML是一種語言,也可以稱其為一種技術(shù)。UML具有半形式化的特點,它的形式化部分使其具有嚴密和精確的特點,它的非形式化部分使其易于接受和推廣。UML模型構(gòu)件的結(jié)構(gòu)采用形式化描述,而相應(yīng)的語義采用自然語言描述,這是將UML稱為半形式化技術(shù)的原因之一。另外,UML技術(shù)可以對模型進行形式化的描述,但是UML技術(shù)本身沒有指出如何對模型進行形式化驗證,這是將UML稱為半形式化技術(shù)的原因之二。事實上,UML的半形式化特點固然使其易于使用、易于推廣,但是不能支持一些軟件工程的應(yīng)用場景。如果需要分析軟件模型演進的一致性,這是單獨使用UML技術(shù)不能做到的。UML模型在軟件工程的不同階段會持續(xù)演進,演進過程中會引入UML模型一致性問題。使用UML不能分析此問題,這是因為UML技術(shù)本身無法進行模型驗證�？梢圆捎闷渌问交治黾夹g(shù)協(xié)助分析UML模型的一致性。Event-B就是這樣一種形式化技術(shù),它可以形式化的描述模型,也可以對模型進行形式化驗證。如何將UML技術(shù)和Event-B技術(shù)結(jié)合是本文的重點。要實現(xiàn)兩種技術(shù)的結(jié)合,需要開發(fā)基于Event-B技術(shù)分析UML模型一致性的一整套方法。本文提出了UML模型向Event-B模型轉(zhuǎn)換的規(guī)則和算法設(shè)計方法;設(shè)計了具體的轉(zhuǎn)換算法,并證明了這些算法的規(guī)范性;并且證明了采用這些算法轉(zhuǎn)換得到的Event-B模型和原UML模型的語義一致性,進而證明了它們的等價性;在上述基礎(chǔ)上,本文提出了基于Event-B形式化分析UML模型一致性的方法,并將此方法應(yīng)用于改進一個基于云平臺的應(yīng)用軟件模型。本文的主要內(nèi)容包括如下幾個方面:首先分析了UML技術(shù)半形式化特點帶來的好處與問題,介紹了克服這些問題的研究進展,并提出了可以將Event-B和UML結(jié)合的方法和思路。其次介紹了UML技術(shù),包括UML的元-元模型和元模型以及UML建模的一般過程。還介紹了Event-B技術(shù),包括Event-B模型的元-元模型和元模型以及Event-B技術(shù)的Rodin平臺。接著研究了UML模型向Event-B模型轉(zhuǎn)換的方法,包括轉(zhuǎn)換規(guī)則和實現(xiàn)算法,并且證明了算法的規(guī)范性以及模型轉(zhuǎn)換的等價性。并且在前述提出的模型轉(zhuǎn)換規(guī)則和算法的基礎(chǔ)上,提出了基于Event-B形式化分析UML模型演進一致性的方法,并且通過案例演示了該方法的一般使用過程。最后構(gòu)建了一個基于云平臺的應(yīng)用軟件UML模型,并且將前述提出的基于Event-B形式化分析UML模型演進一致性的方法應(yīng)用于此UML模型的建模過程,呈現(xiàn)了該方法對UML模型的改進。從應(yīng)用結(jié)果看,本文提出的基于Event-B形式化分析UML模型一致性的方法是有效的,可以支持分析、設(shè)計人員的工作,可以在軟件工程的分析和設(shè)計階段作為支撐UML模型質(zhì)量改進的有效方法。
【關(guān)鍵詞】：UML Event-B 類圖 狀態(tài)圖 形式化分析
【學(xué)位授予單位】：江蘇科技大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：TP311.5;TP393.09
【目錄】：

• 摘要3-5
• Abstract5-13
• 第一章 緒論13-21
• 1.1 選題背景13-15
• 1.2 研究現(xiàn)狀和相關(guān)工作15-18
• 1.2.1 形式化方法和技術(shù)15-16
• 1.2.2 UML與其它形式化技術(shù)的結(jié)合16-18
• 1.3 本文主要工作18-19
• 1.4 本文組織結(jié)構(gòu)19-21
• 第二章 UML和Event-B技術(shù)21-35
• 2.1 統(tǒng)一建模語言UML21-24
• 2.1.1 UML元-元模型和元模型21-22
• 2.1.2 UML模型的圖22-23
• 2.1.3 UML建模的一般過程23-24
• 2.2 形式化技術(shù)Event-B24-31
• 2.2.1 Event-B元-元模型和元模型25
• 2.2.2 Event-B模型的構(gòu)件25-28
• 2.2.3 Event-B模型的證明義務(wù)28-30
• 2.2.4 Event-B技術(shù)的Rodin平臺30-31
• 2.3 基于云平臺的軟件模型31-32
• 2.3.1 云平臺對模型的約束31-32
• 2.3.2 模型在云平臺上部署32
• 2.4 本章小結(jié)32-35
• 第三章 UML模型向Event-B模型的轉(zhuǎn)換方法35-51
• 3.1 模型轉(zhuǎn)換過程和形式化35-38
• 3.1.1 模型轉(zhuǎn)換過程的形式化35-36
• 3.1.2 Event-B模型的形式化重定義36-37
• 3.1.3 UML模型的形式化重定義37-38
• 3.2 模型轉(zhuǎn)換的規(guī)則和算法38-46
• 3.2.1 模型轉(zhuǎn)換規(guī)則和算法的設(shè)計過程38
• 3.2.2 模型轉(zhuǎn)換算法實現(xiàn)和規(guī)范性證明38-46
• 3.3 模型轉(zhuǎn)換的等價性46-49
• 3.3.1 模型等價性的假設(shè)46-48
• 3.3.2 模型等價性的證明48-49
• 3.4 本章小結(jié)49-51
• 第四章 基于Event-B的模型演進一致性分析方法51-65
• 4.1 模型演進的一致性51-54
• 4.1.1 Event-B模型的證明義務(wù)之證明51-52
• 4.1.2 Event-B模型演進相關(guān)證明義務(wù)52-54
• 4.2 模型演進一致性分析54-63
• 4.2.1 模型演進一致性分析的過程54
• 4.2.2 模型演進一致性分析的案例54-57
• 4.2.3 案例輸出結(jié)果的分析57-59
• 4.2.4 案例中模型的轉(zhuǎn)換細節(jié)59-62
• 4.2.5 案例中證明的推導(dǎo)方法62-63
• 4.3 本章小結(jié)63-65
• 第五章 應(yīng)用一致性分析方法改進基于云平臺的應(yīng)用軟件模型65-91
• 5.1 建立基于云平臺的應(yīng)用軟件UML模型65-81
• 5.1.1 UML需求模型65-70
• 5.1.2 UML分析模型70-74
• 5.1.3 UML設(shè)計模型74-80
• 5.1.4 UML部署模型80-81
• 5.2 驗證UML模型的一致性81-87
• 5.2.1 演進前UML模型轉(zhuǎn)換81-83
• 5.2.2 演進后UML模型轉(zhuǎn)換83-86
• 5.2.3 Rodin平臺運行結(jié)果86-87
• 5.3 UML模型的改進87-89
• 5.3.1 Event-B模型的改進87-88
• 5.3.2 原UML模型的改進88-89
• 5.4 本章小結(jié)89-91
• 第六章 結(jié)束語91-93
• 6.1 本文總結(jié)91-92
• 6.2 未來工作92-93
• 參考文獻93-97
• 攻讀學(xué)位期間發(fā)表的論文97-99
• 致謝99

  本文關(guān)鍵詞：使用UML和Event-B構(gòu)建基于云平臺的應(yīng)用軟件模型，由筆耕文化傳播整理發(fā)布。

，

本文編號：285888