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