[發明專利]用于分布式應用確認的模型檢查

有效

• 申請號: 201110340478.5
• 申請日: 2011-10-19
• 公開（公告）號: CN102436376A
• 公開（公告）日: 2012-05-02
• 發明（設計）人: L·繆;P·宋;L·張;M·G·塔塔
• 申請（專利權）人: 微軟公司
• 主分類號: G06F9/44
• 分類號: G06F9/44;G06F11/36
• 代理公司: 上海專利商標事務所有限公司 31100
• 代理人: 蔡悅

技術領域

本發明涉及計算機應用領域，尤其涉及分布式應用。

背景技術

分布式系統的復雜性及其測試機制已經被廣泛地探索了許多年。在分布式系統中存在許多固有的挑戰，諸如異步通信的等待時間、差錯恢復、時鐘漂移、以及服務分區，從而導致眾多問題，包括死鎖、競爭條件、以及許多其他困難。測試這樣的復雜系統提出了巨大挑戰。在幾年中，已經調查并實現了許多自動測試生成、部署以及執行方法。然而，在自動系統確認和驗證的領域中仍然要求大量努力。

由于事件順序控制復雜性以及隨著系統規模增加導致的測試場景的激增，絕大多數測試方法在使用基于模型的方法方面是隨機的。在這樣的情況下，驗證無法與特定動作和故障相耦合。典型的當前模型構造分布式系統可到達并隨后進行蠻力驗證的狀態圖，這導致狀態空間激增以及高級系統抽象中的困難。大型分布式系統的一個示例是微軟TM?SQL?Azure。SQL?Azure提供基于云的存儲服務，該基于云的存儲服務可將大量數據存儲在分布式數據中心中的各種實際物理硬件上。SQL?Azure是巨大的分布式系統。另外，系統規模動態地改變以便提供彈性存儲。

不僅對這樣的系統的開發而且對這樣的系統的測試提出了巨大挑戰。傳統測試方法可能在一個物理計算機上測試功能，并依賴故障注入來測試故障轉移以及依賴長運距工具來將負載引入系統。測試隨后可檢查分布式系統是否健康而沒有錯誤、沒有分區處于異常狀態、沒有節點處于停機等等。調查分布式系統的問題是非平凡的過程。當分布式系統上發生問題時，調查涉及特定領域的專長和知識。太多軌跡可涉及相關(correlation)和長期調查。當前，事件相關是手動地進行的，該相關涉及對一組歷史表的相關。不知道有關的系統組件的細節，是難以追蹤到問題的根源的。監視分布式系統的健康也主要是手動過程。受限自動監視可檢查某些因素，諸如可用性、服務切換以及監督錯誤，但個人只是在某一事物出錯的情況下檢查其他大量的度量；否則，信息僅被記錄并被忽略。另外，某些異常行為本身可能不表現為明顯的應用錯誤或導致明顯的應用錯誤，或可以無法按自動監視需要的方式被永久存儲。典型示例是存儲器中的狀態、由于失效觸發事件的不必要狀態轉換、以及可被手動檢查忽略的瞬時健康狀態。

發明內容

此處描述了模型檢查系統，該模型檢查系統通過提供模型和通用框架來檢查應用不變屬性、檢測異常行為并監視應用健康從而有效地驗證和確認分布式應用的設計。由模型檢查器驗證的屬性適用于該系統中的單個實體、適用于該系統中的許多實體的組、以及適用于作為整體的系統。模型檢查系統檢查針對從應用的正式描述所導出的應用模型來檢查在線應用行為，這被稱為模型檢查。該系統將具體應用制定為抽象模型以及期望在所有條件下適用于應用的多個規則或屬性。存在四個類型的不變屬性，包括：安全性——在系統中任何點處總為真；活躍度——在系統中故障靜止之后最終為真；公平性——沒有總是忽略某些可應用的轉換的系統執行；以及穩定性——在某一時間點之后總為真。模型檢查器將實際應用執行與模型相比較，并且確認屬性保持為真或是報告屬性被違反。在可同步進行各種驗證和確認活動的情況下，實現了通用框架。

模型檢查系統將目標分布式應用建模成小的有限狀態機的集合和依賴圖來捕捉組件之間的相關。在某些實施例中，模型檢查器所使用的相關關鍵字不依賴于分布式應用運行的機器上的物理時鐘時間。該系統基于事件依賴圖自動地執行根本原因分析。即使失敗涉及多個機器、組件和日志，該系統可將整個事件序列進行相關，以便從在每一組件的貢獻動作期間一直導致問題的操作來跟蹤該問題。由此，模型檢查系統提供了在更現實的生產條件下對分布式應用的有效且全面的確認。

提供發明內容述以便以簡化形式介紹將在以下的具體實施方式中進一步描述的一些概念。本發明內容并不旨在標識所要求保護主題的關鍵特征或必要特征，也不旨在用于限制所要求保護主題的范圍。

附圖說明

圖1是示出在一個實施例中的模型檢查系統的各組件的框圖。

圖2是示出在一個實施例中的模型檢查系統用于使用模型檢查來執行分布式應用的處理的流程圖。

圖3是示出在一個實施例中模型檢查系統用于學習分布式應用行為的一個或多個模型的處理的流程圖。

具體實施方式