基於定理證明的多核並行程式驗證

《基於定理證明的多核並行程式驗證》是依託西安電子科技大學，由張南擔任項目負責人的青年科學基金項目。

基本介紹

• 中文名：基於定理證明的多核並行程式驗證
• 項目類別：青年科學基金項目
• 項目負責人：張南
• 依託單位：西安電子科技大學

中文摘要

擴展命題投影時序邏輯Propositional Projection Temporal Logic(PPTL)，提出適合描述多核並行程式的柱面計算模型Cylinder Computation Model(CCM)，建立擴展的命題投影時序邏輯CCM-PPTL系統。研究它的語法，語義和邏輯規則，研究它的範式，範式圖及可判定性。定義CCM-PPTL的公理和推理規則，建立CCM-PPTL的公理系統；證明該公理系統的合理性和完備性。對PPTL定理證明器進行擴展，實現基於PVS的CCM-PPTL證明器原型。建立基於CCM-PPTL公理系統和證明器對多核並行程式進行驗證的理論和方法。

結題摘要

多核並行程式設計已成為新的程式設計規範。並行程式往往捲入並發程式的概念如並行進程或執行緒之間的互動和同步，資源的共享和競爭等等。由於並行和並發程式具有內在的複雜性，程式的錯誤往往隱藏很深，應用程式測試和分析技術很難被發現。因此，如何保障多核計算環境下並行程式的正確性和可靠性，成為計算機科學領域所面臨的新的挑戰。 建模、仿真和驗證語言（MSVL）是一個基於共享變數模型的並發時序邏輯程式設計語言。本項目主要研究基於MSVL證明理論的多核並行程式驗證方法，研究內容包括：（1）擴展命題投影時序邏輯 PPTL，定義柱面計算CCM 的語法和語義；（2）在擴展的命題投影時序邏輯 CCM-PPTL中，研究相關柱面計算 CCM 的邏輯規則及定理；（3）研究擴展的命題投影時序邏輯 CCM-PPTL 的公理系統；（4）開發基於擴展的命題投影時序邏輯 CCM-PPTL 的公理系統的驗證器；（5）研究多核並行程式的驗證實例。 本項目建立了擴展的命題投影時序邏輯系統 CCM-PPTL，建立了該邏輯系統的模型理論包括語法、語義、 邏輯規則以及相關定理；建立了擴展的命題投影時序邏輯 CCM-PPTL 的公理系統，包括公理集合和推理規則集合，並證明了該公理系統的合理性和完備性；建立了基於擴展的命題投影時序邏輯 CCM-PPTL 的公理系統的多核並行程式的驗證理論和方法；並給出了驗證示範實例；開發了基於擴展的命題投影時序邏輯 CCM-PPTL 的公理系統的驗證器原型。基於本項目提出的柱面計算CCM形式驗證理論與方法，可以有效提高多核並行程式的正確性和可靠性。