中科院需求工程 需求工程(第九講)文檔驅(qū)動的方法_

1、金芝中國科學(xué)院數(shù)學(xué)與系統(tǒng)科學(xué)研究院需求文檔的重要性四變量模型SCR需求方法形式化SCR和表演算機制總結(jié) 工程師的職責(zé)之一：保證產(chǎn)品的適用性 要求和應(yīng)用專家準(zhǔn)確、細(xì)致地溝通 溝通必須以寫下來的需求陳述為基礎(chǔ) 用戶和實現(xiàn)者能夠閱讀和分析 能夠在產(chǎn)品開發(fā)完成后用于評估這個產(chǎn)品 能夠用于評定產(chǎn)品完成后的關(guān)于產(chǎn)品缺陷的爭論 沒有文檔，任何工程師做不到這一點 發(fā)現(xiàn)需求是一門藝術(shù)，文檔化需求并驗證它的完整性是一門學(xué)科 需求文檔不表達(dá)如何開發(fā)產(chǎn)品,需求文檔是關(guān)于將開發(fā)什么產(chǎn)品要做什么的描述 三個術(shù)語 描述：關(guān)于該產(chǎn)品的一些信息,可以不完整,但必須是真實的 規(guī)格說明：該產(chǎn)品需求屬性的一個描述,軟件產(chǎn)品的外部可見

2、的行為 模型：具有產(chǎn)品的部分屬性，以及可能不屬于產(chǎn)品的屬性，維護(hù)完整性一致性，方便驗證 可以描述已經(jīng)存在的軟件我們可以不用讀代碼就能夠回答關(guān)于該軟件的問題 可以描述還不存在的軟件程序員和客戶可以就需求達(dá)成一致意見 驗證產(chǎn)品是否滿足需求（測試和/或?qū)彶椋?可以建立工具檢查規(guī)格說明 可以建立工具模擬系統(tǒng)并檢查系統(tǒng) 描述必須比代碼容易理解 文檔必須用一種不限制解決方案的方式陳述需求 測試和證明最終能夠自動化 在計算機出現(xiàn)之前，工程師使用經(jīng)典數(shù)學(xué)來描述和分析產(chǎn)品 在計算機科學(xué)中，大多數(shù)研究者發(fā)明新的“語言” 我們將軟件作為產(chǎn)品來開發(fā) 我們?yōu)槭裁床荒芎唵蔚赜梦覀兞?xí)慣的數(shù)學(xué)來建模？ 傳統(tǒng)產(chǎn)品是無生命的東西

3、（X） 我們需要描述被程序遵循的過程（X） 功能不是連續(xù)的（） 在開始構(gòu)建產(chǎn)品之前，決定要構(gòu)建什么 在設(shè)計之前顯式地說出是“什么決定”，而不是象設(shè)計中那樣隱式地給出 確定你構(gòu)建的是必需的 讓用戶在產(chǎn)品構(gòu)建之前進(jìn)行評判 為軟件開發(fā)者提供有組織的參考文檔 提供精確，一致的信息 關(guān)于約束的問題只涉及一次 讓他們不用決定什么對用戶來說是最好的 補償他們對環(huán)境的知識的缺少 給他們足夠的信息進(jìn)行設(shè)計決策 讓他們準(zhǔn)確地估計需要的時間和資源 容許人員的更替 為質(zhì)量保證組提供參考文檔 測試設(shè)計不應(yīng)該以來程序 授權(quán)的需要質(zhì)量保證組和程序員可能不一致 說明實現(xiàn)相關(guān)的所有約束 知道你面臨什么 為應(yīng)付客戶的變化提供某種

4、形式的保護(hù) 能夠評判可行性和代價 說明未來修訂的約束 硬件/軟件系統(tǒng)的傳統(tǒng)模型基于兩個假設(shè)： 系統(tǒng)具有輸入和輸出 輸出是輸入的數(shù)學(xué)函數(shù) 其中，輸入是系統(tǒng)的實際物理輸入 數(shù)學(xué)函數(shù)可能很復(fù)雜并難以描述 難以得到應(yīng)用專家的審查 在系統(tǒng)的外部，存在物理變量，一些是監(jiān)視變量、一些是控制變量、一些兩者都是 外部設(shè)備感應(yīng)監(jiān)視變量，決定計算機的輸入，讀取計算機輸出，影響控制變量的值 系統(tǒng)需求說明在監(jiān)視變量和控制變量之間希望存在的關(guān)系 領(lǐng)域?qū)＜腋鶕?jù)監(jiān)視變量和控制變量來審查需求，而不是根據(jù)輸入和輸出變量 軟件需求使用輸入和輸出變量來描述影響系統(tǒng)行為的環(huán)境量由系統(tǒng)控制的環(huán)境量度量被監(jiān)測的量設(shè)置被控制的量NAT：物理

