需求工程金芝中國科學(xué)院數(shù)學(xué)與系統(tǒng)科學(xué)研究院zhijin@第九講：文檔驅(qū)動方法需求文檔的重要性四變量模型SCR需求方法形式化SCR和表演算機制總結(jié)從軟件工程師的職責(zé)談起工程師的職責(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é)科好文檔的作用可以描述已經(jīng)存在的軟件——我們可以不用讀代碼就能夠回答關(guān)于該軟件的問題可以描述還不存在的軟件——程序員和客戶可以就需求達成一致意見驗證產(chǎn)品是否滿足需求（測試和/或?qū)彶椋┛梢越⒐ぞ邫z查規(guī)格說明可以建立工具模擬系統(tǒng)并檢查系統(tǒng)文檔可接受的標(biāo)準(zhǔn)描述必須比代碼容易理解文檔必須用一種不限制解決方案的方式陳述需求測試和證明最終能夠自動化程序與其它工程產(chǎn)品不同嗎？在計算機出現(xiàn)之前，工程師使用經(jīng)典數(shù)學(xué)來描述和分析產(chǎn)品在計算機科學(xué)中，大多數(shù)研究者發(fā)明新的“語言”我們將軟件作為產(chǎn)品來開發(fā)程序與其它工程產(chǎn)品不同嗎？我們?yōu)槭裁床荒芎唵蔚赜梦覀兞?xí)慣的數(shù)學(xué)來建模？傳統(tǒng)產(chǎn)品是無生命的東西（X）我們需要描述被程序遵循的過程（X）功能不是連續(xù)的（√）需求階段的目的容許人員的更替為質(zhì)量保證組提供參考文檔測試設(shè)計不應(yīng)該以來程序授權(quán)的需要——質(zhì)量保證組和程序員可能不一致說明實現(xiàn)相關(guān)的所有約束知道你面臨什么為應(yīng)付客戶的變化提供某種形式的保護能夠評判可行性和代價說明未來修訂的約束四變量模型在系統(tǒng)的外部，存在物理變量，一些是監(jiān)視變量、一些是控制變量、一些兩者都是外部設(shè)備感應(yīng)監(jiān)視變量，決定計算機的輸入，讀取計算機輸出，影響控制變量的值系統(tǒng)需求說明在監(jiān)視變量和控制變量之間希望存在的關(guān)系領(lǐng)域?qū)＜腋鶕?jù)監(jiān)視變量和控制變量來審查需求，而不是根據(jù)輸入和輸出變量軟件需求使用輸入和輸出變量來描述四變量模型的關(guān)系整個系統(tǒng)：滿足監(jiān)視變量和控制變量之間的關(guān)系輸入設(shè)備：滿足監(jiān)視變量和輸入變量之間的關(guān)系輸出設(shè)備：滿足輸出變量和控制變量之間的關(guān)系軟件系統(tǒng)：滿足輸入設(shè)備和輸出設(shè)備之間的關(guān)系識別和聲明監(jiān)視和控制變量識別監(jiān)視變量：(mt1,mt2,…,mtn)識別控制變量：(ct1,ct2,…,ctp)主要的監(jiān)視變量是系統(tǒng)外的東西，它的值應(yīng)該影響系統(tǒng)的輸入，比如：客戶計量器的讀數(shù)蒸汽溫度主要的控制變量是系統(tǒng)外的東西，它的值應(yīng)該由系統(tǒng)來決定，比如：操作者來計算機屏幕上看到的東西什么將出現(xiàn)在帳單上定義變量之間的關(guān)系NAT關(guān)系：mtctmt：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)系：mtctmt：m在t時刻的取值ct：c在t時刻的取值(mt,ct)REQ當(dāng)且僅當(dāng)ct描述的環(huán)境控制量是計算機系統(tǒng)在mt描述的環(huán)境監(jiān)視量下是允許的關(guān)系滿足的條件domain(REQ)domain(NAT)domain(REQNAT)=domain(REQ)

