基于狀態(tài)約簡的模型一致性驗證的研究及應(yīng)用.pdf

1、隨著計算機軟件模型日趨復(fù)雜以及大規(guī)模與并發(fā)系統(tǒng)的應(yīng)用,如何保證系統(tǒng)模型的正確性、一致性成為當(dāng)前研究的熱點。本課題以面向任務(wù)的系統(tǒng)集成設(shè)計方法為研究背景,該方法的建模特點是模型規(guī)模較大、結(jié)構(gòu)復(fù)雜并且允許多人協(xié)同設(shè)計,因此有可能產(chǎn)生模型不一致現(xiàn)象。近年來,許多學(xué)者研究了使用形式化方法描述系統(tǒng)模型,并使用模型檢測技術(shù)驗證模型一致性的方法。然而現(xiàn)有方法仍然存在一些不足,比如:沒有對類圖、時序圖和狀態(tài)圖之間由于模型重疊產(chǎn)生的一致性做出合適定義;在

2、對復(fù)雜模型一致性的驗證過程中,由于沒有考慮冗余元素致使驗證效率較低;現(xiàn)有將UML模型轉(zhuǎn)換為PROMELA模型的方法無法驗證某些視圖、模型結(jié)構(gòu)的一致性。針對上述不足,本文所做工作如下:
　　首先,綜合考慮 UML類圖、時序圖、狀態(tài)圖的元素,結(jié)合模型的動態(tài)行為特征對行為一致性給出了新的定義;分析狀態(tài)圖中與一致性無關(guān)的冗余狀態(tài)和遷移的特征,提出了針對無觸發(fā)遷移、不可達狀態(tài)、偽狀態(tài)和復(fù)合狀態(tài)的約簡規(guī)則和狀態(tài)圖約簡算法,實驗表明該算法有效地

3、降低了驗證模型的復(fù)雜程度,減少了驗證過程中狀態(tài)和遷移數(shù)量,提高了驗證效率。
　　接著,針對當(dāng)前的模型轉(zhuǎn)換方法不完全支持時序圖多條交互、時序圖和狀態(tài)圖復(fù)雜結(jié)構(gòu)以及行為一致性驗證的不足,通過分析PROMELA的建模特征,提出了基于進程同步的UML模型到PROMELA轉(zhuǎn)換方法,并設(shè)計了相應(yīng)的模型轉(zhuǎn)換算法。實驗結(jié)果表明,該方法能夠有效驗證類圖、時序圖和狀態(tài)圖之間的行為一致性,并且支持類圖,時序圖多條交互、組合片段,狀態(tài)圖復(fù)雜結(jié)構(gòu)。通過與現(xiàn)