軟件工程第十章形式化方法

軟件工程第十章形式化方法第1頁，共105頁，2023年，2月20日，星期二

第十章形式化方法形式化方法提供了規(guī)約環(huán)境的基礎(chǔ)，它使得所生成的分析模型比用傳統(tǒng)的或面向?qū)ο蟮姆椒ㄉ傻哪Ｐ透暾?、一致和無二義性。集合論和邏輯符號(hào)的描述設(shè)施使得我們可以創(chuàng)建清晰的關(guān)于事實(shí)的陳述。第2頁，共105頁，2023年，2月20日，星期二支配形式化方法的基本概念是：數(shù)據(jù)不變式、狀態(tài)、離散數(shù)學(xué)、序列相關(guān)聯(lián)的符號(hào)體系、形式化規(guī)約語言。第3頁，共105頁，2023年，2月20日，星期二10.1形式化方法形式化方法的定義定義10—1：用于開發(fā)計(jì)算機(jī)系統(tǒng)的形式化方法是描述系統(tǒng)性質(zhì)的基于數(shù)學(xué)的技術(shù)。這樣的形式化方法提供了一個(gè)框架，人們可以在框架中以系統(tǒng)的方式刻劃、開發(fā)和驗(yàn)證系統(tǒng)。第4頁，共105頁，2023年，2月20日，星期二形式化方法主要思想利用形式化規(guī)格說明語言定義用戶需求，并采用數(shù)學(xué)推演的方法證明需求定義的性質(zhì)，例如一致性、實(shí)時(shí)系統(tǒng)的活性和公平性等。對(duì)于復(fù)雜的應(yīng)用問題，盡管無法驗(yàn)證整個(gè)需求定義的完全性，但仍有可能為避免某些要點(diǎn)的疏漏而建立數(shù)學(xué)斷言，然后予以形式證明或反駁。第5頁，共105頁，2023年，2月20日，星期二形式化方法是克服需求分析階段不精確性、不一致性和不完全性的有效途徑。第6頁，共105頁，2023年，2月20日，星期二10.1.1形式化方法概念

例10--1：符號(hào)表(如右圖)：它由一組沒有重復(fù)的項(xiàng)構(gòu)成。程序被用于維護(hù)一個(gè)符號(hào)表，在許多不同類型的應(yīng)用中使用此符號(hào)表。第7頁，共105頁，2023年，2月20日，星期二如果對(duì)于上表有一個(gè)陳述：包括不多于Max2D的用戶名，那么就為表設(shè)定了一個(gè)限制，這就稱為數(shù)據(jù)不變式的條件的一個(gè)構(gòu)成成分。數(shù)據(jù)不變式是一個(gè)條件，它在包含一組數(shù)據(jù)的系統(tǒng)的執(zhí)行過程中總保持為真。第8頁，共105頁，2023年，2月20日，星期二上面討論的符號(hào)表的數(shù)據(jù)不變式有兩個(gè)構(gòu)成成分：(1)表中包含的名字?jǐn)?shù)不超過MaxIds。(2)在表中沒有重復(fù)的名字。第9頁，共105頁，2023年，2月20日，星期二狀態(tài)的概念 在形式化方法的語言環(huán)境中，狀態(tài)是系統(tǒng)訪問和修改的存儲(chǔ)數(shù)據(jù)。在上述符號(hào)表程序的例子中，狀態(tài)是符號(hào)表。操作的概念 這是在系統(tǒng)中發(fā)生的讀或?qū)憼顟B(tài)數(shù)據(jù)的動(dòng)作。第10頁，共105頁，2023年，2月20日，星期二10.1.2數(shù)學(xué)知識(shí)1.集合和構(gòu)造性規(guī)約 所謂集合，乃是有某些可以相互區(qū)分的如何對(duì)象，如數(shù)、變量、函數(shù)、字母、數(shù)字、圖、語言、程序、事件等，或者沒有任何對(duì)象，匯集在一起所組成的整體。第11頁，共105頁，2023年，2月20日，星期二例10--2：一個(gè)包含4個(gè)元素的自然數(shù)集合： ｛1，3，5，7｝例10--3：包含五種程序設(shè)計(jì)語言的名字的集合： ｛C，C＋＋，Pascal，Basic，F(xiàn)ORTRAN｝例10--4：下面的數(shù)的聚集不是集合，因?yàn)樗酥貜?fù)的元素2： ｛33，2，99，11，22，88，2｝第12頁，共105頁，2023年，2月20日，星期二

