本文關(guān)鍵詞：基于抽象狀態(tài)自動機和π演算的UML動態(tài)語義研究

  更多相關(guān)文章： 統(tǒng)一建模語言 形式化方法 抽象狀態(tài)自動機 π演算

【摘要】：隨著集成電路產(chǎn)業(yè)的發(fā)展,計算機的硬件性能在近二十年內(nèi)迅速提高。硬件以及計算機應(yīng)用領(lǐng)域的不斷擴展,使得人們對軟件技術(shù)提出更多更高的要求。如何改進軟件的質(zhì)量,提高開發(fā)效率成為軟件產(chǎn)業(yè)的重要研究工作。 自90年代面向?qū)ο蟮母拍钐岢鲆詠?由于其可視化、可重用、貼近需求等優(yōu)點獲得了廣泛認(rèn)可,模型也成為溝通用戶需求和最終實現(xiàn)的重要橋梁。UML統(tǒng)一并擴展了眾多的建模語言,采用豐富的圖形作為建模元素。UML的強可讀性適用于軟件開發(fā)的初級階段,但由于缺乏精確的語義元素,所以在分析、設(shè)計和實現(xiàn)時難以建立完整、無二義性的模型,也缺乏必要的精化和驗證工具。 形式化方法基于嚴(yán)格的數(shù)學(xué)和邏輯技術(shù),可以對軟件系統(tǒng)進行規(guī)約、設(shè)計和驗證,提高安全性與可靠性。形式化的目的是在系統(tǒng)開發(fā)的早期階段發(fā)現(xiàn)并消除不一致、不明確或不完整現(xiàn)象。邏輯精確的語義使開發(fā)者與用戶形成對需求的一致理解,消除了模糊、不一致；語義的驗證自動化,提高了系統(tǒng)的可靠性和效率。然而,由于對設(shè)計者提出了數(shù)學(xué)和邏輯的要求,所以形式化方法在應(yīng)用領(lǐng)域上存在局限性,很難普及。 理想的軟件開發(fā)是對可視化建模技術(shù)和形式化方法的結(jié)合。本文研究UML的動態(tài)語義,在保證易讀性的基礎(chǔ)上,增添必要的語義元素,保證模型的無歧義和可驗證性,主要研究成果如下： (1)使用抽象狀態(tài)自動機對UML活動圖進行語義規(guī)約。首先定義了活動圖的靜態(tài)語義,分別對動作節(jié)點(原子節(jié)點)、分支節(jié)點、并發(fā)節(jié)點和活動節(jié)點分別給出了語義規(guī)約,并遞歸產(chǎn)生了抽象自動機活動圖的規(guī)約。隨后通過規(guī)則對活動圖的動態(tài)行為,如分支、匯合以及觸發(fā)捕獲事件等行為給出了相應(yīng)的語義規(guī)約。在工作流的循環(huán)鑒別器模型中,采用這種方法更為清晰地規(guī)約了語義。 (2)使用抽象狀態(tài)自動機對UML狀態(tài)圖進行語義規(guī)約。作為UML中描述行為的重要圖形,狀態(tài)圖涵蓋了對象在其生命周期內(nèi)的全部轉(zhuǎn)換形態(tài)。本文首先給出了狀態(tài)圖的靜態(tài)語義,規(guī)約了遷移及狀態(tài)的語義,然后在UML狀態(tài)圖的基礎(chǔ)上,給出了擴展的抽象狀態(tài)自動機模型,提出了基于擴展模型的狀態(tài)圖行為語義。 (3)使用抽象狀態(tài)自動機對UML順序圖進行語義規(guī)約。定義了順序圖中消息和對象的語義規(guī)約,隨后,針對圖形中消息傳送條件不明確,時序不清晰的問題,為順序圖的消息傳送行為進行了規(guī)約。 根據(jù)前面給出的狀態(tài)圖和順序圖的語義規(guī)約,對電梯實例的UML動態(tài)模型進行了語義歸約和規(guī)則驗證,消除了在遞歸調(diào)用中可能出現(xiàn)的死鎖和不一致。 (4)提出了UML動態(tài)圖的π增量精化體系。先給出了π演算對UML動態(tài)圖的語義規(guī)約,將動態(tài)圖中的各個元素分別映射到π演算的進程和通道；然后規(guī)約了動態(tài)圖的各種動態(tài)要素,如狀態(tài)的不同轉(zhuǎn)換模式、各種消息的傳送行為等的語義規(guī)約。最后利用弱互模擬關(guān)系,定義了順序圖和狀態(tài)圖的行為等價性判別標(biāo)準(zhǔn)；提出了最大弱互模擬集、替換規(guī)則,并藉此給出了在精化模型上進行增量一致性檢測的方法,電話系統(tǒng)的實例表明,這種方法大大提高了驗證的效率。
【關(guān)鍵詞】：統(tǒng)一建模語言 形式化方法 抽象狀態(tài)自動機 π演算
【學(xué)位授予單位】：華東理工大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2015
【分類號】：TP311.5
【目錄】：