5、世界的法則核系統(tǒng)環(huán)境引入的約束REQ：系統(tǒng)必須維護(hù)的被監(jiān)視的量和被控制的量之間的其他約束IN：從被監(jiān)視的量到輸入數(shù)據(jù)項的映射OUT：從輸出數(shù)據(jù)項到被控制的量的映射 整個系統(tǒng)：滿足監(jiān)視變量和控制變量之間的關(guān)系 輸入設(shè)備：滿足監(jiān)視變量和輸入變量之間的關(guān)系 輸出設(shè)備：滿足輸出變量和控制變量之間的關(guān)系 軟件系統(tǒng)：滿足輸入設(shè)備和輸出設(shè)備之間的關(guān)系 識別監(jiān)視變量：(mt1, mt2, , mtn) 識別控制變量：(ct1, ct2, , ctp)主要的監(jiān)視變量是系統(tǒng)外的東西，它的值應(yīng)該影響系統(tǒng)的輸入，比如： 客戶計量器的讀數(shù) 蒸汽溫度主要的控制變量是系統(tǒng)外的東西，它的值應(yīng)該由系統(tǒng)來決定，比如： 操作者來計

6、算機屏幕上看到的東西 什么將出現(xiàn)在帳單上 NAT關(guān)系：mt ct mt：m在t時刻的取值 ct：c在t時刻的取值 (mt, ct) NAT 當(dāng)且僅當(dāng)ct描述的環(huán)境控制量是環(huán)境約束在mt描述的環(huán)境監(jiān)視量下是允許的 REQ關(guān)系：mt ct mt：m在t時刻的取值 ct：c在t時刻的取值 (mt, ct) REQ 當(dāng)且僅當(dāng)ct描述的環(huán)境控制量是計算機系統(tǒng)在mt描述的環(huán)境監(jiān)視量下是允許的關(guān)系滿足的條件1. domain(REQ) domain(NAT)2. domain(REQNAT) = domain(REQ) domain(NAT)其中，（1）表示系統(tǒng)需求文檔的完整性；（1）和（2）表示系統(tǒng)需求文

7、檔的可行性 IN關(guān)系：mt it mt：m在t時刻的取值 it：c在t時刻的取值 (mt, it) IN 當(dāng)且僅當(dāng)在mt描述的環(huán)境監(jiān)視量下輸入設(shè)備正常工作時可能產(chǎn)生的值 OUT關(guān)系：ot ct ot：m在t時刻的取值 ct：c在t時刻的取值 (ot, ct) OUT 當(dāng)且僅當(dāng)輸出設(shè)備正常工作時并輸出ot描述的取值時可能的環(huán)境控制量的取值 軟件需求由系統(tǒng)需求決定： REQ (mt, ct) IN (mt, it) OUT (ot, ct) NAT (mt, ct) 實際軟件描述為 SOF (it, ot)： (it, ot) SOF 當(dāng)且僅當(dāng)ot描述的是軟件在輸出it描述的取值時可能的產(chǎn)生的輸出