在集合中，元素出現(xiàn)的順序是不重要的。我們將集合中元素的數(shù)量稱為集合的基數(shù)(cardinality)，并用操作符#返回集合的基數(shù)。

例10--5：表達(dá)式說明用于已知集合的基數(shù)操作符，其結(jié)果指出集合中項(xiàng)的數(shù)量： ＃｛A，B，C，D｝＝4第13頁，共105頁，2023年，2月20日，星期二

如果要定義一個(gè)集合，可以通過枚舉出集合的元素來定。也可以是創(chuàng)建一個(gè)構(gòu)造性集合規(guī)約，這種方式是用布爾表達(dá)式來刻劃集合成員的一般形式。例10--6：下面是一個(gè)構(gòu)造性規(guī)約的例子： ｛n：N｜n＜5·n｝第14頁，共105頁，2023年，2月20日，星期二

這個(gè)規(guī)約中有三個(gè)部分： ①：基調(diào)n：N； ②：謂詞n＜5； ③：項(xiàng)n。 基調(diào)刻劃在形成集合時(shí)考慮的值的范圍，謂詞定義集合如何被構(gòu)造，項(xiàng)則給出集合中項(xiàng)的一般形式。

第15頁，共105頁，2023年，2月20日，星期二2.集合運(yùn)算符 用命題法定義兩個(gè)集合的運(yùn)算。 定義10--2設(shè)A，B為任意兩個(gè)集合。令

A∪B={x│x∈A或x∈B}A∩B={x│x∈A和x∈B}A－B={x│x∈A且xB}AB=（A∪B）－（A∩B）第16頁，共105頁，2023年，2月20日，星期二集合的運(yùn)算可以用文氏圖如圖直觀地表示。圖中的陰影部分表示運(yùn)算的結(jié)果。第17頁，共105頁，2023年，2月20日，星期二第18頁，共105頁，2023年，2月20日，星期二3．笛卡爾乘積

4.邏輯運(yùn)算符

4.序列

第19頁，共105頁，2023年，2月20日，星期二10.1.3應(yīng)用數(shù)學(xué)符號(hào)描述形式規(guī)約例10--18：塊處理器在操作系統(tǒng)中一個(gè)更重要的部分是維護(hù)由用戶創(chuàng)建的文件的子系統(tǒng)，塊處理器是文件子系統(tǒng)中的一部分。文件存儲(chǔ)中的文件由存儲(chǔ)設(shè)備上的存儲(chǔ)塊構(gòu)成，在計(jì)算機(jī)的操作中，文件被創(chuàng)建和刪除，需要存儲(chǔ)塊的獲取和釋放。為了處理這些，文件子系統(tǒng)維持一個(gè)未用塊池，并將保持對(duì)當(dāng)前使用塊的跟蹤。當(dāng)塊從被刪除文件釋放時(shí)，它們通常被加入到等待進(jìn)入未用塊池的塊隊(duì)列中。如圖所示.第20頁，共105頁，2023年，2月20日，星期二第21頁，共105頁，2023年，2月20日，星期二

對(duì)這個(gè)子系統(tǒng)而言，狀態(tài)是自由塊的集合、已用塊的集合、以及返回塊的隊(duì)列，數(shù)據(jù)不變式用自然語言表達(dá)如下：第22頁，共105頁，2023年，2月20日，星期二

1.沒有塊同時(shí)被標(biāo)記為未用和已用。

2.所有在隊(duì)列中的塊集合將是當(dāng)前已用塊集合的子集。

3.沒有隊(duì)列元素包含相同的塊號(hào)。第23頁，共105頁，2023年，2月20日，星期二4.已用塊和未用塊的集合將是組成文件的塊的總集。

5.在未用塊集合中沒有重復(fù)的塊號(hào)。

6.在已用塊集合中沒有重復(fù)的塊號(hào)。第24頁，共105頁，2023年，2月20日，星期二和子系統(tǒng)關(guān)聯(lián)的某些操作如下：

1.將一個(gè)塊集合加到隊(duì)列尾。

2.從隊(duì)列前面移走一個(gè)已用塊集合并將其放到未用塊集合中。