• 摘要5-7
• Abstract7-12
• 圖表目錄12-14
• 第1章 緒論14-27
• 1.1 研究背景14-16
• 1.2 面向?qū)ο蠓椒▽W(xué)16-21
• 1.2.1 發(fā)展歷程16-18
• 1.2.2 主要的面向?qū)ο蠓椒?/span>18-21
• 1.3 形式化方法21-24
• 1.3.1 軟件規(guī)約的主要技術(shù)21-22
• 1.3.2 形式化方法與半形式化方法的優(yōu)缺點22-24
• 1.3.3 形式化方法與半形式化方法的結(jié)合24
• 1.4 課題主要研究內(nèi)容24-25
• 1.5 論文組織結(jié)構(gòu)25-27
• 第2章 UML形式化規(guī)格說明研究動態(tài)27-37
• 2.1 UML建模27-32
• 2.1.1 什么是模型27-28
• 2.1.2 為什么要建模28
• 2.1.3 UML的發(fā)展史28-30
• 2.1.4 UML的組成30
• 2.1.5 UML的現(xiàn)狀及其優(yōu)缺點30-32
• 2.1.6 UML模型形式化的要求32
• 2.2 相關(guān)的研究工作32-35
• 2.2.1 基于Z的UML形式化33
• 2.2.2 基于B的UML形式化33-34
• 2.2.3 基于VDM的UML形式化34
• 2.2.4 基于邏輯的UML形式化34-35
• 2.2.5 基于網(wǎng)絡(luò)的UML形式化35
• 2.3 現(xiàn)有工作與本課題的對比35-36
• 2.4 本章小結(jié)36-37
• 第3章 抽象狀態(tài)自動機和π演算37-48
• 3.1 抽象狀態(tài)自動機方法37-43
• 3.1.1 抽象狀態(tài)自動機概述37-38
• 3.1.2 抽象狀態(tài)自動機方法學(xué)的優(yōu)點38-39
• 3.1.3 抽象狀態(tài)自動機的定義39-43
• 3.2 π演算43-47
• 3.2.1 π演算概述43-44
• 3.2.2 演算的語法44-45
• 3.2.3 結(jié)構(gòu)同余性(Structural Congruence)45-46
• 3.2.4 π演算的行為語義46-47
• 3.3 本章小結(jié)47-48
• 第4章 基于抽象狀態(tài)自動機的UML動態(tài)圖語義規(guī)約48-80
• 4.1 UML語義結(jié)構(gòu)48-49
• 4.2 活動圖的抽象狀態(tài)自動機語義49-60
• 4.2.1 UML活動圖概述49-50
• 4.2.2 抽象狀態(tài)自動機活動圖的基本定義50-52
• 4.2.3 抽象狀態(tài)自動機活動圖的語義52-56
• 4.2.4 實例應(yīng)用56-60
• 4.3 狀態(tài)圖的抽象狀態(tài)自動機語義60-68
• 4.3.1 狀態(tài)圖的基本元素60-61
• 4.3.2 狀態(tài)圖的靜態(tài)語義元素61-63
• 4.3.3 狀態(tài)機的動態(tài)語義規(guī)約63-68
• 4.4 順序圖的抽象狀態(tài)自動機語義68-74
• 4.4.1 順序圖形式化的意義68-69
• 4.4.2 順序圖的抽象狀態(tài)自動機模型語義元素69-70
• 4.4.3 順序圖的抽象狀態(tài)自動機模型語義規(guī)則70-71
• 4.4.4 模型的規(guī)約和驗證71
• 4.4.5 順序圖抽象狀態(tài)自動機模型實例71-74
• 4.5 順序圖與狀態(tài)圖的一致性驗證實例74-79
• 4.5.1 電梯實例74-76
• 4.5.2 語義規(guī)約76-77
• 4.5.3 規(guī)則驗證77
• 4.5.4 分析與層次樹模型77-79
• 4.5.5 結(jié)論79
• 4.6 本章小結(jié)79-80
• 第5章 基于π演算的UML動態(tài)圖增量精化驗證80-101
• 5.1 模型精化80
• 5.2 為什么采用π演算作為精化工具80-81
• 5.3 UML動態(tài)子圖的π語義模型81-89
• 5.3.1 狀態(tài)圖的π語義81-85
• 5.3.2 順序圖的π語義85-89
• 5.4 互模擬關(guān)系89-94
• 5.4.1 行為等價性89
• 5.4.2 圖形中的互模擬89-91
• 5.4.3 強互模擬關(guān)系91-92
• 5.4.4 弱互模擬關(guān)系92-94
• 5.5 增量精化體系94-99
• 5.5.1 電話系統(tǒng)實例94-98
• 5.5.2 等價性分析98-99
• 5.5.3 結(jié)論99
• 5.6 本章小結(jié)99-101
• 第6章 結(jié)束語101-103
• 6.1 本文的主要研究成果101-102
• 6.2 UML動態(tài)圖形式化語義的研究展望102-103
• 參考文獻103-111
• 致謝111-112
• 攻讀博士學(xué)位期間完成論文及出版著作112

【參考文獻】

中國期刊全文數(shù)據(jù)庫 前2條

1 郭峰;姚淑珍;;基于Petri網(wǎng)的UML狀態(tài)圖的形式化模型[J];北京航空航天大學(xué)學(xué)報;2007年02期

2 劉暉,李明祿;基于抽象狀態(tài)機的網(wǎng)格系統(tǒng)設(shè)計和分析[J];電子學(xué)報;2003年S1期

，

本文編號：1101460