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

1、分類號(hào)：密級(jí)：UDC：學(xué)號(hào)：碩士學(xué)位論文基于基于UML時(shí)序圖的系統(tǒng)形式模型自動(dòng)生成研究時(shí)序圖的系統(tǒng)形式模型自動(dòng)生成研究ResearchonAutomaticGenerationMethodofFmalSystemModelBasedonUMLSequenceDiagram學(xué)位類別：工程碩士作者姓名：王雪嬌學(xué)科專業(yè)：計(jì)算機(jī)技術(shù)研究方向：模型檢測(cè)指導(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è)計(jì)、開發(fā)和測(cè)試過程中均起著至關(guān)重要的作用，但是由于統(tǒng)一建模語言的可視化圖形缺少確切的語義描述。對(duì)于設(shè)計(jì)規(guī)范要求苛刻的系統(tǒng)，進(jìn)行模型驗(yàn)證的時(shí)候難度比較大，給設(shè)計(jì)人員帶來了更多的挑戰(zhàn)。系統(tǒng)形式模型的自動(dòng)生成與實(shí)現(xiàn)成為亟待解決的熱點(diǎn)問題，鑒于此，本文的創(chuàng)

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

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

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