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

需求工程金芝中國科學(xué)院數(shù)學(xué)與系統(tǒng)科學(xué)研究院zhijin@第九講：文檔驅(qū)動(dòng)方法需求文檔的重要性四變量模型SCR需求方法形式化SCR和表演算機(jī)制總結(jié)從軟件工程師的職責(zé)談起工程師的職責(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)品缺陷的爭論……沒有文檔，任何工程師做不到這一點(diǎn)發(fā)現(xiàn)需求是一門藝術(shù)，文檔化需求并驗(yàn)證它的完整性是一門學(xué)科好文檔的作用可以描述已經(jīng)存在的軟件——我們可以不用讀代碼就能夠回答關(guān)于該軟件的問題可以描述還不存在的軟件——程序員和客戶可以就需求達(dá)成一致意見驗(yàn)證產(chǎn)品是否滿足需求（測(cè)試和/或?qū)彶椋┛梢越⒐ぞ邫z查規(guī)格說明可以建立工具模擬系統(tǒng)并檢查系統(tǒng)文檔可接受的標(biāo)準(zhǔn)描述必須比代碼容易理解文檔必須用一種不限制解決方案的方式陳述需求測(cè)試和證明最終能夠自動(dòng)化程序與其它工程產(chǎn)品不同嗎？在計(jì)算機(jī)出現(xiàn)之前，工程師使用經(jīng)典數(shù)學(xué)來描述和分析產(chǎn)品在計(jì)算機(jī)科學(xué)中，大多數(shù)研究者發(fā)明新的“語言”我們將軟件作為產(chǎn)品來開發(fā)程序與其它工程產(chǎn)品不同嗎？我們?yōu)槭裁床荒芎唵蔚赜梦覀兞?xí)慣的數(shù)學(xué)來建模？傳統(tǒng)產(chǎn)品是無生命的東西（X）我們需要描述被程序遵循的過程（X）功能不是連續(xù)的（√）需求階段的目的容許人員的更替為質(zhì)量保證組提供參考文檔測(cè)試設(shè)計(jì)不應(yīng)該以來程序授權(quán)的需要——質(zhì)量保證組和程序員可能不一致說明實(shí)現(xiàn)相關(guān)的所有約束知道你面臨什么為應(yīng)付客戶的變化提供某種形式的保護(hù)能夠評(píng)判可行性和代價(jià)說明未來修訂的約束四變量模型在系統(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ù)輸入和輸出變量軟件需求使用輸入和輸出變量來描述四變量模型的關(guān)系整個(gè)系統(tǒng)：滿足監(jiān)視變量和控制變量之間的關(guān)系輸入設(shè)備：滿足監(jiān)視變量和輸入變量之間的關(guān)系輸出設(shè)備：滿足輸出變量和控制變量之間的關(guān)系軟件系統(tǒng)：滿足輸入設(shè)備和輸出設(shè)備之間的關(guān)系識(shí)別和聲明監(jiā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ì)算機(jī)屏幕上看到的東西什么將出現(xiàn)在帳單上定義變量之間的關(guān)系NAT關(guān)系：mtctmt：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)系：mtctmt：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)系滿足的條件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時(shí)刻的取值it：c在t時(shí)刻的取值(mt,it)IN當(dāng)且僅當(dāng)在mt描述的環(huán)境監(jiān)視量下輸入設(shè)備正常工作時(shí)可能產(chǎn)生的值OUT關(guān)系：otctot：m在t時(shí)刻的取值ct：c在t時(shí)刻的取值(ot,ct)OUT當(dāng)且僅當(dāng)輸出設(shè)備正常工作時(shí)并輸出ot描述的取值時(shí)可能的環(huán)境控制量的取值軟件需求文檔的檢查完整包含上述內(nèi)容驗(yàn)證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四變量模型蘊(yùn)涵的需求過程說明系統(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需求方法SCR：SoftwareCostReduction提出：Heninger,K.L.,80年代初期成功應(yīng)用領(lǐng)域：A-7操作飛行程序潛水艇通訊系統(tǒng)加拿大Darlington核電站安全組件Lockheed’sC-130j操作飛行程序基本概念和表示法構(gòu)造子一：模式類定義在被監(jiān)護(hù)變量上一個(gè)狀態(tài)機(jī)其中的狀態(tài)稱為系統(tǒng)模式變遷由事件觸發(fā)模式類刻畫了系統(tǒng)運(yùn)行的一段相互關(guān)聯(lián)的上下文主要目的是劃分狀態(tài)集合，簡化函數(shù)的描述基本概念和表示法構(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)刻畫系統(tǒng)某個(gè)特定可度量時(shí)期的某方面的性質(zhì)當(dāng)一個(gè)條件的值從真變?yōu)榧?，或者從假變?yōu)檎?，就發(fā)生一個(gè)事件。從這個(gè)意義上說，條件主要用于刻畫事件發(fā)生的時(shí)機(jī)案例：安全注入系統(tǒng)基本需求：負(fù)責(zé)打開和關(guān)閉安全注入閥。需要監(jiān)測(cè)水壓，當(dāng)水壓低于閾值以下時(shí)，打開注入閥，向反應(yīng)堆內(nèi)核填加冷凍劑系統(tǒng)操作員可以用‘Block’（或‘Reset’）開關(guān)阻止安全注入（或恢復(fù)安全注入）安全注入系統(tǒng)：SCR需求Overridden：表示安全噴射被阻止三個(gè)被監(jiān)測(cè)量每個(gè)感應(yīng)器產(chǎn)生一個(gè)輸入量被控制的量兩個(gè)模式類重載三個(gè)系統(tǒng)模式安全注入系統(tǒng)：SCR需求系統(tǒng)有兩個(gè)模式類：“壓力”模式“重載”模式模式類“壓力”中有三個(gè)系統(tǒng)模式：壓力太低，WaterPress=<Low允許的范圍，Low<WaterPress=<Permit壓力高，Permit<WaterPressSCR需求的表示模式變遷表：定義軟件可以處于的模式（狀態(tài)）及其模式變遷一個(gè)系統(tǒng)將包含不同的模式類，每個(gè)模式類有一個(gè)模式表，展示引起模式之間的變遷的條件函數(shù)表示形式：模式事件模式當(dāng)前模式事件下一模式TooLow@T(WaterPress≥Low)PermittedPermitted@T(WaterPress≥Permit)HighPermitted@T(WaterPress<Low)TooLowHigh@T(WaterPress<Permit)PermittedSCR需求的表示事件表描述從模式和事件到控制變量或項(xiàng)的取值上的一個(gè)函數(shù)函數(shù)表示形式：模式事件控制變量的取值|項(xiàng)的取值當(dāng)前模式事件HighFalse@T(Inmode)TooLow,Permitted@T(Block=On)WHENReset=Off@T(Inmode)@T(Reset=On)OverriddenTrueFalseSCR需求的表示條件表描述從模式和條件到控制變量或項(xiàng)上的一個(gè)函數(shù)函數(shù)表示形式：模式條件控制變量的取值|項(xiàng)的取值當(dāng)前模式條件High,PermittedTrueFalseTooLowOverriddenOverriddenSafetyInjectionOffOnSCR需求定義過程生成系統(tǒng)需求規(guī)范SRS確定并描述控制變量C；確定并描述監(jiān)視變量M；確定并描述系統(tǒng)模式類；定義關(guān)系REQ；生成系統(tǒng)設(shè)計(jì)規(guī)范SDS確定并描述輸入和輸出變量；定義輸入/輸出變量和監(jiān)視/控制變量之間的關(guān)系；生成軟件需求規(guī)范SoRS定義關(guān)系D_IN和D_OUT；對(duì)SRS進(jìn)行擴(kuò)充，增加諸如系統(tǒng)在硬件失效時(shí)的行為等需求定義硬件失效時(shí)行為；對(duì)每個(gè)控制變量增加時(shí)序約束；把關(guān)系REQ擴(kuò)展為關(guān)系。SCR需求中各類關(guān)系形式化SCR：基礎(chǔ)基礎(chǔ)命名：模式集合（MS=Mi）實(shí)體名集合（RF=MRIRORGR）實(shí)體取值的集合（VS=MSTS）數(shù)據(jù)類型集合（TS）TY：函數(shù)，系統(tǒng)實(shí)體該實(shí)體的合法值TY：RFVS模式類名集合輸入變量名集合輸出變量名集合項(xiàng)名集合安全注入系統(tǒng)：SCR需求Overridden：表示安全噴射被阻止三個(gè)被監(jiān)測(cè)量每個(gè)感應(yīng)器產(chǎn)生一個(gè)輸入量被控制的量兩個(gè)模式類重載三個(gè)系統(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)測(cè)事件：@T(r=v),rIR,vTY(r)基本事件：@T(c),c是一個(gè)簡單條件簡單條件事件：@T(c)WHENd,@T(c)是一個(gè)基本事件，d是一個(gè)簡單條件或者復(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)模型一個(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)變遷形式化SCR：系統(tǒng)模型假設(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)必須全部完成實(shí)體排序構(gòu)造實(shí)體的新狀態(tài)依賴集監(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)系SCR需求的表示條件表描述從模式和條件到控制變量或項(xiàng)上的一個(gè)函數(shù)函數(shù)表示形式：模式條件控制變量的取值|項(xiàng)的取值當(dāng)前模式條件High,PermittedTrueFalseTooLowOverriddenOverriddenSafetyInjectionOffOnSafetyInjection在新狀態(tài)中依賴模式類Pressure和項(xiàng)OverriddenSCR需求的表示模式變遷表：定義軟件可以處于的模式（狀態(tài)）及其模式變遷一個(gè)系統(tǒng)將包含不同的模式類，每個(gè)模式類有一個(gè)模式表，展示引起模式之間的變遷的條件函數(shù)表示形式：模式事件模式當(dāng)前模式事件下一模式TooLow@T(WaterPress≥Low)PermittedPermitted@T(WaterPress≥Permit)HighPermitted@T(WaterPress<Low)TooLowHigh@T(WaterPress<Permit)Permitted模式類Pressure在新狀態(tài)中依賴WaterPressSCR需求的表示事件表描述從模式和事件到控制變量或項(xiàng)的取值上的一個(gè)函數(shù)函數(shù)表示形式：模式事件控制變量的取值|項(xiàng)的取值當(dāng)前模式事件HighFalse@T(Inmode)TooLow,Permitted@T(Block=On)WHENReset=Off@T(Inmode)@T(Reset=On)OverriddenTrueFalseOverridden在新狀態(tài)中依賴模式類Pressure和監(jiān)測(cè)變量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ù)：變遷表自動(dòng)一致性檢查合適的語法類型正確性變量和模式定義的完整性初始值：模式類、輸入變量、輸出變量可達(dá)性：模式類忠的每個(gè)模式都是初始模式靜態(tài)可達(dá)的互斥性：條件相互之間是互斥的