第4章形式化說(shuō)明技術(shù)ppt課件

1、tjm4.1 概述概述4.2 有窮形狀機(jī)有窮形狀機(jī)4.3 Petri網(wǎng)網(wǎng)4.4 Z言語(yǔ)言語(yǔ)tjmw按照方式化的程度劃分軟件工程運(yùn)用的方法：按照方式化的程度劃分軟件工程運(yùn)用的方法：w非方式化非方式化w半方式化半方式化w方式化方式化w方式化方法定義：方式化方法定義：w 是描畫(huà)系統(tǒng)性質(zhì)的、基于數(shù)學(xué)的技術(shù)。是描畫(huà)系統(tǒng)性質(zhì)的、基于數(shù)學(xué)的技術(shù)。tjm優(yōu)點(diǎn)優(yōu)點(diǎn)缺點(diǎn)缺點(diǎn)形式形式化方化方法法形式化的規(guī)格說(shuō)明可以用數(shù)學(xué)方形式化的規(guī)格說(shuō)明可以用數(shù)學(xué)方法研究、驗(yàn)證。法研究、驗(yàn)證。消除了二義性，鼓勵(lì)在軟件工程消除了二義性，鼓勵(lì)在軟件工程過(guò)程的早期階段使用更嚴(yán)格的方過(guò)程的早期階段使用更嚴(yán)格的方法，從而可以減少差錯(cuò)。法，從

2、而可以減少差錯(cuò)。主要關(guān)注于系統(tǒng)的主要關(guān)注于系統(tǒng)的功能和數(shù)據(jù)，而問(wèn)功能和數(shù)據(jù)，而問(wèn)題的時(shí)序、控制和題的時(shí)序、控制和行為等方面的需求行為等方面的需求卻更難于表示。卻更難于表示。復(fù)雜難學(xué)習(xí)。復(fù)雜難學(xué)習(xí)。欠形欠形式化式化方法方法簡(jiǎn)單易學(xué)。簡(jiǎn)單易學(xué)?？赡艽嬖诿?、二可能存在矛盾、二義性、含糊性、不義性、含糊性、不完整性及等問(wèn)題。完整性及等問(wèn)題。tjmw應(yīng)該選用適當(dāng)?shù)谋硎痉椒☉?yīng)該選用適當(dāng)?shù)谋硎痉椒╳應(yīng)該方式化，但不要過(guò)分方式化應(yīng)該方式化，但不要過(guò)分方式化w應(yīng)該估算本錢(qián)應(yīng)該估算本錢(qián)w應(yīng)該有方式化方法顧問(wèn)隨時(shí)提供咨詢應(yīng)該有方式化方法顧問(wèn)隨時(shí)提供咨詢w不應(yīng)該放棄傳統(tǒng)的開(kāi)發(fā)方法不應(yīng)該放棄傳統(tǒng)的開(kāi)發(fā)方法w應(yīng)該建立詳

3、盡的文檔應(yīng)該建立詳盡的文檔w不應(yīng)該放棄質(zhì)量規(guī)范不應(yīng)該放棄質(zhì)量規(guī)范w不應(yīng)該盲目依賴方式化方法不應(yīng)該盲目依賴方式化方法w應(yīng)該測(cè)試、測(cè)試再測(cè)試應(yīng)該測(cè)試、測(cè)試再測(cè)試w應(yīng)該重用應(yīng)該重用tjm例：一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)例：一個(gè)保險(xiǎn)箱上裝了一個(gè)復(fù)合鎖，鎖有三個(gè)位置，分別標(biāo)志為志為1、2、3，轉(zhuǎn)盤(pán)可向左，轉(zhuǎn)盤(pán)可向左(L)或向右或向右(R)轉(zhuǎn)動(dòng)。這樣，在轉(zhuǎn)動(dòng)。這樣，在恣意時(shí)辰轉(zhuǎn)盤(pán)都有恣意時(shí)辰轉(zhuǎn)盤(pán)都有6種能夠的運(yùn)動(dòng)，即種能夠的運(yùn)動(dòng)，即1L、1R、2L、2R、3L和和3R。保險(xiǎn)箱的組合密碼是。保險(xiǎn)箱的組合密碼是1L、3R、2L，轉(zhuǎn)盤(pán)的任何，轉(zhuǎn)盤(pán)的任何其他運(yùn)動(dòng)都將引起報(bào)警。其他運(yùn)動(dòng)都將引起報(bào)

