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

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

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