《大規模分散式系統實時可預測線上分析研究》是依託上海交通大學，由戚正偉擔任項目負責人的聯合基金項目。
基本介紹
- 中文名：大規模分散式系統實時可預測線上分析研究
- 項目類別：聯合基金項目
- 項目負責人：戚正偉
- 依託單位：上海交通大學
- 負責人職稱：教授
- 申請代碼：F02
- 研究期限：2009-01-01 至 2011-12-31
- 批准號：60873209
- 支持經費：30（萬元）
項目摘要
鑒於大規模分散式系統的複雜性，對其進行調試、測試和監控是一項重大的挑戰。現有的基於有限路徑的線上模型檢測方法缺少實時概念；可預測分析方法中缺少與定量時間有關的依賴。本課題提出了分散式系統定量時間依賴模型，通過動態實時向量時鐘算法給出系統的一致狀態。根據時間依賴等偏序關係和可預測調度算法得到實時計算格，通過視窗尺寸調整、時間依賴和BDD技術最佳化其存儲和遍歷。建立實時有限路徑時態邏輯RFLTL的形式化模型，採用RFLTL描述帶定量時間約束的安全性和活性性質，並用重寫邏輯描述RFLTL典範項代數和典範可達模型。通過二叉決策有限自動機BDFSM壓縮RFLTL狀態空間，並根據重寫邏輯提供的商代數模型、等式抽象和代數模擬抽象，結合現有的偏序規約、SAT/SMT等最佳化算法，通過實時計算格的劃分，在現有謂詞檢測基礎上，提供一個高效的分散式實時可預測線上分析方法，更有效地檢測系統錯誤和性能缺陷。
