面向運行時監控的軟體設計與驗證理論研究

《面向運行時監控的軟體設計與驗證理論研究》是依託中國人民解放軍國防科技大學，由董威擔任項目負責人的面上項目。

基本介紹

• 中文名：面向運行時監控的軟體設計與驗證理論研究
• 項目類別：面上項目
• 項目負責人：董威
• 依託單位：中國人民解放軍國防科技大學

中文摘要

由於軟體自身及其環境的複雜性，軟體故障難以完全避免。因此，在軟體運行過程中實施有效監控，儘早發現可能問題並及時採取修正措施，對提高軟體可靠性與安全性具有重要意義。本課題將首先從航天、武器裝備等領域中關鍵軟體的特點和監控需求出發，探索其失效模式特徵與分類，研究支持多維監控屬性描述的形式化規約技術與監控性質模版；然後結合統一建模語言UML、Aspect軟體設計、設計模式等軟體工程主流技術以及軟體形式建模與設計驗證理論的最新進展，研究面向運行時監控的軟體設計與驗證理論以及針對典型監控屬性的設計模式；進一步以軟體運行時驗證理論為基礎，結合程式分析、軟體故障診斷與隔離等技術，研究運行時主動監控理論框架與關鍵技術，使監控能對軟體運行進行一定程度的預測，及時發現故障趨勢，並通過對軟體運行過程的調整和干涉來避免故障實際產生；最終建立自動化程度高、與主流軟體工程環境相結合的軟體運行時監控設計與驗證工具環境。

結題摘要

對於各種關鍵領域的軟體，即使在開發過程中採用非常嚴格的設計和驗證方法，也無法避免軟體部署後存在遺留缺陷，從而在運行過程中發生背離期望性質的行為。因此，在軟體運行過程中進行動態監控非常重要。但現有監控方法，例如運行時驗證技術等，只能被動的觀察軟體系統執行，當發現對關鍵性質的違背時，往往意味著軟體失效已經發生。對此，基於預測和預防的思想，本項目提出了軟體主動監控的概念，並對其理論基礎和關鍵技術進行了深入研究。主動監控的目標不局限在軟體失效發生後採用相關技術修復失效，而是希望能夠儘早預測失效的可能發生，然後產生相應的調控動作，以避免軟體運行實際到達失效狀態。本項目的主要研究成果包括：（1）結合閉環反饋的控制理論，提出了基於預測語義的軟體主動監控理論和相應的實現框架。該方法針對時序邏輯性質生成基於預測語義的監控器，對可能到來的、違背性質的行為進行預測，並按照部分系統模型生成必要的干涉動作對系統進行調控，以規避實際導致缺陷產生的執行路徑。實例研究表明，該方法能適用於safety-critical系統（如嵌入式控制軟體）和security-critical系統（如信息系統軟體）。（2）在軟體主動監控理論框架下，研究相適應的監控屬性規約技術，以對功能屬性、時序屬性、參數化屬性、周期性等複雜性質進行描述，並設計了能表達控制流與數據流關係的事件序列選擇語言。（3）為了最佳化帶有監控需求的軟體結構、減少監控機制對軟體的影響，研究了面向運行時監控的軟體設計方法，包括基於UML和Aspect的軟體監控設計方法、混成系統的運行監控方法、嵌入式作業系統的運行監控方法、監控設計的一致性檢測方法等。（4）為了提高監控器的生成和運行效率，對監控器自動生成、最佳化和部署方法進行了研究，包括提出了一種能適用於更複雜時序性質的高效預測監控器生成方法；為了提高預測能力以及減少運行時監控開銷，研究了結合靜態分析的預測監控最佳化方法，並研究了多對象、多監控器的協同技術。本項目根據上述研究成果設計實現了軟體主動監控工具原型，對汽車控制系統、火車交通控制、嵌入式作業系統、安全作業系統、部分開源軟體等進行了實驗驗證，取得良好的效果。