安全苛求系統(tǒng)及其評估(編輯修改稿)
2025-02-13 14:00 本頁面
【文章內容簡介】 項執(zhí)行，前提是通過快速的危險故障檢測和 屏蔽 來確保它的安全操作 (例如通過編碼，多路計算和比較，或通過連續(xù)的測試 )。盡管只由一個項實施實際的安全相關功能，但檢查 /測試 /檢測功能應被看作為第二項。檢查 /測試 /檢測功應是獨立的，以避免共因失效。 軟件容錯和故障安全技術 ?多版本編程技術 ?恢復塊 ?選擇合適的程序設計語言 ?設計良好、清晰的軟件架構 ?軟件模塊化，減少模塊相互依賴 ?防御性編程 ?軟件注釋 ?軟件測試 系統(tǒng)可靠性基本概念 ?失效率 ?浴盆曲線 ?MTTF ?MTTR ?MTBF ?可用性 可靠性模型 ?可靠性方框圖 ? 串聯 ? 并聯 ? 串并聯組合 ?失效的獨立性 ?馬爾可夫模型 ? 離散馬爾可夫模型 ? 連續(xù)馬爾可夫模型 ?其他模型 可靠性預測和評估 ?硬件可靠性預測 ?軟件可靠性預測 形式化方法概要 ? 傳統(tǒng)的諸如測試、故障樹等檢錯、糾錯和容錯技術擅長處理由隨機產生、系統(tǒng)老化或系統(tǒng)單部件引起的，而不是由復雜的交互作用引起的故障。它們是在假設系統(tǒng)的設計正確的情況下，對軟件、硬件故障進行處理。同時，軟件的故障處理主要借鑒于硬件故障處理技術。然而硬、軟件的故障性質是有差別的，軟件具有離散性，更適合用集合、格、群等數學工具來表達。 ? 一種更為嚴格和客觀安全保障方法 ? 形式化是指使用離散數學和邏輯學的技術來分析需求、設計和構建計算機系統(tǒng)及其軟件，用嚴格的數學符號和數學法則對目標系統(tǒng)的的結構與行為進行有效的綜合分析和推理的方法，它為系統(tǒng)的說明、開發(fā)驗證提供了一個框架，以利于發(fā)現目標系統(tǒng)需求中的不一致、不完整的情況。 形式化方法分類 ? 形式化規(guī)范 ? 描述順序系統(tǒng)行為的形式規(guī)范方法：典型有 Z、 B、 VDM等。 這類方法中狀態(tài)使用集合、關系和函數等數學結構來表示；狀態(tài)轉移使用前置條件和后置條件來表示。 ? 描述并發(fā)系統(tǒng)行為的形式規(guī)范方法：典型有 CSP、 CCS、時序邏輯和 I/O自動機。這類方法中狀態(tài)只使用簡單的數學類型例如整數或對狀態(tài)根本沒有定義；系統(tǒng)的行為用序列、樹或事件的偏序關系來表示。 ? 集成的形式規(guī)范方法：典型有 SDL和 RAISE。它們把兩種不同的方法結合起來，既能表示復雜的狀態(tài)類型又能描述并發(fā)系統(tǒng)的特性 。 ? 形式化驗證 ? 模型檢驗 (model checking)： 模型檢驗是對有限狀態(tài)系統(tǒng)的一種形式化確認方法，具體做法是：采用一種形式語言描述系統(tǒng)的規(guī)范說明，構造一種算法來遍歷根據系統(tǒng)規(guī)范設計的實現模型，確認實現模型是否滿足系統(tǒng)的規(guī)范說明。由于系統(tǒng)的狀態(tài)是有限的，所以該算法必然會終止。 ? 定理證明： 定理證明的原理是：首先我們定義一種數學邏輯，該邏輯系統(tǒng)實際上是一個形式化的系統(tǒng)，由一系列公理和推理規(guī)則組成。然后我們用這種數學邏輯分別表示被驗證系統(tǒng)和其被期望的特性。所謂定理證明就是從系統(tǒng)的公理出發(fā)使用推理規(guī)則逐步推導出其所期望的特性的證明過程。證明所需要的步驟依賴于系統(tǒng)的公理和推理規(guī)則，在某種程度上也依賴于其派生定義和中間引理。與模型檢驗不同 !定理證明可直接處理無限的狀態(tài)空間。 形式化方法的開發(fā)過程 系 統(tǒng) 概 念 設 計 （ D 1 ）系 統(tǒng) 需 求 分 析 （ D 2 ）系 統(tǒng) 功 能 分 配 （ D 3 ）設 計 系 統(tǒng) 體 系 結 構 （ D 4 ）安 全 苛 求 子 系 統(tǒng)非 安 全 苛 求 系 統(tǒng)軟 / 硬 件 功 能 分 配 （ D 5 ）設 計 生 成 實 現 （ D 6 ）系 統(tǒng) 集 成 、 安 裝 （ D 7 ）系 統(tǒng) 認 證 運 行 （ D 8 ）安 全 苛 求 / 非 苛 求 功 能 需 求系 統(tǒng) 概 念對 概 念 模 型 （ V 1 ）對 系 統(tǒng) 需 求 分 析 （ V 2 ）對 體 系 結 構 模 型 （ V 3 ）對 軟 / 硬 件 需 求 （ V 4 ）對 設 計 ( V 5 ）系 統(tǒng) 安 全 約 束體 系 結 構 安 全 確 認系 統(tǒng) 開 發(fā) 形 式 化 驗 證驗證和確認計劃 驗證和確認人員必須滿足獨立性要求 動態(tài)測試 ? 功能測試 ? 結構測試 ? 隨機測試 ? 動態(tài)測試技術 ? 基于等價類劃分的測試案例 ? 基于邊界值分析的測試案例 ? 狀態(tài)轉移測試 ? 概率測試 ? 基于結構的測試 ? 過程仿真 ? 猜錯 ? 播錯 ? 實時和內存測試 ? 性能測試 ? 壓力測試 ? 環(huán)境仿真 ? 安全性測試 靜態(tài)分析技術 ?走查 /設計審核 ?檢查表 ?形式證明 ?Fagan檢查 ?控制流分析 ?數據流分析 ?符號執(zhí)行 ?度量 建模技術 ?形式化方法 ?軟件原型 ?性能建模 ?狀態(tài)轉移圖 ?時間 Petri網 ?數據流圖 ?結構圖 ?環(huán)境建模 測試策略 ?測試覆蓋率 —— 完備測試不可能 ? 語句覆蓋率 ? 分枝覆蓋率 ? 組合判定覆蓋率等等 ?測試充分性準則 ? 基于需求的準則 ? 基于結構的準則
試題試卷相關推薦
鄂ICP備17016276號-1