第4章形式化說明技術ppt課件

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

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

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

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

5、：保險箱解鎖，報警。：保險箱解鎖，報警。tjm運用更方式化的術語，一個有窮形狀機可以表示為一個5元組(J，K，T，S，F(xiàn))，其中：J是一個有窮的非空形狀集；K是一個有窮的非空輸入集；T是一個從(J-F)K到J的轉(zhuǎn)換函數(shù)；SJ，是一個初始形狀；FJ，是終態(tài)集。 tjm Petri網(wǎng)簡稱網(wǎng)簡稱PNG (Petri Net Graph) Petri網(wǎng)已廣泛地運用于硬件與軟件系統(tǒng)的網(wǎng)已廣泛地運用于硬件與軟件系統(tǒng)的開發(fā)中，它適用于描畫與分析相互獨立、開發(fā)中，它適用于描畫與分析相互獨立、協(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 有向邊有向邊 ：表示對轉(zhuǎn)換的輸：表示對轉(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兩個用于轉(zhuǎn)換的輸入函數(shù)：兩個用于轉(zhuǎn)換的輸入函數(shù)：I(t1)=P2，P4I(t2)=P2兩個用于轉(zhuǎn)換的輸出函數(shù)：兩個用于轉(zhuǎn)換的輸出函數(shù)：O(t1)=P1O(t2)=P3，P3tjm更方式化的

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

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

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

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