基于UML時序圖的系統(tǒng)形式模型自動生成研究.pdf

1、分類號：密級：UDC：學(xué)號：碩士學(xué)位論文基于基于UML時序圖的系統(tǒng)形式模型自動生成研究時序圖的系統(tǒng)形式模型自動生成研究ResearchonAutomaticGenerationMethodofFmalSystemModelBasedonUMLSequenceDiagram學(xué)位類別：工程碩士作者姓名：王雪嬌學(xué)科專業(yè)：計算機技術(shù)研究方向：模型檢測指導(dǎo)教師：張水平教授2016年05月30日江西理工大學(xué)碩士學(xué)位論文摘要I摘要伴著全球信息化飛速發(fā)

2、展的步伐，系統(tǒng)形式建模在學(xué)術(shù)界和工業(yè)界的應(yīng)用越來越普遍，其中系統(tǒng)形式建模方法成為構(gòu)建安全系統(tǒng)的重要保障之一。統(tǒng)一建模語言是一種能夠直觀的描述系統(tǒng)模型中行為的可視化語言。雖然統(tǒng)一建模語言在軟件設(shè)計、開發(fā)和測試過程中均起著至關(guān)重要的作用，但是由于統(tǒng)一建模語言的可視化圖形缺少確切的語義描述。對于設(shè)計規(guī)范要求苛刻的系統(tǒng)，進行模型驗證的時候難度比較大，給設(shè)計人員帶來了更多的挑戰(zhàn)。系統(tǒng)形式模型的自動生成與實現(xiàn)成為亟待解決的熱點問題，鑒于此，本文的創(chuàng)

3、新點及主要工作分為如下三個部分：（1）依照系統(tǒng)場景需求的系統(tǒng)模型給出語義描述。系統(tǒng)模型具有Kripke結(jié)構(gòu)，并給出系統(tǒng)形式模型的語義描述。對系統(tǒng)模型的語義描述進行擴展，分別給出半形式化描述系統(tǒng)模型UML時序圖和有限狀態(tài)機的語義描述。通過UML時序圖內(nèi)某一對象的語義描述，引出執(zhí)行確定有限狀態(tài)機（ExecutionDeterministicFiniteStateMachine，EDFSM）的形式描述。（2）在UML2.0時序圖已存在片段的基

4、礎(chǔ)上，結(jié)合Alt和Neg兩種片段提出的一種新的適用于特殊系統(tǒng)場景下的Stop片段，Stop片段用于必要情況下終止系統(tǒng)模型中的事件繼續(xù)執(zhí)行。根據(jù)UML時序圖和執(zhí)行確定有限狀態(tài)機的語義描述，提出標(biāo)準(zhǔn)UML時序圖及帶有單一片段的UML時序圖中的某一對象到執(zhí)行確定有限狀態(tài)機的算法生成規(guī)則。（3）結(jié)合UML模型的語義描述和FSP（FiniteStateProcess，F(xiàn)SP）進程代數(shù)符號表示，介紹深度優(yōu)先搜索算法并對其進行改進。基于改進深度優(yōu)先搜

5、索算法設(shè)計并實現(xiàn)FSP進程代數(shù)模型的自動輸出，運用LTSA（LabeledTransitionSystemAnalysis）工具達到系統(tǒng)形式模型自動生成的目的。本文選用基本考生網(wǎng)上報名系統(tǒng)作為實例，實現(xiàn)基于改進深度優(yōu)先搜索算法的系統(tǒng)形式模型的自動生成，運用MCA_ETGBA模型檢測工具，驗證了系統(tǒng)形式模型生成算法的可行性。系統(tǒng)形式模型的自動生成解決了半形式化建模缺乏語義描述的不足，為規(guī)范要求高的系統(tǒng)提供了有效途徑。關(guān)鍵字：UML時序圖；