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

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

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

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

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