3.檢查是否塊隊(duì)列為空。第25頁，共105頁，2023年，2月20日，星期二描述塊處理器的不變式有如下一組條件：

1.沒有塊同時(shí)被標(biāo)記為未用和已用。

2.所有在隊(duì)列中的塊集合將是當(dāng)前已用塊集合的子集。

3.在未用塊集合中沒有重復(fù)的塊號(hào)。第26頁，共105頁，2023年，2月20日，星期二4.沒有隊(duì)列元素包含相同的塊號(hào)。

5.已用塊和未用塊的集合將是組成文件的塊的總集。

6.在已用塊集合中沒有重復(fù)的塊號(hào)。第27頁，共105頁，2023年，2月20日，星期二10.1.4形式化規(guī)約語言形式化規(guī)約語言通常由三個(gè)主要的成分構(gòu)成：

(1)語法，定義用于表示規(guī)約的特定符號(hào)；

(2)語義，幫助定義用于描述系統(tǒng)的“對(duì)象的全域(universeofobjects)”；

(3)一組關(guān)系，定義確定出哪個(gè)對(duì)象真正滿足規(guī)約的規(guī)則。第28頁，共105頁，2023年，2月20日，星期二形式化規(guī)約語言的語法域通?；趶臉?biāo)準(zhǔn)集合論符號(hào)和謂詞演算導(dǎo)出的語法。第29頁，共105頁，2023年，2月20日，星期二10.2有限狀態(tài)機(jī)（FSM）很多實(shí)時(shí)系統(tǒng)，特別是實(shí)時(shí)控制系統(tǒng)，其整個(gè)分析機(jī)制與系統(tǒng)的狀態(tài)有相當(dāng)大的關(guān)系。有限狀態(tài)機(jī)由有限的狀態(tài)和相互之間的轉(zhuǎn)移構(gòu)成，在任何時(shí)候只能處于給定數(shù)目的狀態(tài)中的一個(gè)。第30頁，共105頁，2023年，2月20日，星期二當(dāng)接收到一個(gè)輸入事件時(shí)，狀態(tài)機(jī)產(chǎn)生一個(gè)輸出，同時(shí)也可能伴隨著狀態(tài)的轉(zhuǎn)移。主要有兩種方法來建立有限狀態(tài)機(jī)，一種是"狀態(tài)轉(zhuǎn)移圖"，另一種是"狀態(tài)轉(zhuǎn)移表"，分別用圖形方式和表格方式建立有限狀態(tài)機(jī)。第31頁，共105頁，2023年，2月20日，星期二有限狀態(tài)機(jī)的組成如下：（1）一個(gè)有限的狀態(tài)集合Q

（2）一個(gè)有限的輸入集合I

