活性順序圖規(guī)約到時(shí)間博弈自動(dòng)機(jī)模型的轉(zhuǎn)換方法研究與工具實(shí)現(xiàn).pdf

1、活性順序圖(Live Sequence Chart,LSC)是一種基于場(chǎng)景的形式規(guī)約語(yǔ)言，可以直觀且精確地刻畫系統(tǒng)構(gòu)件間的交互行為，常用于反應(yīng)式系統(tǒng)開發(fā)的需求分析。由于在多個(gè)場(chǎng)景描述間容易產(chǎn)生邏輯矛盾，因此在對(duì)系統(tǒng)模型求精(refinement)前，必須驗(yàn)證確保系統(tǒng)的LSC規(guī)約是一致的。
　　為了有效地判定規(guī)約的一致性，本文主要研究了一種LSC規(guī)約的形式化綜合方法，該方法通過將LSC規(guī)約等價(jià)地轉(zhuǎn)換到時(shí)間博弈自動(dòng)機(jī)(Timed Ga

2、mes Automata)模型，把LSC規(guī)約的一致性檢測(cè)問題轉(zhuǎn)化為時(shí)間博弈解決工具UPPAAL-TIGA中計(jì)算系統(tǒng)獲勝策略的問題。主要研究成果如下：
　　(1)針對(duì)LSC規(guī)約到TGA模型的等價(jià)轉(zhuǎn)換問題，本文研究了LSC中的Instance、Cut、Event和UPPAAL-TIGA工具中TGA的Process、Location、Edge的語(yǔ)義等價(jià)性，給出了從LSC規(guī)約到TGA模型的轉(zhuǎn)換規(guī)則和算法描述。
　　(2)針對(duì)LSC模

3、型文件到UPPAAL-TIGA模型文件的自動(dòng)轉(zhuǎn)換問題，本文分析了模型文件轉(zhuǎn)換處理的具體流程，解析了LSC-editor工具的lsc文件和UPPAAL-TIGA工具的xml文件，給出了LSC和TGA中各語(yǔ)義的數(shù)據(jù)結(jié)構(gòu)，基于：
　　(1)的轉(zhuǎn)換算法，最終實(shí)現(xiàn)了一個(gè)模型轉(zhuǎn)換工具LSC-to-TGA。
　　(2)研究了一個(gè)道岔自動(dòng)控制系統(tǒng)的應(yīng)用實(shí)例，分析了故障容錯(cuò)和超速防護(hù)場(chǎng)景下的系統(tǒng)需求并給出了LSC規(guī)約，使用LSC-to-TGA