4、警。保險(xiǎn)箱的形狀轉(zhuǎn)換圖保險(xiǎn)箱的形狀轉(zhuǎn)換圖tjm 有窮形狀機(jī)的組成包括有窮形狀機(jī)的組成包括5個(gè)部分：形狀集個(gè)部分：形狀集J、輸入集、輸入集K、由當(dāng)前形狀和當(dāng)前輸入確定下一個(gè)形狀、由當(dāng)前形狀和當(dāng)前輸入確定下一個(gè)形狀(次態(tài)次態(tài))的轉(zhuǎn)換函數(shù)的轉(zhuǎn)換函數(shù)T、初始態(tài)、初始態(tài)S和終態(tài)集和終態(tài)集F。保險(xiǎn)箱的有窮形狀機(jī)的各部分如下：保險(xiǎn)箱的有窮形狀機(jī)的各部分如下：形狀集形狀集J：保險(xiǎn)箱鎖定，：保險(xiǎn)箱鎖定，A，B，保險(xiǎn)箱解鎖，報(bào)，保險(xiǎn)箱解鎖，報(bào)警。警。輸入集輸入集K：1L，1R，2L，2R，3L，3R。轉(zhuǎn)換函數(shù)轉(zhuǎn)換函數(shù)T：見(jiàn)書(shū)：見(jiàn)書(shū)P68表表4.1所示。所示。初始態(tài)初始態(tài)S：保險(xiǎn)箱鎖定。：保險(xiǎn)箱鎖定。終態(tài)集終態(tài)集F

5、：保險(xiǎn)箱解鎖，報(bào)警。：保險(xiǎn)箱解鎖，報(bào)警。tjm運(yùn)用更方式化的術(shù)語(yǔ)，一個(gè)有窮形狀機(jī)可以表示為一個(gè)5元組(J，K，T，S，F(xiàn))，其中：J是一個(gè)有窮的非空形狀集；K是一個(gè)有窮的非空輸入集；T是一個(gè)從(J-F)K到J的轉(zhuǎn)換函數(shù)；SJ，是一個(gè)初始形狀；FJ，是終態(tài)集。 tjm Petri網(wǎng)簡(jiǎn)稱網(wǎng)簡(jiǎn)稱PNG (Petri Net Graph) Petri網(wǎng)已廣泛地運(yùn)用于硬件與軟件系統(tǒng)的網(wǎng)已廣泛地運(yùn)用于硬件與軟件系統(tǒng)的開(kāi)發(fā)中，它適用于描畫(huà)與分析相互獨(dú)立、開(kāi)發(fā)中，它適用于描畫(huà)與分析相互獨(dú)立、協(xié)同操作的處置系統(tǒng)，也就是并發(fā)執(zhí)行的協(xié)同操作的處置系統(tǒng)，也就是并發(fā)執(zhí)行的處置系統(tǒng)。處置系統(tǒng)。 Petri網(wǎng)包含網(wǎng)包含4種

6、元素：種元素：一組位置一組位置P 圓圈圓圈 ：表示系統(tǒng)的形狀：表示系統(tǒng)的形狀一組轉(zhuǎn)換一組轉(zhuǎn)換T 短直線短直線 ：表示系統(tǒng)中的事：表示系統(tǒng)中的事件件輸入函數(shù)輸入函數(shù)I 有向邊有向邊 ：表示對(duì)轉(zhuǎn)換的輸：表示對(duì)轉(zhuǎn)換的輸入入輸出函數(shù)輸出函數(shù)O 有向邊有向邊 ：表示由轉(zhuǎn)換的輸：表示由轉(zhuǎn)換的輸出出tjmPetri網(wǎng)的組成例如：網(wǎng)的組成例如：tjm一組位置一組位置P為為P1，P2，P3，P4一組轉(zhuǎn)換一組轉(zhuǎn)換T為為t1，t2兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)：兩個(gè)用于轉(zhuǎn)換的輸入函數(shù)：I(t1)=P2，P4I(t2)=P2兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)：兩個(gè)用于轉(zhuǎn)換的輸出函數(shù)：O(t1)=P1O(t2)=P3，P3tjm更方式化的

7、更方式化的Petri網(wǎng)構(gòu)造，是一個(gè)四元組網(wǎng)構(gòu)造，是一個(gè)四元組C=(P,T,I,O)。其中，其中，P=P1，Pn是一個(gè)有窮位置集，是一個(gè)有窮位置集，n0。T=t1，tm是一個(gè)有窮轉(zhuǎn)換集，是一個(gè)有窮轉(zhuǎn)換集，m0，且且T和和P不相交。不相交。I：TP為輸入函數(shù)，是由轉(zhuǎn)換到位置無(wú)序單位為輸入函數(shù)，是由轉(zhuǎn)換到位置無(wú)序單位組的映射。組的映射。O：TP為輸出函數(shù)，是由轉(zhuǎn)換到位置無(wú)序單位為輸出函數(shù)，是由轉(zhuǎn)換到位置無(wú)序單位組的映射。組的映射。一個(gè)無(wú)序單位組或多重組是允許一個(gè)元素有多個(gè)實(shí)一個(gè)無(wú)序單位組或多重組是允許一個(gè)元素有多個(gè)實(shí)例的廣義集。例的廣義集。tjm帶標(biāo)志的帶標(biāo)志的Petri網(wǎng)：網(wǎng)：Petri網(wǎng)的標(biāo)志是