domain(NAT)其中，（1）表示系統(tǒng)需求文檔的完整性；（1）和（2）表示系統(tǒng)需求文檔的可行性定義變量之間的關(guān)系IN關(guān)系：mtitmt：m在t時刻的取值it：c在t時刻的取值(mt,it)IN當(dāng)且僅當(dāng)在mt描述的環(huán)境監(jiān)視量下輸入設(shè)備正常工作時可能產(chǎn)生的值OUT關(guān)系：otctot：m在t時刻的取值ct：c在t時刻的取值(ot,ct)OUT當(dāng)且僅當(dāng)輸出設(shè)備正常工作時并輸出ot描述的取值時可能的環(huán)境控制量的取值軟件需求文檔的檢查完整包含上述內(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必須滿足：mtitotct[IN(mt,it)SOF(it,ot)OUT(ot,ct)NAT(mt,ct)REQ(mt,ct)采用功能表述：mt[mtdomain(NAT)(REQ(mt)=OUT(SOF(IN(mt)))))]更簡潔的表述：（NAT（INSOFOUT））REQ四變量模型蘊涵的需求過程說明系統(tǒng)：“理想”系統(tǒng)的行為假設(shè)能夠獲得被檢測系統(tǒng)變量的精確值假設(shè)能夠計算出被控制系統(tǒng)變量的精確值期望要保持的監(jiān)測變量和控制變量之間的關(guān)系，用NAT和REQ表示定義可允許的軟件行為：對軟件系統(tǒng)行為的可容忍的程度，包括：對度量被檢測的屬性值和計算被控制的屬性值的時間延遲和精度要求，用IN和OUT表示SCR需求方法SCR：SoftwareCostReduction提出：Heninger,K.L.,80年代初期成功應(yīng)用領(lǐng)域：A-7操作飛行程序潛水艇通訊系統(tǒng)加拿大Darlington核電站安全組件Lockheed’sC-130j操作飛行程序基本概念和表示法構(gòu)造子一：模式類定義在被監(jiān)護變量上一個狀態(tài)機其中的狀態(tài)稱為系統(tǒng)模式變遷由事件觸發(fā)模式類刻畫了系統(tǒng)運行的一段相互關(guān)聯(lián)的上下文主要目的是劃分狀態(tài)集合，簡化函數(shù)的描述基本概念和表示法構(gòu)造子二：項定義在輸入變量，模式，或者其它項之上的輔助函數(shù)是一個抽象概念，或者高層概念引入的目的是為了減少冗余說明基本概念和表示法構(gòu)造子三：條件定義某個事件點上的一個或多個系統(tǒng)實體上的謂詞，比如：關(guān)系式等其中，系統(tǒng)實體可以是輸入/輸出變量，模式或者項刻畫系統(tǒng)某個特定可度量時期的某方面的性質(zhì)當(dāng)一個條件的值從真變?yōu)榧?，或者從假變?yōu)檎?，就發(fā)生一個事件。從這個意義上說，條件主要用于刻畫事件發(fā)生的時機案例：安全注入系統(tǒng)基本需求：負(fù)責(zé)打開和關(guān)閉安全注入閥。需要監(jiān)測水壓，當(dāng)水壓低于閾值以下時，打開注入閥，向反應(yīng)堆內(nèi)核填加冷凍劑系統(tǒng)操作員可以用‘Block’（或‘Reset’）開關(guān)阻止安全注入（或恢復(fù)安全注入）安全注入系統(tǒng)：SCR需求Overridden：表示安全噴射被阻止三個被監(jiān)測量每個感應(yīng)器產(chǎn)生一個輸入量被控制的量兩個模式類重載三個系統(tǒng)模式安全注入系統(tǒng)：SCR需求系統(tǒng)有兩個模式類：“壓力”模式“重載”模式模式類“壓力”中有三個系統(tǒng)模式：壓力太低，WaterPress=<Low允許的范圍，Low<WaterPress=<Permit壓力高，Permit<WaterPressSCR需求的表示模式變遷表：定義軟件可以處于的模式（狀態(tài)）及其模式變遷一個系統(tǒng)將包含不同的模式類，每個模式類有一個模式表，展示引起模式之間的變遷的條件函數(shù)表示形式：模式事件模式當(dāng)前模式事件下一模式TooLow@T(WaterPress≥Low)PermittedPermitted@T(WaterPress≥Permit)HighPermitted@T(WaterPress<Low)TooLowHigh@T(WaterPress<Permit)PermittedSCR需求的表示事件表描述從模式和事件到控制變量或項的取值上的一個函數(shù)函數(shù)表示形式：模式事件控制變量的取值|項的取值當(dāng)前模式事件HighFalse@T(Inmode)TooLow,Permitted@T(Block=On)WHENReset=Off@T(Inmode)@T(Reset=On)OverriddenTrueFalseSCR需求的表示條件表描述從模式和條件到控制變量或項上的一個函數(shù)函數(shù)表示形式：模式條件控制變量的取值|項的取值當(dāng)前模式條件High,PermittedTrueFalseTooLowOverriddenOverriddenSafetyInjectionOffOnSCR需求定義過程生成系統(tǒng)需求規(guī)范SRS確定并描述控制變量C；確定并描述監(jiān)視變量M；確定并描述系統(tǒng)模式類；定義關(guān)系REQ；生成系統(tǒng)設(shè)計規(guī)范SDS確定并描述輸入和輸出變量；定義輸入/輸出變量和監(jiān)視/控制變量之間的關(guān)系；生成軟件需求規(guī)范SoRS定義關(guān)系D_IN和D_OUT；對SRS進行擴充，增加諸如系統(tǒng)在硬件失效時的行為等需求定義硬件失效時行為；對每個控制變量增加時序約束；把關(guān)系REQ擴展為關(guān)系。SCR需求中各類關(guān)系形式化SCR：基礎(chǔ)基礎(chǔ)命名：模式集合（MS=Mi）實體名集合（RF=MRIRORGR）實體取值的集合（VS=MSTS）數(shù)據(jù)類型集合（TS）TY：函數(shù)，系統(tǒng)實體該實體的合法值TY：RFVS模式類名集合輸入變量名集合輸出變量名集合項名集合安全注入系統(tǒng)：SCR需求Overridden：表示安全噴射被阻止三個被監(jiān)測量每個感應(yīng)器產(chǎn)生一個輸入量被控制的量兩個模式類重載三個系統(tǒng)模式形式化SCR：例RF={Block，Reset，WaterPres，Pressure，SafetyInjection，Overridden}TY（Pressure）={TooLow，Permitted，High}TY（WaterPres）={0，1，2，，2000}TY（Overridden）={true，false}TY（Block）={On，Off}形式化SCR：條件簡單條件truefalserv：rRF，{=，，>，<，，}，vTY(r)復(fù)合條件：簡單條件通過連接詞組合而成連接詞：，，形式化SCR：事件基本表示法@T事件種類原始事件：@T(r=v),rRF,vTY(r)監(jiān)測事件：@T(r=v),rIR,vTY(r)基本事件：@T(c),c是一個簡單條件簡單條件事件：@T(c)WHENd,@T(c)是一個基本事件，d是一個簡單條件或者復(fù)合條件條件事件：簡單條件事件的和取或析取事件的語義簡單事件@T(c)=cc‘如果c=rv，則c’=(rv)’=r’v簡單條件事件@T(c)WHENd=cc‘d老狀態(tài)下的條件c新狀態(tài)下的條件c形式化SCR：事件例@T(Block=On)WHENReset=OffBlockOnBlock’=OnReset=Off形式化SCR：系統(tǒng)模型一個系統(tǒng)為一個四元組：Em輸入事件的集合S可能的系統(tǒng)狀態(tài)的集合s0初始狀態(tài)T系統(tǒng)變換，為Em