（3）一個(gè)變遷函數(shù)δ：Q×I→Q變遷函數(shù)也是一個(gè)狀態(tài)函數(shù)，在某一狀態(tài)下，給定輸入后，F(xiàn)SM轉(zhuǎn)入該函數(shù)產(chǎn)生的新狀態(tài)。δ的定義域內(nèi)的某些數(shù)值可以是未定義的。第32頁，共105頁，2023年，2月20日，星期二下圖示意了一個(gè)簡(jiǎn)單的有限狀態(tài)機(jī)。左圖表明該FSM有q0、q1、q2、q3四個(gè)狀態(tài)，輸入集中有a、b、c三個(gè)元素；右圖中各個(gè)狀態(tài)之間的轉(zhuǎn)換關(guān)系則更清晰。第33頁，共105頁，2023年，2月20日，星期二第34頁，共105頁，2023年，2月20日，星期二有限狀態(tài)機(jī)的優(yōu)點(diǎn)在于簡(jiǎn)單易用，狀態(tài)間的關(guān)系能夠直觀看到。第35頁，共105頁，2023年，2月20日，星期二有限狀態(tài)機(jī)應(yīng)用在實(shí)時(shí)系統(tǒng)中時(shí)，其最大的缺點(diǎn)是：任何時(shí)刻系統(tǒng)只能有一個(gè)狀態(tài)，無法表示并發(fā)性，不能描述異步并發(fā)的系統(tǒng)。另外，在系統(tǒng)部件較多時(shí)，狀態(tài)數(shù)隨之增加，導(dǎo)致復(fù)雜性顯著增長(zhǎng)。第36頁，共105頁，2023年，2月20日，星期二10.3Petri網(wǎng)概念Petri網(wǎng)是在軟件分析中，用一種系統(tǒng)的數(shù)學(xué)和圖形的描述與分析的方法。對(duì)于具有并發(fā)、異步、分布、并行、不確定性或隨機(jī)性的信息處理系統(tǒng)，都可以利用Petri網(wǎng)方法構(gòu)造出要開發(fā)的Petri網(wǎng)模型。第37頁，共105頁，2023年，2月20日，星期二由于Petri網(wǎng)的表示手法是用圖形工具。因此其表示形式與傳統(tǒng)方法的結(jié)構(gòu)圖、流程圖具有同樣的直觀、形象效果。第38頁，共105頁，2023年，2月20日，星期二Petri網(wǎng)可以建立狀態(tài)方程、代數(shù)方程以及系統(tǒng)行為的其他數(shù)學(xué)模型。因此，系統(tǒng)開發(fā)人員和理論研究工作者都可以根據(jù)需要利用Petri網(wǎng)。第39頁，共105頁，2023年，2月20日，星期二10.3.1靜態(tài)結(jié)構(gòu)Petri網(wǎng)理論認(rèn)為，任何系統(tǒng)是由兩類基本元素組成：一類是表示狀態(tài)的元素，另一是表示狀態(tài)變化的元素。第40頁，共105頁，2023年，2月20日，星期二在Petri網(wǎng)中，表示狀態(tài)的元素用位置（place）表示，表示狀態(tài)變化的元素用轉(zhuǎn)移（transition）表示。轉(zhuǎn)移的作用是改變狀態(tài)，位置的作用是決定轉(zhuǎn)移能否發(fā)生。將狀態(tài)的元素和狀態(tài)變化的元素兩者間的這種依賴關(guān)系用?。^）表示出來就是一個(gè)Petri網(wǎng)。第41頁，共105頁，2023年，2月20日，星期二Petri網(wǎng)的基本成份可以表示為一個(gè)三元組：

N=（P，T；F）并滿足以下條件：（1）P∪T≠ф

（2）P∩T=ф

（3）F（P×T）∪（T×P）（4）DOM（F）∪COD（F）=P∪T第42頁，共105頁，2023年，2月20日，星期二例：N的Petri網(wǎng)

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），（t2，p1），（p1，t3），（t3，p3），（t3，p4），（p3，t4），（p4，t5），（t4，p5），（t5，p6），（p5，t6），（p6，t6），（t6，p6）}N的Petri網(wǎng)圖形表示如下圖所示。第43頁，共105頁，2023年，2月20日，星期二第44頁，共105頁，2023年，2月20日，星期二10.3.2動(dòng)態(tài)特征在用Petri網(wǎng)作為系統(tǒng)分析和建模工具時(shí)，除了具有描述的靜態(tài)結(jié)構(gòu)的能力外，還包括位置容量以及轉(zhuǎn)移啟動(dòng)對(duì)位置容量的影響信息。第45頁，共105頁，2023年，2月20日，星期二如果對(duì)于位置容量的有限容量用大于零的整數(shù)表示。轉(zhuǎn)移啟動(dòng)對(duì)位置中標(biāo)記數(shù)的影響用弧上的整數(shù)表示。那么，于是具有動(dòng)態(tài)特征的Petri網(wǎng)就可以表示為六元組：∑=（P，T；F，K，W，M0）第46頁，共105頁，2023年，2月20日，星期二例：具有M0和W的Petri網(wǎng)可以表示為下圖所示。第47頁，共105頁，2023年，2月20日，星期二第48頁，共105頁，2023年，2月20日，星期二對(duì)于上圖所示的Petri網(wǎng)，

M0=（1，0，0，0，0，0）

W（t2，p1）=W（t5，p6）

=W（t6，p1）

=4W（t3，p3）=6W（t4，p5）=5

第49頁，共105頁，2023年，2月20日，星期二W（p1，t3）=W（p3，t4）

=W（p5，t6）

=（p6，t6）

=W（t3，p4）

=W（p4，t5）

=W（p1，t1）

=W（t1，p2）

