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

【摘要】：軟件工程實(shí)踐中廣泛采用UML(Unified Modeling Language)作為建模語(yǔ)言,UML是一種語(yǔ)言,也可以稱(chēng)其為一種技術(shù)。UML具有半形式化的特點(diǎn),它的形式化部分使其具有嚴(yán)密和精確的特點(diǎn),它的非形式化部分使其易于接受和推廣。UML模型構(gòu)件的結(jié)構(gòu)采用形式化描述,而相應(yīng)的語(yǔ)義采用自然語(yǔ)言描述,這是將UML稱(chēng)為半形式化技術(shù)的原因之一。另外,UML技術(shù)可以對(duì)模型進(jìn)行形式化的描述,但是UML技術(shù)本身沒(méi)有指出如何對(duì)模型進(jìn)行形式化驗(yàn)證,這是將UML稱(chēng)為半形式化技術(shù)的原因之二。事實(shí)上,UML的半形式化特點(diǎn)固然使其易于使用、易于推廣,但是不能支持一些軟件工程的應(yīng)用場(chǎng)景。如果需要分析軟件模型演進(jìn)的一致性,這是單獨(dú)使用UML技術(shù)不能做到的。UML模型在軟件工程的不同階段會(huì)持續(xù)演進(jìn),演進(jìn)過(guò)程中會(huì)引入U(xiǎn)ML模型一致性問(wèn)題。使用UML不能分析此問(wèn)題,這是因?yàn)閁ML技術(shù)本身無(wú)法進(jìn)行模型驗(yàn)證�？梢圆捎闷渌问交治黾夹g(shù)協(xié)助分析UML模型的一致性。Event-B就是這樣一種形式化技術(shù),它可以形式化的描述模型,也可以對(duì)模型進(jìn)行形式化驗(yàn)證。如何將UML技術(shù)和Event-B技術(shù)結(jié)合是本文的重點(diǎn)。要實(shí)現(xiàn)兩種技術(shù)的結(jié)合,需要開(kāi)發(fā)基于Event-B技術(shù)分析UML模型一致性的一整套方法。本文提出了UML模型向Event-B模型轉(zhuǎn)換的規(guī)則和算法設(shè)計(jì)方法;設(shè)計(jì)了具體的轉(zhuǎn)換算法,并證明了這些算法的規(guī)范性;并且證明了采用這些算法轉(zhuǎn)換得到的Event-B模型和原UML模型的語(yǔ)義一致性,進(jìn)而證明了它們的等價(jià)性;在上述基礎(chǔ)上,本文提出了基于Event-B形式化分析UML模型一致性的方法,并將此方法應(yīng)用于改進(jìn)一個(gè)基于云平臺(tái)的應(yīng)用軟件模型。本文的主要內(nèi)容包括如下幾個(gè)方面:首先分析了UML技術(shù)半形式化特點(diǎn)帶來(lái)的好處與問(wèn)題,介紹了克服這些問(wèn)題的研究進(jìn)展,并提出了可以將Event-B和UML結(jié)合的方法和思路。其次介紹了UML技術(shù),包括UML的元-元模型和元模型以及UML建模的一般過(guò)程。還介紹了Event-B技術(shù),包括Event-B模型的元-元模型和元模型以及Event-B技術(shù)的Rodin平臺(tái)。接著研究了UML模型向Event-B模型轉(zhuǎn)換的方法,包括轉(zhuǎn)換規(guī)則和實(shí)現(xiàn)算法,并且證明了算法的規(guī)范性以及模型轉(zhuǎn)換的等價(jià)性。并且在前述提出的模型轉(zhuǎn)換規(guī)則和算法的基礎(chǔ)上,提出了基于Event-B形式化分析UML模型演進(jìn)一致性的方法,并且通過(guò)案例演示了該方法的一般使用過(guò)程。最后構(gòu)建了一個(gè)基于云平臺(tái)的應(yīng)用軟件UML模型,并且將前述提出的基于Event-B形式化分析UML模型演進(jìn)一致性的方法應(yīng)用于此UML模型的建模過(guò)程,呈現(xiàn)了該方法對(duì)UML模型的改進(jìn)。從應(yīng)用結(jié)果看,本文提出的基于Event-B形式化分析UML模型一致性的方法是有效的,可以支持分析、設(shè)計(jì)人員的工作,可以在軟件工程的分析和設(shè)計(jì)階段作為支撐UML模型質(zhì)量改進(jìn)的有效方法。
【關(guān)鍵詞】：UML Event-B 類(lèi)圖 狀態(tài)圖 形式化分析
【學(xué)位授予單位】：江蘇科技大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2016
【分類(lèi)號(hào)】：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)一建模語(yǔ)言UML21-24
• 2.1.1 UML元-元模型和元模型21-22
• 2.1.2 UML模型的圖22-23
• 2.1.3 UML建模的一般過(guò)程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平臺(tái)30-31
• 2.3 基于云平臺(tái)的軟件模型31-32
• 2.3.1 云平臺(tái)對(duì)模型的約束31-32
• 2.3.2 模型在云平臺(tái)上部署32
• 2.4 本章小結(jié)32-35
• 第三章 UML模型向Event-B模型的轉(zhuǎn)換方法35-51
• 3.1 模型轉(zhuǎn)換過(guò)程和形式化35-38
• 3.1.1 模型轉(zhuǎn)換過(guò)程的形式化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è)計(jì)過(guò)程38
• 3.2.2 模型轉(zhuǎn)換算法實(shí)現(xiàn)和規(guī)范性證明38-46
• 3.3 模型轉(zhuǎn)換的等價(jià)性46-49
• 3.3.1 模型等價(jià)性的假設(shè)46-48
• 3.3.2 模型等價(jià)性的證明48-49
• 3.4 本章小結(jié)49-51
• 第四章 基于Event-B的模型演進(jìn)一致性分析方法51-65
• 4.1 模型演進(jìn)的一致性51-54
• 4.1.1 Event-B模型的證明義務(wù)之證明51-52
• 4.1.2 Event-B模型演進(jìn)相關(guān)證明義務(wù)52-54
• 4.2 模型演進(jìn)一致性分析54-63
• 4.2.1 模型演進(jìn)一致性分析的過(guò)程54
• 4.2.2 模型演進(jìn)一致性分析的案例54-57
• 4.2.3 案例輸出結(jié)果的分析57-59
• 4.2.4 案例中模型的轉(zhuǎn)換細(xì)節(jié)59-62
• 4.2.5 案例中證明的推導(dǎo)方法62-63
• 4.3 本章小結(jié)63-65
• 第五章 應(yīng)用一致性分析方法改進(jìn)基于云平臺(tái)的應(yīng)用軟件模型65-91
• 5.1 建立基于云平臺(tái)的應(yīng)用軟件UML模型65-81
• 5.1.1 UML需求模型65-70
• 5.1.2 UML分析模型70-74
• 5.1.3 UML設(shè)計(jì)模型74-80
• 5.1.4 UML部署模型80-81
• 5.2 驗(yàn)證UML模型的一致性81-87
• 5.2.1 演進(jìn)前UML模型轉(zhuǎn)換81-83
• 5.2.2 演進(jìn)后UML模型轉(zhuǎn)換83-86
• 5.2.3 Rodin平臺(tái)運(yùn)行結(jié)果86-87
• 5.3 UML模型的改進(jìn)87-89
• 5.3.1 Event-B模型的改進(jìn)87-88
• 5.3.2 原UML模型的改進(jìn)88-89
• 5.4 本章小結(jié)89-91
• 第六章 結(jié)束語(yǔ)91-93
• 6.1 本文總結(jié)91-92
• 6.2 未來(lái)工作92-93
• 參考文獻(xiàn)93-97
• 攻讀學(xué)位期間發(fā)表的論文97-99
• 致謝99

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

，

本文編號(hào)：285888