8、變量的取值 完整包含上述內(nèi)容 驗證REQ在NAT定義的條件下的滿足系統(tǒng)可行性條件 一些其它簡單檢查 SOF中出現(xiàn)的輸入變量都是IN中的輸入變量 OUT中出現(xiàn)的輸出變量都是SOF中的輸出變量 IN中出現(xiàn)的監(jiān)視變量都是REQ中的監(jiān)視變量 OUT中出現(xiàn)的控制變量都是REQ中的控制變量 REQ和NAT中的變量相同 讓軟件是可接受的，SOF必須滿足： mt it ot ct IN (mt, it) SOF (it, ot) OUT (ot, ct) NAT (mt, ct) REQ (mt, ct) 采用功能表述： mt mt domain(NAT) (REQ(mt) = OUT(SOF(IN(mt)

9、更簡潔的表述： （NAT（INSOFOUT） REQ 定義“控制變量”的完整列表 定義“監(jiān)測變量”的完整列表 對每個監(jiān)測變量，說明其可能的取值集合（如果和時間相關(guān)，則定義為時間函數(shù)）。這個監(jiān)測變量的取值集合是NAT的值域 對每個控制變量，將它的取值描述為監(jiān)測變量的取值的函數(shù) 說明系統(tǒng)：“理想”系統(tǒng)的行為 假設(shè)能夠獲得被檢測系統(tǒng)變量的精確值 假設(shè)能夠計算出被控制系統(tǒng)變量的精確值 期望要保持的監(jiān)測變量和控制變量之間的關(guān)系，用NAT和REQ表示 定義可允許的軟件行為： 對軟件系統(tǒng)行為的可容忍的程度，包括： 對度量被檢測的屬性值和計算被控制的屬性值的時間延遲和精度要求，用IN和OUT表示 SCR：So

10、ftware Cost Reduction 提出：Heninger,K.L., 80年代初期 成功應(yīng)用領(lǐng)域： A-7操作飛行程序 潛水艇通訊系統(tǒng) 加拿大Darlington核電站安全組件 Lockheeds C-130j操作飛行程序 基本表示法表表示法狀態(tài)機 構(gòu)造子一：模式類 定義在被監(jiān)護(hù)變量上一個狀態(tài)機 其中的狀態(tài)稱為系統(tǒng)模式 變遷由事件觸發(fā) 構(gòu)造子二：項 定義在輸入變量，模式，或者其它項之上的輔助函數(shù) 是一個抽象概念，或者高層概念 引入的目的是為了減少冗余說明 構(gòu)造子三：條件 定義某個事件點上的一個或多個系統(tǒng)實體上的謂詞，比如：關(guān)系式等 其中，系統(tǒng)實體可以是輸入/輸出變量，模式或者項 刻畫

11、系統(tǒng)某個特定可度量時期的某方面的性質(zhì) 當(dāng)一個條件的值從真變?yōu)榧伲蛘邚募僮優(yōu)檎?，就發(fā)生一個事件。從這個意義上說，條件主要用于刻畫事件發(fā)生的時機 構(gòu)造子四：事件 當(dāng)系統(tǒng)的任何實體的值發(fā)生了變化，就有一個事件出現(xiàn) SCR描述兩類事件發(fā)生的時機：T（c）：當(dāng)條件c變?yōu)檎鍲（c）：當(dāng)條件c變?yōu)榧?由檢測變量的變化引起的事件為檢測事件 在特定條件下發(fā)生的事件為條件事件T（c）WHEN d：在條件d為真的情況下，當(dāng)條件c變?yōu)檎鍲（c）WHEN d：在條件d為真的情況下，當(dāng)條件c變?yōu)榧?基本需求： 負(fù)責(zé)打開和關(guān)閉安全注入閥。 需要監(jiān)測水壓，當(dāng)水壓低于閾值以下時，打開注入閥，向反應(yīng)堆內(nèi)核填加冷凍劑 系統(tǒng)操作員

12、可以用Block（或Reset）開關(guān)阻止安全注入（或恢復(fù)安全注入）Overridden：表示安全噴射被阻止三個被三個被監(jiān)測量監(jiān)測量每個感應(yīng)器產(chǎn)每個感應(yīng)器產(chǎn)生一個輸入量生一個輸入量被控制被控制的量的量兩個模兩個模式類式類重載重載三個系三個系統(tǒng)模式統(tǒng)模式 系統(tǒng)有兩個模式類： “壓力”模式 “重載”模式 模式類“壓力”中有三個系統(tǒng)模式： 壓力太低，WaterPress = Low 允許的范圍，Low WaterPress = Permit 壓力高， Permit WaterPress 模式變遷表：定義軟件可以處于的模式（狀態(tài)）及其模式變遷 一個系統(tǒng)將包含不同的模式類，每個模式類有一個模式表，展示引起

