基于圖轉(zhuǎn)換的關(guān)聯(lián)屬性規(guī)約模型檢測(cè)及其支撐平臺(tái)研究.pdf

1、圖轉(zhuǎn)換系統(tǒng)廣泛應(yīng)用在軟件建模和分析階段，現(xiàn)有的圖轉(zhuǎn)換系統(tǒng)通常采用命題式時(shí)序邏輯(propositional temporal logic)表達(dá)待驗(yàn)證規(guī)約，但是該邏輯無法直接表達(dá)建模實(shí)體隨時(shí)間演化的關(guān)聯(lián)屬性，提出一種輕量級(jí)可支持通用圖轉(zhuǎn)換系統(tǒng)中關(guān)聯(lián)屬性規(guī)約的驗(yàn)證方法，通過引入標(biāo)記節(jié)點(diǎn)及相關(guān)屬性，將包含相應(yīng)關(guān)聯(lián)屬性的規(guī)約公式等價(jià)轉(zhuǎn)換為常規(guī)命題式時(shí)序邏輯，從而可以間接支持該類型規(guī)約的驗(yàn)證。以流行的對(duì)象式圖轉(zhuǎn)換模型檢測(cè)工具 GROOVE為平臺(tái)，

2、結(jié)合啟發(fā)案例，通過實(shí)驗(yàn)驗(yàn)證了所提出方法的可行性。
　　由于引入標(biāo)記節(jié)點(diǎn)及屬性來完成關(guān)聯(lián)屬性規(guī)約的驗(yàn)證會(huì)帶來額外的狀態(tài)數(shù)，加劇狀態(tài)空間爆炸問題，增加系統(tǒng)開銷，應(yīng)用對(duì)稱化簡(jiǎn)以及層次化技術(shù)，優(yōu)化模型結(jié)構(gòu)，減少狀態(tài)數(shù)，來節(jié)約系統(tǒng)的時(shí)間開銷。結(jié)合具體實(shí)例，通過實(shí)驗(yàn)對(duì)比，展示出對(duì)稱化簡(jiǎn)以及圖形層次化技術(shù)在圖轉(zhuǎn)換系統(tǒng)的模型檢測(cè)中減少狀態(tài)空間的有效性。
　　此外，為提供更好的可用性，采用圖形化編輯框架GEF(Graphic Editing