軟件工程導(dǎo)論梁文新辦公室：綜合樓108電

話：87571625wxliang@10/19/20221liang@第四章形式化說明技術(shù)(FormalDescriptionTechnique，F(xiàn)DT)4.1概述4.2有窮狀態(tài)機(FSM/FSA)4.3Petri網(wǎng)(PetriNets)4.4Z語言(ZNotation)4.5小結(jié)10/19/20222liang@4.1概述按照形式化的程度，可以把軟件工程使用的方法劃分成非形式化、半形式化和形式化三類非形式化方法(Informal)用自然語言描述需求規(guī)格說明半形式化方法(Semi-formal)用數(shù)據(jù)流圖或?qū)嶓w-聯(lián)系圖建立模型形式化方法(Formal)是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)即如果一種方法有堅實的數(shù)學(xué)基礎(chǔ)，那么它就是形式化的10/19/20223liang@4.1概述4.1.1非形式化方法的缺點矛盾：相互沖突的陳述二義性：讀者可以用不同的方式理解的陳述含糊：籠統(tǒng)的陳述不完整性：最常遇到的問題抽象層次混亂：非常抽象的陳述中混進了一些關(guān)于細(xì)節(jié)的低層次陳述10/19/20224liang@4.1概述4.1.2形式化方法的優(yōu)點把數(shù)學(xué)引入軟件開發(fā)過程，形成基于數(shù)學(xué)的形式化方法數(shù)學(xué)最有用的一個性質(zhì)是，能夠簡潔準(zhǔn)確地描述物理現(xiàn)象、對象或動作的結(jié)果，因此是理想的建模工具。數(shù)學(xué)特別適合于表示狀態(tài)，也就是表示“做什么”在理想情況下，分析員可以寫出不含二義性的系統(tǒng)的數(shù)學(xué)規(guī)格說明，并可用數(shù)學(xué)方法對其進行驗證，以發(fā)現(xiàn)存在的矛盾和不完整性，在這樣的規(guī)格說明中完全沒有含糊性事實上復(fù)雜的軟件系統(tǒng)通常難以用幾個數(shù)學(xué)公式來描述在軟件開發(fā)過程中使用數(shù)學(xué)，可以在不同的軟件工程活動之間平滑地過渡（系統(tǒng)規(guī)格說明、系統(tǒng)設(shè)計、程序代碼）提供了高層確認(rèn)的手段可以使用數(shù)學(xué)方法證明，設(shè)計符合規(guī)格說明，程序代碼正確地實現(xiàn)了設(shè)計結(jié)果10/19/20225liang@4.1概述4.1.3應(yīng)用形式化方法的準(zhǔn)則應(yīng)該建立詳盡的文檔用自然語言注釋形式化的規(guī)格說明書不應(yīng)該放棄質(zhì)量標(biāo)準(zhǔn)形式化方法并不能完全確保軟件的正確性不應(yīng)該盲目依賴形式化方法無法用形式化方法證明從非形式化需求到形式化規(guī)格說明的轉(zhuǎn)換是正確的，因此，必須用其他方法(例如，評審、測試)來驗證軟件正確性應(yīng)該測試、測試再測試應(yīng)該重用10/19/20227liang@4.2有窮狀態(tài)機(FSM/FSA)4.2.1概念FSM(Finite-StateMachine)/FSA(Finite-StateAutomaton)isamodelofbehaviorcomposedofafinitenumberofstates,transitionsbetweenthosestates,andactions一個保險箱上裝了一個復(fù)合鎖，鎖有3個位置，分別標(biāo)記為1、2、3，轉(zhuǎn)盤可向左（L）或向右（R）轉(zhuǎn)動這樣，任何時刻轉(zhuǎn)盤都有6種可能的運動，即1L、1R、2L、2R、3L、3R保險箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤的任何其他運動都將引起報警10/19/20228liang@StateTransitionTable10/19/202210liang@FSM/FSA的數(shù)學(xué)模型FSM可以表示為一個5元組（J，K，T，S，F(xiàn)）狀態(tài)集J(finite,non-emptysetofstates)：{保險箱鎖定，A，B，保險箱解鎖，報警}輸入集K(finite,non-emptysetofinput)：{1L、1R、2L、2R、3L、3R}初始態(tài)S(initialstate,anelementofJ,i.e.S∈J)：保險箱鎖定終態(tài)集F(finalstates,a(possiblyempty)subsetofJ,FJ)：{保險箱解鎖，報警}轉(zhuǎn)換函數(shù)T(state-transitionfunction,(J-F)*KJ)：如表4.1所示10/19/202211liang@FSM/FSA的數(shù)學(xué)模型加入謂詞集P，把有窮狀態(tài)機擴展為一個6元組，其中每個謂詞都是系統(tǒng)全局狀態(tài)Y的函數(shù)則轉(zhuǎn)換函數(shù)T：（J-F）*K*PJ10/19/202212liang@4.2有窮狀態(tài)機(FSM/FSA)電梯按鈕EB（e，f）：按下電梯e內(nèi)的按鈕并請求到f層去狀態(tài)：EBON（e，f）：電梯按鈕（e，f）打開EBOFF（e，f）：電梯按鈕（e，f）關(guān)閉事件EBP（e，f）：電梯按鈕（e，f）被按下EAF（e，f）：電梯到達(dá)f層謂詞V（e，f）：電梯e停在f層10/19/202214liang@4.2有窮狀態(tài)機(FSM/FSA)圖4.2電梯按鈕的狀態(tài)轉(zhuǎn)換圖10/19/202215liang@4.2有窮狀態(tài)機(FSM/FSA)圖4.3樓層按鈕的狀態(tài)轉(zhuǎn)換圖10/19/202217liang@4.2有窮狀態(tài)機(FSM/FSA)電梯狀態(tài)M（d，e，f）：電梯e正沿d方向移動，即將到達(dá)的是第f層S（d，e，f）：電梯e停在f層，將朝d方向移動（尚未關(guān)門）W（e，f）：電梯e在f層等待（已關(guān)門）事件DC（e，f）：電梯e在樓層f關(guān)上門ST（e，f）：電梯e靠近f層時觸發(fā)傳感器，電梯控制器決定在當(dāng)前樓層電梯是否停下RL（e，f）：f層的電梯按鈕或樓層按鈕被按下進入打開狀態(tài)，登錄需求10/19/202218liang@4.2有窮狀態(tài)機(FSM/FSA)圖4.4電梯的狀態(tài)轉(zhuǎn)換圖關(guān)門之時的規(guī)則10/19/202219liang@思考題定義開門狀態(tài)O（e，f）：電梯e在f層開門，則如何由移動或等待進入這個狀態(tài)？如何從等待進入到向上或向下移動狀態(tài)？10/19/202220liang@4.2有窮狀態(tài)機(FSM/FSA)4.2.3評價有窮狀態(tài)機描述規(guī)格說明：當(dāng)前狀態(tài)+事件(+謂詞)下個狀態(tài)優(yōu)點：易于書寫、易于驗證、精確、易于理解可開發(fā)出CASE工具直接將規(guī)格說明轉(zhuǎn)變?yōu)榇a缺點：開發(fā)大系統(tǒng)時三元組的數(shù)量會迅速增長無法處理定時需求（同步，競爭，死鎖）10/19/202221liang@4.3Petri網(wǎng)4.3.1概述并發(fā)系統(tǒng)中遇到的一個主要問題是定時問題:同步、競爭、死鎖Petri網(wǎng)是一種用于確定系統(tǒng)中隱含的定時問題的一種有效技術(shù)，可有效的描述并發(fā)活動10/19/202222liang@4.3Petri網(wǎng)包含元素位置P{P1，P2，P3，P4}轉(zhuǎn)換T{t1，t2}圖4.5Petri網(wǎng)的組成輸入函數(shù)II（t1）={P2，P4}I（t2）={P2}輸出函數(shù)OO（t1）={P1}O（t2）={P3，P3}placetransitionarcweightInputOutput10/19/202224liang@4.3Petri網(wǎng)更形式化的Petri網(wǎng)結(jié)構(gòu)，是一個四元組C=（P，T，I，O）其中，P={P1，…，Pn}是一個有窮位置集，n>=0T={t1，…，tm}是一個有窮轉(zhuǎn)換集，m>=0，且T和P不相交。I：為輸入函數(shù)，是由轉(zhuǎn)換到位置無序單位組(bags)的映射。O：為輸出函數(shù)，是由轉(zhuǎn)換到位置無序單位組的映射。10/19/202225liang@Firingexample2H2+O2

