基於分離邏輯的雲存儲管理程式正確性驗證方法

《基於分離邏輯的雲存儲管理程式正確性驗證方法》是依託北京大學，由王捍貧擔任負責人的面上項目。

基本介紹

• 中文名：基於分離邏輯的雲存儲管理程式正確性驗證方法
• 項目負責人：王捍貧
• 項目類別：面上項目
• 依託單位：北京大學

項目摘要

雲計算作為一種新興的計算模型，代表了計算領域未來的發展方向。而雲存儲作為雲計算的基礎之一，與傳統存儲系統相比有著顯而易見的優勢，在近年來得到了迅速的發展。為提高雲存儲服務的可靠性和安全性，需要對雲存儲系統管理程式進行正確性驗證，這是一個亟待解決的問題，雲存儲系統的特殊特點也導致該問題具有挑戰性。本項目擬主要研究：1.對現有的雲存儲系統架構進行抽象建模；2.在上述模型基礎上構造抽象管理語言，並研究其語義定義方法；3.管理系統的性質描述方法（斷言公式）及其語義；4.結合上述管理語言和斷言公式，構建出Hoare型三元組推導系統，最終實現對雲存儲系統管理程式進行正確性驗證。研究雲存儲管理語言的正確性驗證，可以促進雲存儲技術的標準化，提升雲存儲服務的質量，節約雲存儲研發成本，並可以促進形式化方法的研究發展，對學術的進步及國民經濟和社會的發展都有著重要意義。

結題摘要

隨著雲存儲系統在眾多領域上的作用越來越重要，人們有必要對雲存儲系統的管理程式進行相應的正確性驗證，以提高雲存儲系統相關數據服務的可靠性。本項目基於分離邏輯為理論基礎，針對待證目標構建出了一個新的形式化邏輯系統，其中包含了以下幾方面的工作：1. 抽象雲存儲系統的架構，提煉出以數據塊為基本單位對檔案內容進行拆分，將每個數據塊獨立地存放在數據節點中，進而實現對超大規模數據集的部署方式；2. 建立一種描述雲存儲系統管理的形式化建模語言，包含對檔案和數據塊在內的數據結構及相應的操作命令給出語法規則，並對雲存儲系統管理程式的狀態進行定義；3. 構造一種能夠同時處理原始地址和塊地址的斷言語言，包含對之前邏輯系統中斷言的擴展，用以描述原始地址屬性，並且新定義用於描述數據塊屬性的塊斷言，這兩種斷言能夠分別描述雲存儲系統的一些性質，但是彼此之間又是相互獨立的，本項目通過將上述兩種斷言以恰當的方式進行組合，形成了一個用於描述雲存儲系統完整屬性的全局斷言；4. 定義用於形式推理雲存儲系統的規範規則，通過採用與分離邏輯類似的方式，即霍爾三元組的形式，將全局斷言限定在前置條件與後置條件中，本項目以此制定了相應的公理以及規則；5. 初步驗證雲存儲系統管理程式的正確性，包括按照邏輯系統制定的語法編寫出相應的模擬程式，運用斷言語言定義系統所需要滿足的屬性，以及運用規則來證明該程式的終止性與正確性，以此體現了邏輯系統的實用價值。本項目從形式化驗證的角度對雲存儲可靠性所做的相關研究，較好地完成了項目契約規定的研究任務，對提高雲存儲系統中數據管理的可靠性，保證數據處理過程中的正確性有一定的參考價值。本項目完成論文發表和研究生培養的目標，其中幾篇發表在包含Information and Computation、ICALP等國際一流的會議或期刊上。