=W（p2，t2）=1第50頁，共105頁，2023年，2月20日，星期二10.3.3轉(zhuǎn)移啟動(dòng)規(guī)則前面介紹的Petri網(wǎng)的動(dòng)態(tài)特征是Petri網(wǎng)的動(dòng)態(tài)行為的特性描述。這種動(dòng)態(tài)行為是通過轉(zhuǎn)移啟動(dòng)引起標(biāo)識(shí)改變的變化來體現(xiàn)的。而轉(zhuǎn)移啟動(dòng)則要有可以啟動(dòng)轉(zhuǎn)移（轉(zhuǎn)移有效）的條件和啟動(dòng)規(guī)則。第51頁，共105頁，2023年，2月20日，星期二

（1）轉(zhuǎn)移t有效的條件（2）轉(zhuǎn)移t啟動(dòng)的結(jié)果第52頁，共105頁，2023年，2月20日，星期二我們以下圖為例說明轉(zhuǎn)移啟動(dòng)規(guī)則。第53頁，共105頁，2023年，2月20日，星期二第54頁，共105頁，2023年，2月20日，星期二為了說明“并發(fā)”和“沖突”這兩個(gè)概念，我們用圖10--9所示的Petri網(wǎng)來表示“混惑”。第55頁，共105頁，2023年，2月20日，星期二第56頁，共105頁，2023年，2月20日，星期二有了這些基本概念后，就可以對(duì)于“并發(fā)”和“沖突”兩個(gè)概念的完整描述。第57頁，共105頁，2023年，2月20日，星期二1.并發(fā)設(shè)M為Petri網(wǎng)∑的一個(gè)標(biāo)識(shí)，若存在t1和t2使得M[t1＞和M[t2＞，并滿足M[t1＞M1M1[t2＞，且M[t2＞M2M[t1＞，則稱t1和t2在M下并發(fā)。第58頁，共105頁，2023年，2月20日，星期二2.沖突設(shè)M為Petri網(wǎng)∑的一個(gè)標(biāo)識(shí)，若存在t1和t2使得M[t1＞和M[t2＞，并滿足M[t1＞M1

]M1[t2＞，且M[t2＞M2]M2[t1＞，則稱t1和t2在M下沖突，說是說在M標(biāo)識(shí)下，t1和t2都有效，但t1和t2中只有一個(gè)能啟動(dòng)，而且其中任一個(gè)轉(zhuǎn)移啟動(dòng)都會(huì)使另一個(gè)轉(zhuǎn)移無效。第59頁，共105頁，2023年，2月20日，星期二10.3.4行為特性行為特性包括：

1、可達(dá)性

2、有界性

3、活性

4、可逆性第60頁，共105頁，2023年，2月20日，星期二5、可覆蓋性

6、持久性

7、同步距離

8、公平性第61頁，共105頁，2023年，2月20日，星期二10.3.5行為特性分析方法行為特性分析方法分為三類：（1）可覆蓋性（可達(dá)性）樹。（2）矩陣方程求解。（3）分層或化簡(jiǎn)。第62頁，共105頁，2023年，2月20日，星期二用不變性、關(guān)聯(lián)矩陣和狀態(tài)方程的分析方法，就是完全用代數(shù)計(jì)算對(duì)網(wǎng)系統(tǒng)進(jìn)行分析的方法。第63頁，共105頁，2023年，2月20日，星期二不變量所謂不變量是指網(wǎng)系統(tǒng)中有S-不變量和T-不變量。下面幾個(gè)圖顯示的是不變量的Petri網(wǎng)。第64頁，共105頁，2023年，2月20日，星期二第65頁，共105頁，2023年，2月20日，星期二第66頁，共105頁，2023年，2月20日，星期二第67頁，共105頁，2023年，2月20日，星期二2.狀態(tài)方程如果N=（P，T；F）是純網(wǎng)，則C與N存在一一對(duì)應(yīng)的關(guān)系。第68頁，共105頁，2023年，2月20日，星期二3.關(guān)聯(lián)矩陣正如網(wǎng)系統(tǒng)的標(biāo)識(shí)可以表示為一個(gè)向量一樣，網(wǎng)結(jié)構(gòu)也可以用一個(gè)矩陣來表示。第69頁，共105頁，2023年，2月20日，星期二10.3.6結(jié)構(gòu)特性分析方法Petri網(wǎng)有它的的拓?fù)浣Y(jié)構(gòu)。結(jié)構(gòu)特性依賴于Petri網(wǎng)的拓?fù)浣Y(jié)構(gòu)。這些特性適合于網(wǎng)的任何初始標(biāo)識(shí)，也就是說這些特性是獨(dú)立于網(wǎng)的初始標(biāo)識(shí)M0的。因此，這些特性通?？梢杂藐P(guān)聯(lián)矩陣C及其相關(guān)的齊次方程或不等式來刻劃。第70頁，共105頁，2023年，2月20日，星期二對(duì)于Petri網(wǎng)N，我們引入如下幾種結(jié)構(gòu)特性：1.結(jié)構(gòu)活性若N存在一個(gè)活的初始標(biāo)識(shí)，則稱N為結(jié)構(gòu)活的。2.完全可控性若N的任何標(biāo)識(shí)都可從N的任一其他標(biāo)識(shí)到達(dá)，則稱N為完全可控的。3.結(jié)構(gòu)有界性若N對(duì)任何有限的初始標(biāo)識(shí)M0都是有界的，則稱N為結(jié)構(gòu)有界性。第71頁，共105頁，2023年，2月20日，星期二定理一：Petri網(wǎng)N是結(jié)構(gòu)有界的，當(dāng)且僅當(dāng)存在一個(gè)m維正整數(shù)向量Y，使得CY≤0。第72頁，共105頁，2023年，2月20日，星期二推論：N中位置pi是結(jié)構(gòu)無界的，當(dāng)且僅當(dāng)存在一個(gè)非負(fù)整數(shù)n維向量X，使得CTX=△M＞≠0，其中的△M第i項(xiàng)大于0（即△M（pi）＞0）。第73頁，共105頁，2023年，2月20日，星期二4.守恒性若N的每一（某些）位置p存在一個(gè)正整數(shù)Y（p），使得對(duì)任何給定的初始標(biāo)識(shí)M0和每個(gè)M∈R（M0），都有標(biāo)識(shí)的加權(quán)和MTY=M0TY為一個(gè)常量，則稱N為（部分）守恒的。第74頁，共105頁，2023年，2月20日，星期二定理二：Petri網(wǎng)是（部分）守恒的，當(dāng)且僅當(dāng)存在一個(gè)正的（非負(fù)）整數(shù)m維向量Y，滿足CY=0，Y≠0。第75頁，共105頁，2023年，2月20日，星期二5.重復(fù)性若N存在一個(gè)標(biāo)識(shí)M0和一個(gè)從M0開始的啟動(dòng)序列σ，使得每個(gè)（某些）轉(zhuǎn)移在σ中可以無限次發(fā)生，則稱N為（部分）重復(fù)的。第76頁，共105頁，2023年，2月20日，星期二定理三：Petri網(wǎng)N是（部分）重復(fù)的，當(dāng)且僅當(dāng)存在一個(gè)正的（非負(fù)）整數(shù)n維向量x，使得CTX≥0，X≠0。第77頁，共105頁，2023年，2月20日，星期二6.一致性若N存在一個(gè)標(biāo)識(shí)M0和一個(gè)從M0返回到M0的啟動(dòng)序列σ，使得每個(gè)（某些）轉(zhuǎn)移在σ中至少出現(xiàn)一次，則稱N為（部分）一致的。第78頁，共105頁，2023年，2月20日，星期二定理四：Petri網(wǎng)N是（部分）一致的，當(dāng)且僅當(dāng)存在一個(gè)正的（非負(fù)）整數(shù)n維向量X，便得CTX=0，X≠0第79頁，共105頁，2023年，2月20日，星期二10.3.7Petri網(wǎng)到程序結(jié)構(gòu)的轉(zhuǎn)換1.流程圖的方法傳統(tǒng)方法的流程圖方法主要用于順序軟件開發(fā)的詳細(xì)設(shè)計(jì)階段的建模與分析。如果把并行處理退化為只有一個(gè)單進(jìn)程的軟件系統(tǒng)，用Petri網(wǎng)表示，那么傳統(tǒng)方法的流程圖方法也可以用于并行軟件的開發(fā)。第80頁，共105頁，2023年，2月20日，星期二2.編程語言的方法除了流程圖與Petri網(wǎng)互相轉(zhuǎn)換的方法外，也可以用編程語言轉(zhuǎn)換。但是編程語言（如Ada、C++等）必須選用具有并發(fā)機(jī)制。用具有并發(fā)機(jī)制編程語言與Petri網(wǎng)兩者之間建立起恰當(dāng)?shù)穆?lián)系，這樣就可以實(shí)現(xiàn)從Petri網(wǎng)到編程語言的轉(zhuǎn)換。第81頁，共105頁，2023年，2月20日，星期二3.面向?qū)ο蟮某绦蛟O(shè)計(jì)方法面向?qū)ο笞钸m合用于Petri網(wǎng)的描述與分析，因?yàn)閷?duì)象把數(shù)據(jù)和施加于這些數(shù)據(jù)上的私有操作封裝在一起。操作名列在封裝對(duì)象的界面上，當(dāng)其他對(duì)象要“啟動(dòng)”該對(duì)象某個(gè)操作時(shí)，則以操作名發(fā)一條消息，該對(duì)象接受了消息，操作即動(dòng)作起來，完成對(duì)私有數(shù)據(jù)的加工。第82頁，共105頁，2023年，2月20日，星期二10.4凈室方法學(xué)凈室軟件工程(Cleanroomsoftwareengineering)是一種在軟件開發(fā)過程中強(qiáng)調(diào)在軟件中建立正確性的需要的方法。代替?zhèn)鹘y(tǒng)的分析、設(shè)計(jì)、編碼、測(cè)試和調(diào)試周期，凈室方法建議一種不同的觀點(diǎn)：通過在第一次正確地書寫代碼增量并在測(cè)試前驗(yàn)證它們的正確性來避免對(duì)成本很高的錯(cuò)誤消除過程的依賴。它的過程模型是在代碼增量積聚到系統(tǒng)的過程的同時(shí)進(jìn)行代碼增量的統(tǒng)計(jì)質(zhì)量驗(yàn)證。第83頁，共105頁，2023年，2月20日，星期二

10.4.1凈室方法對(duì)軟件工程的凈室哲學(xué)首先由Mill和其同事于1980年代提出，雖然對(duì)這個(gè)嚴(yán)格的軟件開發(fā)方法的早期經(jīng)驗(yàn)顯示了很大的希望，但它并沒有得到廣泛的使用，主要是由于下面的原因：第84頁，共105頁，2023年，2月20日，星期二1.凈室方法學(xué)太理論、太數(shù)學(xué)，以至難于在真實(shí)的軟件開發(fā)中使用。

2.不需要進(jìn)行單元測(cè)試，而是進(jìn)行正確性驗(yàn)證和統(tǒng)計(jì)質(zhì)量控制，與當(dāng)前大多數(shù)軟件開發(fā)方式背離。

3.軟件開發(fā)產(chǎn)業(yè)的成熟度。第85頁，共105頁，2023年，2月20日，星期二

10.4.2凈室過程模型凈室方法使用增量軟件模型的一個(gè)專門版本。一個(gè)“軟件增量的流水線”被若干小的、獨(dú)立的軟件工程小組開發(fā)，一旦每個(gè)增量被認(rèn)證通過，它將被集成為一個(gè)整體。因此，系統(tǒng)的功能隨時(shí)間增加。對(duì)每個(gè)增量的凈室任務(wù)序列如圖所示。第86頁，共105頁，2023年，2月20日，星期二第87頁，共105頁，2023年，2月20日，星期二

10.4.3功能規(guī)約凈室軟件工程通過使用稱為盒結(jié)構(gòu)規(guī)約的方法來遵從操作分析原則。從在頂層的本質(zhì)表示轉(zhuǎn)移向在底層的實(shí)現(xiàn)特定的細(xì)節(jié)。有三種盒類型：第88頁，共105頁，2023年，2月20日，星期二黑盒。這種盒刻劃系統(tǒng)或系統(tǒng)的某部分的行為。通過運(yùn)用由激發(fā)得到反應(yīng)的一組變遷規(guī)則，系統(tǒng)(或部分)對(duì)特定的激發(fā)(事件)作出反應(yīng)。第89頁，共105頁，2023年，2月20日，星期二狀態(tài)盒。這種盒以類似于對(duì)象的方式封裝狀態(tài)數(shù)據(jù)和服務(wù)(操作)。在這個(gè)規(guī)約視圖中，表示出狀態(tài)盒的輸入(激發(fā))和輸出(反應(yīng))