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

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

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

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

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

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

6、算機(jī)屏幕上看到的東西 什么將出現(xiàn)在帳單上 NAT關(guān)系：mt ct mt：m在t時(shí)刻的取值 ct：c在t時(shí)刻的取值 (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時(shí)刻的取值 ct：c在t時(shí)刻的取值 (mt, ct) REQ 當(dāng)且僅當(dāng)ct描述的環(huán)境控制量是計(jì)算機(jī)系統(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時(shí)刻的取值 it：c在t時(shí)刻的取值 (mt, it) IN 當(dāng)且僅當(dāng)在mt描述的環(huán)境監(jiān)視量下輸入設(shè)備正常工作時(shí)可能產(chǎn)生的值 OUT關(guān)系：ot ct ot：m在t時(shí)刻的取值 ct：c在t時(shí)刻的取值 (ot, ct) OUT 當(dāng)且僅當(dāng)輸出設(shè)備正常工作時(shí)并輸出ot描述的取值時(shí)可能的環(huán)境控制量的取值 軟件需求由系統(tǒng)需求決定： REQ (mt, ct) IN (mt, it) OUT (ot, ct) NAT (mt, ct) 實(shí)際軟件描述為 SOF (it, ot)： (it, ot) SOF 當(dāng)且僅當(dāng)ot描述的是軟件在輸出it描述的取值時(shí)可能的產(chǎn)生的輸出

8、變量的取值 完整包含上述內(nèi)容 驗(yàn)證REQ在NAT定義的條件下的滿足系統(tǒng)可行性條件 一些其它簡(jiǎn)單檢查 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、更簡(jiǎn)潔的表述： （NAT（INSOFOUT） REQ 定義“控制變量”的完整列表 定義“監(jiān)測(cè)變量”的完整列表 對(duì)每個(gè)監(jiān)測(cè)變量，說明其可能的取值集合（如果和時(shí)間相關(guān)，則定義為時(shí)間函數(shù)）。這個(gè)監(jiān)測(cè)變量的取值集合是NAT的值域 對(duì)每個(gè)控制變量，將它的取值描述為監(jiān)測(cè)變量的取值的函數(shù) 說明系統(tǒng)：“理想”系統(tǒng)的行為 假設(shè)能夠獲得被檢測(cè)系統(tǒng)變量的精確值 假設(shè)能夠計(jì)算出被控制系統(tǒng)變量的精確值 期望要保持的監(jiān)測(cè)變量和控制變量之間的關(guān)系，用NAT和REQ表示 定義可允許的軟件行為： 對(duì)軟件系統(tǒng)行為的可容忍的程度，包括： 對(duì)度量被檢測(cè)的屬性值和計(jì)算被控制的屬性值的時(shí)間延遲和精度要求，用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)機(jī) 構(gòu)造子一：模式類 定義在被監(jiān)護(hù)變量上一個(gè)狀態(tài)機(jī) 其中的狀態(tài)稱為系統(tǒng)模式 變遷由事件觸發(fā) 構(gòu)造子二：項(xiàng) 定義在輸入變量，模式，或者其它項(xiàng)之上的輔助函數(shù) 是一個(gè)抽象概念，或者高層概念 引入的目的是為了減少冗余說明 構(gòu)造子三：條件 定義某個(gè)事件點(diǎn)上的一個(gè)或多個(gè)系統(tǒng)實(shí)體上的謂詞，比如：關(guān)系式等 其中，系統(tǒng)實(shí)體可以是輸入/輸出變量，模式或者項(xiàng) 刻畫

11、系統(tǒng)某個(gè)特定可度量時(shí)期的某方面的性質(zhì) 當(dāng)一個(gè)條件的值從真變?yōu)榧?，或者從假變?yōu)檎?，就發(fā)生一個(gè)事件。從這個(gè)意義上說，條件主要用于刻畫事件發(fā)生的時(shí)機(jī) 構(gòu)造子四：事件 當(dāng)系統(tǒng)的任何實(shí)體的值發(fā)生了變化，就有一個(gè)事件出現(xiàn) SCR描述兩類事件發(fā)生的時(shí)機(jī)：T（c）：當(dāng)條件c變?yōu)檎鍲（c）：當(dāng)條件c變?yōu)榧?由檢測(cè)變量的變化引起的事件為檢測(cè)事件 在特定條件下發(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)測(cè)水壓，當(dāng)水壓低于閾值以下時(shí)，打開注入閥，向反應(yīng)堆內(nèi)核填加冷凍劑 系統(tǒng)操作員

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

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

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

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

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

17、變量的取值 | 項(xiàng)的取值當(dāng)前模式 事件 HighFalseT(Inmode)TooLow, PermittedT(Block=On) WHEN Reset=Off T(Inmode) T(Reset=On) OverriddenTrue False Overridden在新狀態(tài)中依賴模式類Pressure和監(jiān)測(cè)變量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á)性：模式類忠的每個(gè)模式都是初始模式靜態(tài)可達(dá)的 互斥性：條件相互之間是互斥的 覆蓋：條件表中的變量，其域中每點(diǎn)有定義 無循環(huán)性：實(shí)體依賴無循環(huán) 檢驗(yàn)的方面包括 需求描述的良構(gòu)性 語法：我們是否