UML時序圖模型到UPPAAL時間自動機模型轉(zhuǎn)換方法研究和工具實現(xiàn).pdf

1、實時系統(tǒng)中任何一點錯誤都可能導(dǎo)致災(zāi)難性的后果，故保障實時系統(tǒng)的正確性和可靠性是建立實時系統(tǒng)的首要問題。實時系統(tǒng)建模無疑是一種很好的解決方法，但新的問題是如何保證實時系統(tǒng)模型的正確性和可靠性。這依賴于良好的建模語言和建模工具以及完善的仿真和驗證工具。
　　 UML作，為可視化描述軟件結(jié)構(gòu)和行為的標(biāo)準(zhǔn)語言，已經(jīng)廣泛應(yīng)用在各種軟件開發(fā)中，在實時系統(tǒng)領(lǐng)域也發(fā)揮了越來越重要的作用。目前對實時系統(tǒng)建模主要采用UML序列圖(sequence

2、diagram)與狀態(tài)圖(state diagram)相結(jié)合的方法。而UML時序圖(Timing Diagram)不僅能描述對象間的狀態(tài)轉(zhuǎn)換同時還能完美地刻畫交互次序和交互的時間細(xì)節(jié)。UML時序圖強大靈活的描述能力使其在實時系統(tǒng)建模中必將發(fā)揮越來越重要的作用。
　　 實時系統(tǒng)的高可靠性要求必須對實時系統(tǒng)模型進(jìn)行仿真和驗證。UPPAAL是基于時間自動機的一個實時系統(tǒng)驗證工具，具有強大的仿真和驗證能力。但是UPPAAL只能驗證UPP

3、AAL時間自動機所描述的模型，不能對UML時序圖模型進(jìn)行仿真和驗證。如果能將UML時序圖模型轉(zhuǎn)換為UPPAAL時間自動機模型，那么就可以利用UPPAAL對基于UML時序圖的實時系統(tǒng)進(jìn)行仿真和驗證，且如果能夠開發(fā)出轉(zhuǎn)換工具實現(xiàn)自動轉(zhuǎn)換，就可以使UML時序圖模型直接作為UPPAAL的輸入模型而不需要在UPPAAL中重新建立模型，從而縮短開發(fā)周期，降低出錯概率。
　　 本文分析研究了UML時序圖模型和UPPAAL時間自動機模型，提出了

4、從UML時序圖模型到UPPAAL時間自動機模型的轉(zhuǎn)換策略。針對UML時序圖各元素的語義以及UPPAAL時間自動機的相關(guān)語義，給出了將UML時序圖模型映射到UPPAAL時間自動機模型的設(shè)計方案以及轉(zhuǎn)換算法。
　　 同時，文章給出了基于上述UML時序圖模型到UPPAAL時間自動機模型的轉(zhuǎn)換規(guī)則和轉(zhuǎn)換算法的工具UML_TDMtoUPPAAL_TAM。該工具能夠按照已定義好的轉(zhuǎn)換規(guī)則將UMIL時序圖模型轉(zhuǎn)換到UPPAAL的時間自動機模型