《普適計算中可信服務構建的形式化分析與驗證》是依託上海交通大學，由黃林鵬擔任項目負責人的面上項目。
基本介紹
- 中文名：普適計算中可信服務構建的形式化分析與驗證
- 項目類別：面上項目
- 項目負責人：黃林鵬
- 依託單位：上海交通大學
項目摘要,結題摘要,
項目摘要
普適計算通常是在一個異構、移動、開放的環境下進行，不僅需要考慮系統內部各個組件之間的協調合作還要關注系統與外部環境的互動，傳統的服務計算理論和技術很難直接有效套用。本項目擬針對普適環境下服務計算的可信保障問題，提出一種描述普適環境下服務特徵的形式化語言，給出面向普適套用的類型和效果系統以刻畫和抽取構建的普適服務的動態行為，並把它們轉換為服務流程有限狀態機；設計基於抽象狀態機的服務行為驗證模型，根據上述服務流程有限狀態機和用戶給定的規約策略，自動驗證服務的動態運行行為是否符合用戶所給定的規約策略和相關的性質，並推導出服務行為的失效點與可恢復點的映射轉換機制，為移動環境下普適服務的快速重建提供理論指導並避免傳統基於有限狀態機分析中可能出現的狀態爆炸問題；最後基於OSGi構建普適套用場景，對提出的理論模型和技術方案進行驗證。
結題摘要
本項目以普適環境下的可信服務構建為研究對象，以建立符合用戶規約和行為策略的服務編排模型為目標，使用形式化分析和驗證方法確保普適環境下服務計算的可信性，搭建基於OSGi 的普適計算平台和套用場景以驗證課題組提出的理論和方法的可行性和有效性，取得成果如下： （1）普適環境下服務構件特徵的建模研究 普適環境下計算的複雜性和可變性使普適服務的構件特徵和傳統服務的構件特徵相比有較大的不同，因而需要對普適服務構件的特徵進行建模，課題組研究了普適環境下服務構件的主要特性，包括普適服務接口類型、服務行為表達、服務行為規約策略和服務感知接口等，分析了普適計算環境下服務構件的互動方式和組合模式，提出了一種面向普適環境的服務模型，其具有較好的自適應性並可支持動態演化。 （2）基於類型和效果系統的服務編排形式化分析 普適環境下服務具有的動態特徵使服務編排更為複雜，系統不僅需要關注服務的運行行為是否與用戶的規約一致，而且要求服務遵循一些指定的策略，如服務行為一致、資源使用保護等。課題組將類型和效果系統靜態分析技術套用到普適服務編排計畫，形式化分析了普適服務編排計畫的可信性。研究工作包括基於類型和效果系統的服務編排建模技術，服務發布、服務發現、服務調用、服務編排和流程計畫的形式化描述；項目組給出了基於行為一致的服務替換方法，並推導了類型安全性定理，設計了服務替換分析工具，提出了一種面向普適環境的服務重建方法。 （3）基於抽象狀態機的分析與驗證模型 項目組設計了服務執行分析抽象狀態機，根據一致性要求及行為策略定義分析服務流程，從而得到服務協作執行中可能的失效點，並設計失效點與服務執行恢復狀態點的映射轉換機制，從而實現服務動態進入和退出的透明性；設計行為策略及一致性驗證抽象狀態機，通過該抽象狀態機的模擬執行，自動驗證服務行為的一致性以及驗證候選服務是否違背行為策略。 （4）構建可驗證的普適環境下的服務計算平台 基於OSGi 搭建一個普適計算平台並構建典型的普適套用場景，對上述理論和方法進行驗證；通過將抽象狀態機的執行引擎、類型和效果系統的分析工具以及服務流程向有限狀態機的轉換工具整合到上述普適服務計算平台中，構建了一個可信普適套用開發原型。