2H2OH2O2H2Ot2210/19/202227liang@Firingexample2H2+O2

2H2OH2O2H2Ot2210/19/202228liang@4.3Petri網(wǎng)Petri網(wǎng)的標(biāo)記(marking)是在Petri網(wǎng)中權(quán)標(biāo)(token)的分配圖4.6帶標(biāo)記的Petri網(wǎng)（1，2，0，1）圖4.7圖4.6的Petri網(wǎng)在轉(zhuǎn)換t1被激發(fā)后的情況（2，1，0，0）圖4.8圖4.7的Petri網(wǎng)在轉(zhuǎn)換t2被激發(fā)后的情況（2，0，2，0）10/19/202229liang@4.3Petri網(wǎng)對Petri網(wǎng)的一個重要擴充是加入禁止線禁止線是用一個小圓圈而不是用箭頭標(biāo)記的輸入線通常，當(dāng)每個輸入線上至少有一個令牌，而禁止線上沒有令牌的時候，相應(yīng)的轉(zhuǎn)換才是允許的圖4.9含禁止線的Petri網(wǎng)10/19/202230liang@4.3Petri網(wǎng)4.3.2例子每個樓層用一個位置Ff代表(1≤f≤m)電梯是用一個權(quán)標(biāo)代表,在位置Ff上有權(quán)標(biāo)，表示在樓層f上有電梯10/19/202231liang@4.3Petri網(wǎng)1.電梯按鈕電梯中樓層f的按鈕，在Petri網(wǎng)中用位置EBf表示(1≤f≤m)。在EBf上有一個令牌，就表示電梯內(nèi)樓層f的按鈕被按下了10/19/202232liang@4.3Petri網(wǎng)2.樓層按鈕在Petri網(wǎng)中樓層按鈕用位置和表示，分別代表f樓層請求電梯上行和下行的按鈕10/19/202233liang@思考題1上下兩個按鈕同時按下時，電梯到達(dá)時如何正確讓相應(yīng)的按鈕熄滅？g<fg>f10/19/202234liang@思考題2VendingMachineRequirementsThemachinedispensesonlytwosnackbarproducts20c15cThemachineacceptsonlytwokindsofchange10c5cThemachinedoesnotreturnanychange10/19/202235liang@思考題2參考答案5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202236liang@Scenario1：Deposit5c,deposit5c,deposit5c,deposit5c,take20csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202237liang@Scenario1：Deposit5c,deposit5c,deposit5c,deposit5c,take20csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202238liang@Scenario1：Deposit5c,deposit5c,deposit5c,deposit5c,take20csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202239liang@Scenario1：Deposit5c,deposit5c,deposit5c,deposit5c,take20csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202240liang@Scenario1：Deposit5c,deposit5c,deposit5c,deposit5c,take20csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202241liang@Scenario1：Deposit5c,deposit5c,deposit5c,deposit5c,take20csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202242liang@Scenario2：Deposit10c,deposit5c,take15csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202243liang@Scenario2：Deposit10c,deposit5c,take15csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202244liang@Scenario2：Deposit10c,deposit5c,take15csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202245liang@Scenario2：Deposit10c,deposit5c,take15csnackbar5cTake15cbarDeposit5c0cDeposit10cDeposit5c10cDeposit10cDeposit5cDeposit10c20cDeposit5c15cTake20cbar10/19/202246liang@ReferencesTadaoMurata.“Petrinets:Properties,AnalysisandApplications.”Proc.oftheIEEE,77(4),1989./PUBLIC_A_to_O/LiangWenxin_Public/SoftwareEngineering/References10/19/202247liang@4.4Z語言(ZNotation)4.4.1簡介20世紀(jì)70年代由曾在牛津大學(xué)的ComputingLaboratory的ProgrammingResearchGroup工作的法國科學(xué)家J.R.Abrial首次提出和其他地方的程序設(shè)計研究組開發(fā)出Z語言，它基于集合理論和一階謂詞邏輯“Z”得名于集合論的鼻祖，德國著名數(shù)學(xué)家Zermelo(1871-1953),“Z”讀作/z?d/用Z語言描述的最簡單的形式化規(guī)格說明含有下述4個部分給定的集合、數(shù)據(jù)類型及常數(shù)狀態(tài)定義初始狀態(tài)操作10/19/202248liang@4.4Z語言(ZNotation)1.給定的集合Z規(guī)格說明從一系列給定的初始化集合開始即不需要詳細(xì)定義的集合，這種集合用帶方括號的形式表示電梯問題中所有按鈕的集合：〔Button〕10/19/202249liang@4.4Z語言(ZNotation)2.狀態(tài)定義一個Z規(guī)格說明由若干個“格(schema)”組成，每個格由格的名稱(schemaname)、一組變量說明(schemasignature)和一系列限定變量取值范圍的謂詞(schemapredicate/constraints)10/19/202250liang@4.4Z語言(ZNotation)圖4.13描述了格Button_State符號P表示冪集(即給定集的所有子集)約束條件聲明，floor_buttons集與elevator_buttons集不相交，且由它們共同組成buttons集圖4.13Z格Button_State10/19/202251liang@4.4Z語言(ZNotation)3.初始狀態(tài)抽