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

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

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

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