《基於高效I/O模型檢測的大規模Web服務驗證研究》是依託電子科技大學,由吳立軍擔任醒目負責人的面上項目。
基本介紹
- 中文名：基於高效I/O模型檢測的大規模Web服務驗證研究
- 依託單位：電子科技大學
- 項目類別：面上項目
- 項目負責人：吳立軍
項目摘要,結題摘要,
項目摘要
大規模Web服務是Internet最廣泛最重要的套用之一，對大規模Web服務的驗證是計算機安全方面一個非常重要的新研究領域。本項目的研究目標是研究大規模系統高效I/O模型檢測技術，為大規模Web 服務的安全驗證提供高效的途徑。具體內容主要包括以下幾方面：(1) 提出新的時態認知邏輯體系，這種邏輯體系能更加準確地描述大規模Web服務的安全屬性；(2) 研究大規模Web服務的模型化方法；(3) 研究動態和靜態記憶體管理技術, 將深度優先和寬度優先搜尋技術從記憶體擴展到外存, 提出高效I/O模型檢測技術，解決因狀態空間爆炸和記憶體不足導致的模型檢測無法進行的問題，以此為基礎，形成大規模Web服務安全驗證的方法和技術；(4) 以上述方法和技術為基礎，通過擴展SPIN等著名模型檢測工具,設計和實現大規模Web服務驗證工具,並對具有代表性的大規模Web服務系統進行安全性驗證。
結題摘要
大規模Web服務是Internet最廣泛最重要的套用之一，對大規模Web服務的驗證是計算機安全方面一個非常重要的新研究領域。 本項目的研究內容主要包括以下幾方面：(1) 提出新的時態認知邏輯體系，這種邏輯體系能更加準確地描述大規模Web服務的安全屬性；(2) 研究大規模Web服務的模型化方法；(3) 研究動態和靜態記憶體管理技術, 提出高效I/O模型檢測技術 (4)設計和實現大規模Web服務驗證工具。 該項目已取得了較好的成果，共發表論文18篇，其中頂級期刊IEEE Transactions on Software Engineering (TSE)上1篇；頂級期刊Artificial Intelligence上2篇；頂級期刊IEEE Transactions on Computers上2篇；著名期刊IEEE Transactions on Very Large Scale Integration Systems、Journal of Artificial Intelligence Research和IEEE Transactions on Cybernetics上5篇；頂級會議AAAI和IJCAI上3篇。具體如下：（1）提出層次多智慧型體系統中完備可靠的一階知識、信念和肯定性邏輯系統，為大規模Web服務的安全屬性描述提供了更加準確的方法。（2）提出了一種大規模系統I/O高效模型檢測技術。我們算法的速度大約是國際上最好的三個算法DAC, MAP和 IDDFS的三倍。為Web服務的驗證提供了更加高效的方法，相關成果發表在著名刊物《IEEE Transactions on Very Large Scale Integration Systems》等期刊上。（3）首次提出基於I/O模型檢測技術查找所有反例(或多反例)的高效方法。這種方法對模型檢測技術以及大規模Web服務驗證等方面都有重要的理論價值和套用前景。相關成果發表在頂級刊物《IEEE Transactions on Software Engineering》等期刊上。（4）在大規模Web服務驗證的其他算法方面，我們已經提出了多種快速的搜尋算法， 相關成果發表在頂級期刊《Artificial Intelligence》 等刊物上。
