基於模型檢測的高可靠性軟體動態更新的設計與驗證

《基於模型檢測的高可靠性軟體動態更新的設計與驗證》是依託華東師範大學，由張民擔任項目負責人的青年科學基金項目。

基本介紹

• 中文名：基於模型檢測的高可靠性軟體動態更新的設計與驗證
• 項目類別：青年科學基金項目
• 項目負責人：張民
• 依託單位：華東師範大學

項目摘要

對於大多數軟體，更新在其生命周期中都是不可避免的。傳統的更新方法是首先停止當前軟體的運行，安裝新的軟體，然後重新啟動。然而在一些安全攸關的領域，如金融系統，交通控制系統和航空系統，軟體需要保證不間斷的運行，片刻的中斷都有可能造成重大的經濟損失或帶來致命的安全隱患。為解決這類軟體的更新問題，軟體動態更新技術被提出並得到深入的研究。軟體動態更新可以在不中斷軟體運行的前提下實現軟體的更新，是一種非常有前景的更新技術。然而動態更新軟體如同在修理一輛高速行駛的汽車，對更新可靠性有很高的要求，保證在更新過程中不會導致系統錯誤。如何設計一個可靠的軟體動態更新並驗證其可靠性是當前軟體動態更新技術中最主要的難點之一。模型檢測是一種利用數學的方法驗證計算機軟體和硬體可靠性的技術。本課題擬研究如何利用模型檢測的方法設計高可靠性的軟體動態更新方法並對其可靠性進行形式化分析和驗證，具有重要的理論和現實意義。

結題摘要

軟體動態更新是一種在不中斷軟體運行的前提下實現軟體的更新的技術，尤其對那些提供不間斷服務的系統具有非常重要的套用。這類系統大多安全攸關，因此必須保證動態更新的安全性。由於動態更新直接作用於運行中的軟體，傳統的測試方法無法有效地發現更新中所有可能出現問題。 本項目旨在藉助形式化的方法，通過形式化驗證技術實現軟體動態更新的正確性驗證與分析，從而保證其安全性。我們提出一種通用的基於帶標籤Kripke模型的軟體動態更新驗證方法，該方法通過對舊系統和新系統定義成獨立的模型，在此基礎上定義從舊狀態到新狀態的遷移規則，實現了軟體更新的形式化定義。再次，我們從兩個方面定義了軟體動態更新的正確性，分別是新狀態的可達性與套用相關的時序性質。新狀態的可達性保證了軟體的更新一定會完成，與套用相關的時序性質則保證了系統在更新前後的行為正確性。最後，我們在現有針對帶標籤的Kripke結構的模型檢測方法的基礎上進行擴展，實現了軟體動態更新的形式化驗證，並針對Python程式的更新作為案例進行了研究，實驗結果表明方法的可行性。 本研究在軟體動態更新的建模，正確性定義，驗證等方面提出了一套相對通用的建模與驗證方法，並通過具體的案例研究說明了方法的有效性，為軟體動態更新技術提供了嚴格的安全分析方法，可有效解決軟體動態更新安全性分析技術瓶頸，進而促進這一實用技術在實際領域的套用。 基於以上研究成果，本項目共發表論文10篇（包括CCF-B類、SCI二區論文等期刊論文5篇，CCF-C類國際會議論文5篇），獲得軟體著作權1項，培養了4名碩士研究生和輔助培養了博士研究生1名。