《基於多主體認知邏輯模型檢測的Web服務組合驗證》是依託華僑大學，由駱翔宇擔任項目負責人的面上項目。
基本介紹
- 中文名：基於多主體認知邏輯模型檢測的Web服務組合驗證
- 項目類別：面上項目
- 項目負責人：駱翔宇
- 依託單位：華僑大學
項目摘要,結題摘要,
項目摘要
面向服務的體系架構將成為最主流的軟體工程實踐方法之一。由於服務及其協同的動態性、開放多變的網際網路運行環境、以及松耦合的服務開發模式，使得服務的正確性、可靠性、安全性等可信性質難以得到保證。針對Web服務組合可信性質的形式化驗證需求，擬開展基於多主體系統的Web服務組合形式化建模和自動模型檢測技術的研發。提出新的多主體約束自動機模型，將服務抽象為主體自動機，刻畫主體互動接口、主體協同機制以及組合系統的操作行為，從而將Web服務組合抽象為多主體系統。在此模型上提出新的多主體認知邏輯，融合時態、命題動態邏輯、數據流邏輯和動態認知邏輯，可對主體認知狀態進行表示和推理。通過對該多主體認知邏輯的基礎理論和關鍵技術的研究，提出基於多主體約束自動機的模型檢測算法。為了大幅緩解模型檢測技術的狀態爆炸問題，重點考慮基於符號計算技術開發相關模型檢測工具，從而在Web服務形式化建模與驗證領域獲得實質進展。
結題摘要
本項目針對Web服務組合等分散式系統的可信性質的形式化驗證需求，開展了基於多智慧型體系統（MAS）模型檢測的Web服務組合的形式建模與驗證的理論、方法和工具的研究與開發。總體看，本團隊已按計畫完成大部分研究內容。 我們首先豐富了MAS常用的時態認知邏輯，其認知部分完整支持知識、群體知識、分布知識、公共知識、信念、願望和意圖等認知模態詞的表示和推理；時態部分支持即可定性又可定量描述的實時時態邏輯RTCTL*，增強了時態表達能力；我們還將智慧型體聯合邏輯與上述時態、認知邏輯融合起來，極大的增強了所提出邏輯的表達能力，拓寬了套用領域。 驗證工具研發方面，完成了RTCTL*符號化模型檢測的理論研究和工具MCTK的開發，結合前期實現的認知邏輯模型檢測算法，我們實際實現了RTCTL*K的符號化模型檢測工具。我們還提出了RTCTL*以及認知邏輯的圖狀反例表示和生成方法，提高了反例的簡潔性和易讀性。另外，我們還開發了一個帶線性不等式和無解釋函式符號的無量詞一階邏輯證明器Folp，可作為該一階邏輯公式的SMT求解器，以及Craig插值生成器。這對提高模型檢測技術的驗證效率是個有效的辦法。 對於Web服務的模型檢測，我們提出了將多智慧型體系統的謂詞抽象驗證套用於web服務組合抽象驗證與精化的方法。其中採用的驗證平台是我們的MCTK。這一方法可將包含眾多數據的web服務的狀態空間規約到可接受的程度，大大提高驗證效率。
