摘要：

如今計算機系統正在各行業各領域得到越來越廣泛的應用,操作系統作為底層軟件平臺,是計算機系統穩定運行的關鍵.國內外由于操作系統軟件缺陷而導致的災難和事故屢見不鮮.保障操作系統的安全可靠具有重要意義.形式化程序驗證使用嚴格的數學證明來保證軟件的正確性和可靠性,能夠比軟件測試,程序靜態分析等方法帶來更強的保障,已被運用于驗證操作系統等底層軟件. 操作系統全局性質是運行過程中系統時刻滿足的性質.這些性質不只是單個模塊具有的,而是在運行時各組件相互協同過程中系統整體應始終滿足的.全局性質從全局的視角刻畫系統整體行為,能夠直觀體現內核設計和開發人員的想法和意圖,形式化證明系統具有的全局性質是保證系統正確可靠的重要方法. 北京控制工程研究所為我國航天器研發了一個嵌入式實時操作系統,該系統已被成功應用于嫦娥3號等航天任務.目前國內針對該系統開展的形式化驗證工作針對的是單個內核組件或具體應用場景,尚缺乏對系統整體性質的驗證. 本文基于一個已有的操作系統驗證框架開展全局性質驗證工作.本文首先擴展了原驗證框架,克服了其對全局性質驗證的支持不夠成熟,驗證代價較高的問題,然后使用擴展后的框架,為我國某航天器操作系統建立了抽象模型,在模型上形式化描述并驗證了若干全局性質.本文的主要貢獻如下: 1.擴展了Certi-μC/OS驗證框架,在高層抽象模型上給出操作系統全局性質的形式化定義,設計了驗證全局性質的推理規則. 2.使用擴展后的驗證框架為目標系統建立了抽象模型,給出主要模塊的系統調用和中斷處理程序的抽象規范,形式化描述了8條與目標系統任務管理和信號量相關的全局性質,使用推理規則證明了目標系統的抽象模型具有這些性質. 3.所有工作都在證明助手Coq中完成,所有證明腳本均可通過機器檢查.為提高手工證明的效率,還開發了一組通用的Coq證明策略.

展開

《新程序員》：云原生和全面數字化實踐50位技術專家共同創作，文字、視頻、音頻交互閱讀

總結

以上是生活随笔為你收集整理的为什么计算机系统安全具有整体性质,操作系统全局性质的形式化描述和验证的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。