高級(jí)軟件工程(第5章：形式化開發(fā)方法1).ppt

第5章 形式化開發(fā)方法,形式化方法：是建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上，具有精確數(shù)學(xué) 表達(dá)形式和語義的開發(fā)方法。 其中：形式化方法的基本含義是借助數(shù)學(xué)的方法來研究軟 件工程中的有關(guān)問題。 特點(diǎn)： 1. 可以用數(shù)學(xué)方法進(jìn)行驗(yàn)證。如代數(shù)方法； 2. 可以用算法進(jìn)行識(shí)別和變換。 例如： 形式語言（BNF）、有限自動(dòng)機(jī)（FA）等是形式化方法 描述算法的程序流程圖、類pascal、類C等算法描述語言 則是非形式化方法。,形式化方法分類 1. 根據(jù)說明目標(biāo)軟件系統(tǒng)的方式，可以分為兩類： 1) 面向模型的形式化方法 通過構(gòu)造一個(gè)數(shù)學(xué)模型來說明系統(tǒng)的行為。 2) 面向?qū)傩缘男问交椒?通過描述目標(biāo)軟件系統(tǒng)的各種屬性來間接定義系統(tǒng)行為。 2. 根據(jù)表達(dá)能力，可以分為五類： 1) 基于模型的方法 給出系統(tǒng)狀態(tài)和狀態(tài)變換操作的顯式但亦是抽象的定義，即通 過定義系統(tǒng)狀態(tài)和操作建立系統(tǒng)模型。但對(duì)于并發(fā)沒有顯式的表 示。 如：Z語言，VDM，B方法等。 2) 基于邏輯的方法 用邏輯描述系統(tǒng)預(yù)期的性能，包括底層規(guī)約、時(shí)序和可能性行 為。采用與所選邏輯相關(guān)的公理系統(tǒng)證明系統(tǒng)具有預(yù)期的性能。 用具體的編程構(gòu)造擴(kuò)充邏輯從而得到一種廣譜形式化方法，通過 保持正確性的細(xì)化步驟集來開發(fā)系統(tǒng)。 如： ITL (區(qū)間時(shí)序邏輯), TAM (時(shí)序代理模型)，RTTL (實(shí)時(shí)時(shí)序邏輯)等,3) 代數(shù)方法 通過聯(lián)系不同操作間的行為關(guān)系而給出操作的顯式定 義，而不定義狀態(tài)，同樣它亦未給出并發(fā)的顯式表示. 如：OBJ，Clear，Larch族代數(shù)規(guī)約語言等 4) 進(jìn)程代數(shù)方法 給出并發(fā)過程的一個(gè)顯式模型，并通過進(jìn)程間允許的可觀察的通訊上的限制（約束）來表示行為. 如：CSP（通信順序過程） ACP（通信過程代數(shù)） CCS（通信并發(fā)系統(tǒng)/通信系統(tǒng)演算 ）等 5) 基于網(wǎng)絡(luò)的方法 該方法采用具有形式語義的圖形語言，根據(jù)網(wǎng)絡(luò)中的 數(shù)據(jù)流顯式地給出系統(tǒng)的行為模型，包括數(shù)據(jù)在網(wǎng)中從 一個(gè)結(jié)點(diǎn)流向另一個(gè)結(jié)點(diǎn)的條件、并發(fā)行等。 如：Petri 網(wǎng)、謂詞變換網(wǎng),Petri網(wǎng)的提出： 1962年由德國(guó)人C.A.Petri在他的博士 論文：“用自動(dòng)機(jī)通訊” (Communication with automata) 中首次提出的“網(wǎng)狀結(jié)構(gòu)的信息模型” 其中“有限自動(dòng)機(jī)Finite automata”定義為： FAA=（S，S0，F(xiàn)） 其中：S-狀態(tài)集 -字母表 -SS的映射 S0-開始狀態(tài)/狀態(tài)集 F-終止?fàn)顟B(tài)集 FAA可用三種方式描述： 集合法：定義方法； 矩陣法：狀態(tài)轉(zhuǎn)換矩陣/表 狀態(tài)圖法：狀態(tài)轉(zhuǎn)換圖,5. 1 Petri網(wǎng)概述,例子： 一個(gè)保險(xiǎn)箱上裝了一把復(fù)合鎖，鎖有三個(gè)位置，分別 標(biāo)記為1、2、3，轉(zhuǎn)盤可向左（L）或向右（R）轉(zhuǎn)動(dòng)。 這樣，在任意時(shí)刻轉(zhuǎn)盤都有6種可能的運(yùn)動(dòng)如下： L1、R1、L2、R2、L3、R3 保險(xiǎn)箱的組合密碼是： L1、R3、L2 轉(zhuǎn)盤的任何其他運(yùn)動(dòng)都將引起報(bào)警。,1,2,3,則保險(xiǎn)箱撥動(dòng)密碼的狀態(tài)轉(zhuǎn)換情況如DFA的狀態(tài)轉(zhuǎn)換圖所示：,其中：初態(tài) S：保險(xiǎn)箱鎖定 終態(tài) T：保險(xiǎn)箱解鎖 終態(tài) E：報(bào)警 符號(hào) ：轉(zhuǎn)盤的任何其他移動(dòng),保險(xiǎn)箱DFA的狀態(tài)轉(zhuǎn)換表：,其優(yōu)點(diǎn)：1. 簡(jiǎn)潔、直觀 2. 嚴(yán)謹(jǐn)、無二義性 3. 可以從代數(shù)角度進(jìn)行進(jìn)一步的分析,如上述DFA可以轉(zhuǎn)換成如下代數(shù)方程組進(jìn)一步進(jìn)行分析討論 x = L1y y = R3z z = L3 解該線性方程組得：L1R3L3,說明： 1. Petri網(wǎng)是利用FA的狀態(tài)圖發(fā)展起來的網(wǎng)系統(tǒng) 2Petri網(wǎng)是一種系統(tǒng)的數(shù)學(xué)和圖形的描述和分析工具,（密碼）,Petri網(wǎng)的特點(diǎn)： 1. 作為一種圖形工具，直觀形象，便于使用 注：同軟件設(shè)計(jì)中的狀態(tài)圖、結(jié)構(gòu)圖、程序流程圖類 似，直觀形象，便于使用； 如：用Petri網(wǎng)可直觀描述具有并發(fā)、并行、異步、分 布、不確定性和隨機(jī)的信息處理系統(tǒng)，即模擬系 統(tǒng)的動(dòng)態(tài)性和并發(fā)性。 2. 作為一種數(shù)學(xué)工具，便于計(jì)算和驗(yàn)證 如：它可以建立狀態(tài)方程、代數(shù)方程以及系統(tǒng)行為的 其他數(shù)學(xué)模型，便于計(jì)算和驗(yàn)證； 3. 作為一種理論與實(shí)際工作的中介（橋梁），相互借鑒 如： 實(shí)際工作者可以從中學(xué)到如何使他們的建模條理化 理論工作者可以從中學(xué)到如何使他們的建模更實(shí)用化,5. 2 Petri網(wǎng)的定義及基本原理,一、Petri網(wǎng)的靜態(tài)結(jié)構(gòu)（或稱具有靜態(tài)特征的Petri網(wǎng)） Petri網(wǎng) N=（P，T；F），并滿足以下條件： (1) PT (2) PT (3) F （PT）（TP） /雙向映射關(guān)系 (4) DOM(F)COD(F)=PT /表明PT中的元素 / 在N中均被使用到 其中: P=p1,p2,pn 是N的有窮位置集合(表示狀態(tài)的元素) T=t1,t2,tn 是N的有窮轉(zhuǎn)移集合(表示狀態(tài)變化的元素) F是由一個(gè)P元素和一個(gè)T元素組成的二元組的集合 DOM(F)= x |y:(y , x)F /代表F的后集;存在量詞 COD(F)= x |y:(x , y)F /代表F的前集； 注：位置(Place)有人譯為“庫所”，轉(zhuǎn)移(Transition)譯成“變遷”,例1：N=(P , T ; F) P = p1，p2，p3，p4，p5，p6 T = t1，t2，t3，t4，t5，t6 F = ( p1 , t1) , ( t1 , p2) , ( p2 , t2) , ( t1 , p1) , ( p1 , t3) , ( t3 , p3) , ( t3 , p4) , ( p3 , t4) , ( p4 , t5) , ( t4 , p5) , ( t5 , p6) , ( p5 , t6) , ( p6 , t6) 其中： DOM(F)=t1, p2, t2, p1, t3, p3, p4, t4, t5, p5, p6, t6 COD(F)= )=p1, t1, p2, t3, p3, p4, t4, t5, p5, p6 顯然 DOM(F)COD(F)=PT =p1, p2, p3, p4 p5, p6, t1, t2, t3, t4, t5, t6 注：此為關(guān)系集合表示法,Petri網(wǎng)的圖形表示： 1用圓形 表示位置(庫所)p: 作用是決定轉(zhuǎn)移能否發(fā)生 2用矩形 表示轉(zhuǎn)移(變遷)t: 作用是改變位置的狀態(tài) 3用有向弧表示位置與轉(zhuǎn)移的有序偶 例如上述Petri網(wǎng)N的圖形表示:,位置或轉(zhuǎn)移的前集和后集定義： 設(shè)XPT , 令 *x = y | (y , x)F /前集（亦稱x的輸入集） x*= y | (x , y)F /后集（亦稱x的輸出集） 說明：定義兩個(gè)特殊的Petri網(wǎng) 1. 純網(wǎng)：如果對(duì)所有xPT ，都有 *xx* 注：表明x無自循環(huán)（僅通過一個(gè)結(jié)點(diǎn)的循環(huán)） 2. 簡(jiǎn)單網(wǎng)：如果對(duì)所有x，yPT ,，都有 (*x=*y)(x*=y*)( x=y) 即：不存在兩個(gè)不同的結(jié)點(diǎn)，它們的前集和后集相同。 例如：上例是純網(wǎng)且是簡(jiǎn)單網(wǎng),非純網(wǎng)例：,其中： *t1= p1 t1*=p1，p2 *t1t1*= p1 p1，p2= p1 ,其中： * p2 =t1 p2*=t1 *p2p2*= t1 t1= t1 ,其中： *t1= p1 ， *t2=p1 ，t1*= p2 ， t2*=p2 然而 t1t2,非簡(jiǎn)單網(wǎng)例：,二、Petri網(wǎng)的動(dòng)態(tài)特征 具有動(dòng)態(tài)特征的Petri網(wǎng)是一個(gè)六元組： =（P，T；F，K，W，M0） 其中：（P，T；F）同前 K: PN+，是位置上的容量函數(shù)，表示一個(gè)位置 的總?cè)萘?N+=1，2，3， = ：即，若K(P)=，表示位置的容量為無窮 W: FN+，是弧集合上的權(quán)函數(shù) M: PN0，是的標(biāo)識(shí)（Marking），M0為初始標(biāo)識(shí) N0=0，1，2，3， pP M(p)K(p) 其中：M(p): 表示當(dāng)前位置p的實(shí)際存儲(chǔ)數(shù)量。,說明：在Petri網(wǎng)的圖形表示中 1W（x , y）= i 標(biāo)在?。▁ , y）上，即：,其中：i=1 可省略,如：,2M(p)= i 用在位置p對(duì)應(yīng)的圓形中標(biāo)注i個(gè)實(shí)心點(diǎn)標(biāo)記,其中： 1) 實(shí)心點(diǎn)“”稱作標(biāo)記（Token） 2) 同一位置中的諸多標(biāo)記代表同一類完全等價(jià)的個(gè)體 如：其中一個(gè)標(biāo)記代表人，則其他標(biāo)記也代表人,3K(p)標(biāo)記在位置p的圓形外面，如K(p)=10 則有：,其中：K(p)=時(shí)省略不標(biāo),例：設(shè)有Petri網(wǎng),則有：M0=(1，0，0，0，0，0) W(t2 , p1)= W(t5 , p6)= W(t6 , p1)=2 W(t3 , p3)=4 W(t4 , p5)=3 W(p1 , t1)=W(t1 , p2)=W(p2 , t2)=W(p1, t3)=W(t3 , p4) = W(p4 , t5)= W(p3 , t4)= W(p5 , t6)= W(p6 , t6)=1 p: K(P)=,3轉(zhuǎn)移發(fā)生規(guī)則 Petri網(wǎng)的動(dòng)態(tài)行為: 是通過轉(zhuǎn)移t發(fā)生引起標(biāo)識(shí)M改變來 體現(xiàn)的，下面是轉(zhuǎn)移可發(fā)生的條件: （1）轉(zhuǎn)移 t 可發(fā)生的條件 若在標(biāo)識(shí)M下，p1，p1*t=M(p1)W(p1，t)， 且p2，p2t*= M(p2) +W(t，p2) K(p2)， 此時(shí)稱 t 在M下可發(fā)生，記為M t 例如: 可發(fā)生例：,其中：M(p1)=1 M(p2)=0 W(p1，t)=1 W(t，p2)=1 K(p2)=1 則有：M(p1)=1W(p1，t)=1 且M(p2)+W(t，p2)=0+1=1K(p2)=1,不可發(fā)生例：,條件1不成立：,條件2不成立：,2,(2)轉(zhuǎn)移t發(fā)生的結(jié)果 若Mt，t就可以發(fā)生，發(fā)生后將M變成新標(biāo)識(shí)M， 記為MtM，(或MM)，并稱M為M的后繼標(biāo) 識(shí)。對(duì)pP均進(jìn)行如下操作：,t,例：（關(guān)于轉(zhuǎn)移t發(fā)生的結(jié)果）,a.,則：M=M0=(1，0，0) Mt1M M(p1)=M(p1)-W(p1,t1)+W(t1,p1) p1t1*t1 M=(1, 1, 0) M(p2)= M(p2)+W(t1，p2) p2t1* M(p3)= M(p3),b.,c.,說明： 1. 一個(gè)沒有任何輸入位置的轉(zhuǎn)移叫做源轉(zhuǎn)移，一個(gè)源轉(zhuǎn)移的發(fā)生是無條件的且它的發(fā)生只會(huì)產(chǎn)生標(biāo)記，而不消耗任何標(biāo)記。,2一個(gè)沒有任何輸出位置的轉(zhuǎn)移叫做潭轉(zhuǎn)移，一個(gè)潭轉(zhuǎn) 移的發(fā)生將消耗標(biāo)記，而不產(chǎn)生任何標(biāo)記。,利用下例Petri網(wǎng)進(jìn)一步討論,在該P(yáng)etri網(wǎng)中，初始標(biāo)記為： M0=(1，0，0，0，0，0) 1由轉(zhuǎn)移t發(fā)生條件，這時(shí)有 M0t1和M0t3 2轉(zhuǎn)移t發(fā)生的結(jié)果和現(xiàn)象 沖突(Conflict)： 由于M0t1且M0t3，表明t1和t3同時(shí)可以發(fā)生，而 M0(p1)=1，即t1和t3共享一個(gè)“資源”，則t1和t3不能同時(shí)發(fā) 生，網(wǎng)論中稱這種情況為“沖突”。,網(wǎng)論解決沖突的辦法可以是：通過環(huán)境對(duì)系統(tǒng)進(jìn)行控制 其中：環(huán)境：指具體情況。 控制：指給出一定的條件和限制。 如：?jiǎn)?dòng)次數(shù)（權(quán)1）+ 優(yōu)先級(jí)（權(quán)2） 令：t1的優(yōu)先級(jí)t3的優(yōu)先級(jí) 且 t1發(fā)生次數(shù)t3發(fā)生 次數(shù)，則此時(shí)：M0t1 但M0t3 t1發(fā)生有：M0t1M1=(0，1，0，0，0，0) M1t2M0=(1，0，0，0，0，0) 此時(shí)M0t1且M0t3 但t1發(fā)生次數(shù)t3發(fā)生次數(shù)，則 M0t3 但 M0t1 t3發(fā)生有：M0t3M2=(0，0，1，1，0，0) 這時(shí)出現(xiàn)（產(chǎn)生）并發(fā)：,并發(fā)(Concurrent) M2(p3)=1和M2(p4)=1兩件事同時(shí)出現(xiàn)，此時(shí)t4和t5同時(shí)可以發(fā)生，且互不影響，網(wǎng)論中稱這種現(xiàn)象為“并發(fā)” 并行（Parallel） t4和t5同時(shí)發(fā)生。發(fā)生后，則得標(biāo)記： M=(0，0，0，0，1，1) 此時(shí)M t6，若t6發(fā)生，則有： Mt6M0=(1，0，0，0，0，0)，,說明： 1. t6起著使t4、t5兩個(gè)異步（不在同一條執(zhí)行路徑上） 活動(dòng)同步（在同一條執(zhí)行路徑上）的作用。 2. 并發(fā)：是兩件以上的事情同時(shí)發(fā)生，是瞬時(shí)的事件 3. 并行：是兩件以上的進(jìn)程同時(shí)運(yùn)行，是持續(xù)的過程 4并發(fā)和并行的關(guān)系：并發(fā)可導(dǎo)致并行，但并行的事 件并不一定是并發(fā)的。一般情況下說“并發(fā)”也有并行的含義 ,但反之不一定成立。,碰撞(contact) 設(shè)有M0=(1，0，1，0，0，0)，并規(guī)定位置容量均 為K=1(不能超過1)，這時(shí)t3 不能發(fā)生，因?yàn)閠3的發(fā)生 會(huì)使p3的容量超過1，稱這種現(xiàn)象為“碰撞”。,混惑(confusion)： 有時(shí)，一個(gè)Petri網(wǎng)中同時(shí)存在著并發(fā)和沖突，而且并發(fā)的實(shí)施會(huì)引起沖突的消失(減少)或出現(xiàn)(增加)，我們稱這種情況為“混惑”。,例：在下圖所示的Petri網(wǎng)中,M0=(1, 1, 0, 0, 0),此時(shí)M0t1且M0t3（并發(fā)），若t3發(fā)生，則有M=(1, 0, 1, 0, 0),使 Mt1且Mt2，出現(xiàn)“沖突”，因共享p1中的一個(gè)“資源”， 說明“并發(fā)”的存在，使原沒有“沖突”，出現(xiàn)了“沖突”。,說明：存在“混惑的系統(tǒng)不是好系統(tǒng)，因?yàn)樵谶@種系統(tǒng)中， 沖突忽隱忽現(xiàn)，使得外部環(huán)境對(duì)系統(tǒng)難以控制。,關(guān)于“并發(fā)和“沖突”兩個(gè)概念的形式化（完整）描述 1并發(fā) 設(shè)M為Petri網(wǎng)的一個(gè)標(biāo)識(shí)，若存在t1和t2使得Mt1 和Mt2，并滿足： Mt1M1