《基於模型檢測的軟體動態演化一致性保障機制研究》是依託南京航空航天大學，由周宇擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：基於模型檢測的軟體動態演化一致性保障機制研究
- 項目類別：青年科學基金項目
- 項目負責人：周宇
- 依託單位：南京航空航天大學
項目摘要,結題摘要,
項目摘要
演化一致性保障技術是開放環境下軟體演化研究的熱點問題。傳統的模型檢測方法著力於通用的模型內部狀態的表達和處理方式，由於狀態空間爆炸問題，難以直接利用該技術來驗證較大規模軟體一致性。本課題擬針對此問題展開研究，主要包括：1，研究開放環境下軟體演化的形態、行為特徵，提煉一種新的以體系結構為中心的領域建模機制2，根據領域模型特徵，針對性地設計內部狀態生成算法，避免那些本質相同但在通用模型檢測工具中認為是不同的狀態產生；3，研究一致性規約屬性的結構特徵，將全局屬性轉換為一系列等價局部屬性，利用組合推理技術，並行化分別驗證。通過以上研究，在待驗證系統的規模和驗證效率等方面取得進展與突破，為軟體動態演化正確有效地實施提供技術保障。
結題摘要
動態演化能力是開放環境下軟體形態的一種重要特徵，動態演化的關鍵問題之一就是演化的一致性問題，獲得了廣泛的關注，有大量的工作從不同角度對此問題進行研究。本項目主要研究了如何引入模型檢測技術，保障軟體演化模型與規約的一致性，並針對驗證過程的狀態空間爆炸問題，採用多種方式，如對稱化簡技術、組合推理技術等來進一步提高待驗證系統的規模和效率。本項目取得主要成果如下：針對開放環境下軟體系統的層次式結構特徵，提出用層次式時間自動機建模，給出嚴格的操作語義模型，該項成果發表在計算機科學技術學報(JCST)上；提出了一個層次平展化算法，並用互模擬理論證明該算法的正確性，將層次式時間自動機模型等價轉化為平展化時間自動機模型，從而可以用現有模型檢測工具如UPPAAL等對之進行形式化的驗證，該項相關工作發表在軟體學報，中國科學（信息科學），國際軟體過程會議(ICSSP)等，平展化算法獲得了國家發明專利；在屬性規約驗證方面，針對圖文法建模方式不能針對反應式規約的相關屬性進行描述驗證，提出了一種輕量級的針對反應式規約的相關屬性驗證的方法，並且根據套用領域特徵，採用對稱化簡、組合驗證等技術進一步壓縮狀態空間，緩解了狀態爆炸問題，相關工作發表在計算機前沿(FCS)上；開發的基於ECLIPSE富客戶端(rich client)的原型系統，一個支持開放系統動態演化的中間件平台，相關論文發表在Computing期刊上；此外，本項目還做了一些拓展性研究，例如針對開放環境中的不確定性建模問題，開放系統中的協定驗證問題，軟體的缺陷前饋預測問題等，相關工作發表在ICWS, ICSME, ICA3PP, 中國科學(信息科學)等會議或期刊上。本項目系統地針對了軟體動態演化過程中的一致性驗證等問題展開研究，在待驗證系統的規模和效率上取得了一定的進展和突破，取得了較為豐碩的成果，較好地完成了項目計畫目標。
