適航實時操作系統安全可靠的驗證方案

DO-178C[[i]]在核心文檔在DO-178B的基礎上進行了重要改進，其中補充文檔對特定的技術—軟件形式化方法進行了詳細的說明。DO-178C首次正式地承認了機載軟件開發過程當中使用形式化方法的有效性。形式化方法是一類用于機載軟件的規約、開發和驗證的基于技術的數學方法，例如:形式化方法工具可以用來表達飛機上的數學表達控制原則以及它們到飛機計算機上的軟件代碼的轉換。形式化方法可以應用到軟件開發的多個階段，也可以作為一種驗證技術。

DO-178C標準對于軟件開發和管理、驗證提出了明確的目標和要求，并且提供了參考的方法。但是DO-178C標準并沒有提出軟件的驗證的具體細節和流程。在實踐中我們提出了具體的保障適航實時操作系統安全可靠的驗證方案如圖1所示。

在提出的這個方案中我們將驗證方案從宏觀方面分為兩個部分：一個是DO-178C提出的驗證，一個是軟件形式化驗證。

Do-178C提出的方案包括三個活動評審、分析和軟件測試。其中，評審包括四個部分的評審：1）軟件計劃評審；2）軟件需求、設計和代碼評審；3）測試資料評審；4）其它資料的評審。評審的目的是保障軟件的開發計劃符合Do-178C的標準。其中，分析包括3個部分的分析：1）編碼集成分析；2）基于需求的覆蓋性分析；3）基于結構的覆蓋性分析；分析是提供正確性的可重復證據的一種驗證活動。其中軟件測試包含基于需求的軟件測試方法和保障軟件正常和健壯性的測試用例的開發，軟件測試的目的是揭示開發階段制造的錯誤。由于所有的人類活動，尤其是復雜的活動都會引入錯誤，所以測試越嚴厲，我們就可以獲得對產品質量的越大信心。通過對軟件評審、分析、測試驗證活動的執行，檢測出軟件存在的安全隱患，及時更改，使我們的軟件達到滿足適航的A級標準。

軟件形式化驗證部分，我們計劃使用Coq一個基于高階邏輯的定理證明工具驗證系統的關鍵API，包括定時器中斷處理程序（以及用于演示多級中斷的支持的偽中斷處理程序），調度程序，時間管理和四個同步機制：消息隊列，郵箱，信號量和互斥體。

[[i]] DO-178C, Software Considerations in Airborne Systems and Equipment Certification[J].

活動 安全

版權聲明：本文內容由網絡用戶投稿，版權歸原作者所有，本站不擁有其著作權，亦不承擔相應法律責任。如果您發現本站中有涉嫌抄襲或描述失實的內容，請聯系我們jiasou666@gmail.com 處理，核實后本網站將在24小時內刪除侵權內容。