13、模式之間的變遷的條件 函數(shù)表示形式：模式 事件 模式當(dāng)前模式事件下一模式TooLowT(WaterPress Low)PermittedPermittedT(WaterPress Permit)HighPermittedT(WaterPress Low)TooLowHighT(WaterPress ， v TY(r)復(fù)合條件：簡單條件通過連接詞組合而成連接詞：，基本表示法T事件種類原始事件： T(r=v), rRF, vTY(r)監(jiān)測事件： T(r=v), rIR, vTY(r)基本事件： T(c), c是一個簡單條件簡單條件事件： T(c) WHEN d, T(c)是一個基本事件，d是一個簡

14、單條件或者復(fù)合條件條件事件：簡單條件事件的和取或析取 簡單事件 T(c) = c c 如果c = rv，則c = (rv) = rv 簡單條件事件 T(c) WHEN d = c c dT(Block=On) WHEN Reset=OffBlockOn Block=On Reset=Off 一個系統(tǒng)為一個四元組： Em輸入事件的集合 S可能的系統(tǒng)狀態(tài)的集合 s0初始狀態(tài) T系統(tǒng)變換，為Em S到S上的一個部分函數(shù)，表示被允許的系統(tǒng)狀態(tài)變遷 假設(shè)： 單輸入假設(shè)：每次系統(tǒng)變遷正好只有一個監(jiān)測事件出現(xiàn) 同步假設(shè)：系統(tǒng)在響應(yīng)下一個監(jiān)測事件之前，對當(dāng)前的監(jiān)測事件的響應(yīng)必須全部完成 構(gòu)造實體的新狀態(tài)依賴集

15、 監(jiān)測變量的新狀態(tài)依賴集為空 由條件表定義的實體，其新狀態(tài)依賴集包含所關(guān)聯(lián)的模式類名，和出現(xiàn)在條件表中的所有實體名 由事件表或模式變遷表定義的實體，其新狀態(tài)依賴集包含出現(xiàn)在表中作為一個基本事件的一部分的所有實體 新狀態(tài)依賴集構(gòu)成了RF上的一個偏序關(guān)系 條件表 描述從模式和條件到控制變量或項上的一個函數(shù) 函數(shù)表示形式：模式 條件 控制變量的取值 | 項的取值當(dāng)前模式條件High, PermittedTrueFalseTooLowOverridden OverriddenSafetyInjectionOffOnSafetyInjection在新狀態(tài)中依賴模式類Pressure和項Overridde

16、n 模式變遷表：定義軟件可以處于的模式（狀態(tài)）及其模式變遷 一個系統(tǒng)將包含不同的模式類，每個模式類有一個模式表，展示引起模式之間的變遷的條件 函數(shù)表示形式：模式 事件 模式當(dāng)前模式事件下一模式TooLowT(WaterPress Low)PermittedPermittedT(WaterPress Permit)HighPermittedT(WaterPress Low)TooLowHighT(WaterPress Permit )Permitted模式類Pressure在新狀態(tài)中依賴WaterPress 事件表 描述從模式和事件到控制變量或項的取值上的一個函數(shù) 函數(shù)表示形式：模式 事件 控制

17、變量的取值 | 項的取值當(dāng)前模式 事件 HighFalseT(Inmode)TooLow, PermittedT(Block=On) WHEN Reset=Off T(Inmode) T(Reset=On) OverriddenTrue False Overridden在新狀態(tài)中依賴模式類Pressure和監(jiān)測變量Block和Reset 一種可能性： R = 當(dāng)前模式條件High, Permitted TrueFalseTooLowOverridden OverriddenSafetyInjectionOffOn當(dāng)前模式事件下一模式TooLowT(WaterPress Low)Permitte

18、dPermittedT(WaterPress Permit)HighPermittedT(WaterPress Low)TooLowHighT(WaterPress Permit )Permitted當(dāng)前模式事件下一模式TooLowT(WaterPress Low)PermittedPermittedT(WaterPress Permit)HighPermittedT(WaterPress Low)TooLowHighT(WaterPress Permit )Permitted 合適的語法 類型正確性 變量和模式定義的完整性 初始值：模式類、輸入變量、輸出變量 可達(dá)性：模式類忠的每個模式都是初始模式靜態(tài)可達(dá)的 互斥性：條件相互之間是互斥的 覆蓋：條件表中的變量，其域中每點有定義 無循環(huán)性：實體依賴無循環(huán) 檢驗的方面包括 需求描述的良構(gòu)性 語法：我們是否