8、在網(wǎng)的標(biāo)志是在Petri網(wǎng)中權(quán)網(wǎng)中權(quán)標(biāo)標(biāo)(token)的分配。的分配。權(quán)標(biāo)：或叫令牌權(quán)標(biāo)：或叫令牌(token)w例：例：tjm轉(zhuǎn)換轉(zhuǎn)換 t2被激發(fā)后的情況：被激發(fā)后的情況：轉(zhuǎn)換轉(zhuǎn)換 t1被激發(fā)后的情況：被激發(fā)后的情況：tjm例：處置兩個(gè)進(jìn)程的同步問(wèn)題例：處置兩個(gè)進(jìn)程的同步問(wèn)題tjmtjmw例：例：含制止線的含制止線的Petri網(wǎng)：當(dāng)每個(gè)輸入線上至少有一網(wǎng)：當(dāng)每個(gè)輸入線上至少有一個(gè)權(quán)標(biāo)，而制止線上沒(méi)有權(quán)標(biāo)的時(shí)候，相應(yīng)的轉(zhuǎn)個(gè)權(quán)標(biāo)，而制止線上沒(méi)有權(quán)標(biāo)的時(shí)候，相應(yīng)的轉(zhuǎn)換才是允許的。換才是允許的。轉(zhuǎn)換轉(zhuǎn)換t1可以被激發(fā)可以被激發(fā)tjm 用用Z言語(yǔ)描畫(huà)的、最簡(jiǎn)單的方式化規(guī)格闡明含有言語(yǔ)描畫(huà)的、最簡(jiǎn)單的方

9、式化規(guī)格闡明含有4個(gè)部分：個(gè)部分：給定的集合、數(shù)據(jù)類型及常數(shù)給定的集合、數(shù)據(jù)類型及常數(shù)形狀定義形狀定義初始形狀初始形狀操作操作tjm 1. 給定的集合給定的集合 一個(gè)一個(gè)Z規(guī)格闡明從一系列給定的初始化集合不規(guī)格闡明從一系列給定的初始化集合不需求詳細(xì)定義的集合開(kāi)場(chǎng)。需求詳細(xì)定義的集合開(kāi)場(chǎng)。 這種集合用帶方括號(hào)的方式表示。這種集合用帶方括號(hào)的方式表示。 例：對(duì)于電梯問(wèn)題，給定的初始化集合稱為例：對(duì)于電梯問(wèn)題，給定的初始化集合稱為Button，即一切按鈕的集合：，即一切按鈕的集合： Button tjm 2. 形狀定義形狀定義 一個(gè)一個(gè)Z規(guī)格闡明由假設(shè)干個(gè)規(guī)格闡明由假設(shè)干個(gè)“格格(schema)組組

10、成，每個(gè)格含有一組變量闡明和一系列限定變量成，每個(gè)格含有一組變量闡明和一系列限定變量取值范圍的謂詞。取值范圍的謂詞。 例：tjm3. 初始形狀初始形狀指系統(tǒng)第一次開(kāi)啟時(shí)的形狀。指系統(tǒng)第一次開(kāi)啟時(shí)的形狀。例：對(duì)于電梯問(wèn)題來(lái)說(shuō)：例：對(duì)于電梯問(wèn)題來(lái)說(shuō)：Button_InitButton_Statepushed=上式表示，當(dāng)系統(tǒng)初次開(kāi)啟時(shí)上式表示，當(dāng)系統(tǒng)初次開(kāi)啟時(shí)pushed集為空，即集為空，即一切按鈕都處于封鎖形狀。一切按鈕都處于封鎖形狀。 tjm4. 操作操作例：假設(shè)一個(gè)原來(lái)處于封鎖形狀的按鈕被按下，那例：假設(shè)一個(gè)原來(lái)處于封鎖形狀的按鈕被按下，那么該按鈕開(kāi)啟，這個(gè)按鈕就被添加到么該按鈕開(kāi)啟，這個(gè)按鈕就被添加到pushed