S到S上的一個部分函數(shù)，表示被允許的系統(tǒng)狀態(tài)變遷形式化SCR：系統(tǒng)模型假設(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)依賴集監(jiān)測變量的新狀態(tài)依賴集為空由條件表定義的實體，其新狀態(tài)依賴集包含所關(guān)聯(lián)的模式類名，和出現(xiàn)在條件表中的所有實體名由事件表或模式變遷表定義的實體，其新狀態(tài)依賴集包含出現(xiàn)在表中作為一個基本事件的一部分的所有實體新狀態(tài)依賴集構(gòu)成了RF上的一個偏序關(guān)系SCR需求的表示條件表描述從模式和條件到控制變量或項上的一個函數(shù)函數(shù)表示形式：模式條件控制變量的取值|項的取值當(dāng)前模式條件High,PermittedTrueFalseTooLowOverriddenOverriddenSafetyInjectionOffOnSafetyInjection在新狀態(tài)中依賴模式類Pressure和項OverriddenSCR需求的表示模式變遷表：定義軟件可以處于的模式（狀態(tài)）及其模式變遷一個系統(tǒng)將包含不同的模式類，每個模式類有一個模式表，展示引起模式之間的變遷的條件函數(shù)表示形式：模式事件模式當(dāng)前模式事件下一模式TooLow@T(WaterPress≥Low)PermittedPermitted@T(WaterPress≥Permit)HighPermitted@T(WaterPress<Low)TooLowHigh@T(WaterPress<Permit)Permitted模式類Pressure在新狀態(tài)中依賴WaterPressSCR需求的表示事件表描述從模式和事件到控制變量或項的取值上的一個函數(shù)函數(shù)表示形式：模式事件控制變量的取值|項的取值當(dāng)前模式事件HighFalse@T(Inmode)TooLow,Permitted@T(Block=On)WHENReset=Off@T(Inmode)@T(Reset=On)OverriddenTrueFalseOverridden在新狀態(tài)中依賴模式類Pressure和監(jiān)測變量Block和Reset偏序關(guān)系序列一種可能性：R=<WaterPress,Block,Reset,Pressure,Overridden,SafetyInjection>表函數(shù)：條件表當(dāng)前模式條件High,PermittedTrueFalseTooLowOverriddenOverriddenSafetyInjectionOffOn表函數(shù)：事件表當(dāng)前模式事件下一模式TooLow@T(WaterPress≥Low)PermittedPermitted@T(WaterPress≥Permit)HighPermitted@T(WaterPress<Low)TooLowHigh@T(WaterPress<Permit)Permitted表函數(shù)：事件表表函數(shù)：變遷表當(dāng)前模式事件下一模式TooLow@T(WaterPress≥Low)PermittedPermitted@T(WaterPress≥Permit)HighPermitted@T(WaterPress<Low)TooLowHigh@T(WaterPress<Permit)Permitted表函數(shù)：變遷表自動一致性檢查合適的語法類型正確性變量和模式定義的完整性初始值：模式類、輸入變量、輸出變量可達性：模式類忠的每個模式都是初始模式靜態(tài)可達的互斥性：條件相互之間是互斥的