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

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

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

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

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

例10--5：表達式說明用于已知集合的基數(shù)操作符，其結果指出集合中項的數(shù)量： ＃｛A，B，C，D｝＝4第13頁,共105頁，2024年2月25日，星期天

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

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

第15頁,共105頁，2024年2月25日，星期天2.集合運算符 用命題法定義兩個集合的運算。 定義10--2設A，B為任意兩個集合。令

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頁，2024年2月25日，星期天集合的運算可以用文氏圖如圖直觀地表示。圖中的陰影部分表示運算的結果。第17頁,共105頁，2024年2月25日，星期天第18頁,共105頁，2024年2月25日，星期天3．笛卡爾乘積

4.邏輯運算符

4.序列

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

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

1.沒有塊同時被標記為未用和已用。

2.所有在隊列中的塊集合將是當前已用塊集合的子集。

3.沒有隊列元素包含相同的塊號。第23頁,共105頁，2024年2月25日，星期天4.已用塊和未用塊的集合將是組成文件的塊的總集。

5.在未用塊集合中沒有重復的塊號。

6.在已用塊集合中沒有重復的塊號。第24頁,共105頁，2024年2月25日，星期天和子系統(tǒng)關聯(lián)的某些操作如下：

1.將一個塊集合加到隊列尾。

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

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

1.沒有塊同時被標記為未用和已用。

2.所有在隊列中的塊集合將是當前已用塊集合的子集。

3.在未用塊集合中沒有重復的塊號。第26頁,共105頁，2024年2月25日，星期天4.沒有隊列元素包含相同的塊號。

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

6.在已用塊集合中沒有重復的塊號。第27頁,共105頁，2024年2月25日，星期天10.1.4形式化規(guī)約語言形式化規(guī)約語言通常由三個主要的成分構成：

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

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

(3)一組關系，定義確定出哪個對象真正滿足規(guī)約的規(guī)則。第28頁,共105頁，2024年2月25日，星期天形式化規(guī)約語言的語法域通?；趶臉藴始险摲柡椭^詞演算導出的語法。第29頁,共105頁，2024年2月25日，星期天10.2有限狀態(tài)機（FSM）很多實時系統(tǒng)，特別是實時控制系統(tǒng)，其整個分析機制與系統(tǒng)的狀態(tài)有相當大的關系。有限狀態(tài)機由有限的狀態(tài)和相互之間的轉移構成，在任何時候只能處于給定數(shù)目的狀態(tài)中的一個。第30頁,共105頁，2024年2月25日，星期天當接收到一個輸入事件時，狀態(tài)機產生一個輸出，同時也可能伴隨著狀態(tài)的轉移。主要有兩種方法來建立有限狀態(tài)機，一種是"狀態(tài)轉移圖"，另一種是"狀態(tài)轉移表"，分別用圖形方式和表格方式建立有限狀態(tài)機。第31頁,共105頁，2024年2月25日，星期天有限狀態(tài)機的組成如下：（1）一個有限的狀態(tài)集合Q

（2）一個有限的輸入集合I

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

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頁，2024年2月25日，星期天例：N的Petri網

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網圖形表示如下圖所示。第43頁,共105頁，2024年2月25日，星期天第44頁,共105頁，2024年2月25日，星期天10.3.2動態(tài)特征在用Petri網作為系統(tǒng)分析和建模工具時，除了具有描述的靜態(tài)結構的能力外，還包括位置容量以及轉移啟動對位置容量的影響信息。第45頁,共105頁，2024年2月25日，星期天如果對于位置容量的有限容量用大于零的整數(shù)表示。轉移啟動對位置中標記數(shù)的影響用弧上的整數(shù)表示。那么，于是具有動態(tài)特征的Petri網就可以表示為六元組：∑=（P，T；F，K，W，M0）第46頁,共105頁，2024年2月25日，星期天例：具有M0和W的Petri網可以表示為下圖所示。第47頁,共105頁，2024年2月25日，星期天第48頁,共105頁，2024年2月25日，星期天對于上圖所示的Petri網，

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頁，2024年2月25日，星期天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頁，2024年2月25日，星期天10.3.3轉移啟動規(guī)則前面介紹的Petri網的動態(tài)特征是Petri網的動態(tài)行為的特性描述。這種動態(tài)行為是通過轉移啟動引起標識改變的變化來體現(xiàn)的。而轉移啟動則要有可以啟動轉移（轉移有效）的條件和啟動規(guī)則。第51頁,共105頁，2024年2月25日，星期天

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

]M1[t2＞，且M[t2＞M2]M2[t1＞，則稱t1和t2在M下沖突，說是說在M標識下，t1和t2都有效，但t1和t2中只有一個能啟動，而且其中任一個轉移啟動都會使另一個轉移無效。第59頁,共105頁，2024年2月25日，星期天10.3.4行為特性行為特性包括：

1、可達性

2、有界性

3、活性

4、可逆性第60頁,共105頁，2024年2月25日，星期天5、可覆蓋性

6、持久性

7、同步距離

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

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

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

3.軟件開發(fā)產業(yè)的成熟度。第85頁,共105頁，2024年2月25日，星期天

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

10.4.3功能規(guī)約凈室軟件工程通過使用稱為盒結構規(guī)約的方法來遵從操作分析原則。從在頂層的本質表示轉移向在底層的實現(xiàn)特定的細節(jié)。有三種盒類型：第88頁,共105頁，2024年2月25日，星期天黑盒。這種盒刻劃系統(tǒng)或系統(tǒng)的某部分的行為。通過運用由激發(fā)得到反應的一組變遷規(guī)則，系統(tǒng)(或部分)對特定的激發(fā)(事件)作出反應。第89頁,共105頁，2024年2月25日，星期天狀態(tài)盒。這種盒以類似于對象的方式封裝狀態(tài)數(shù)據(jù)和服務(操作)。在這個規(guī)約視圖中，表示出狀態(tài)盒的輸入(激發(fā))和輸出(反應)。狀態(tài)盒也表示黑盒的“激發(fā)歷史”，即，封裝在狀態(tài)盒中的、必須在蘊含的變遷間保留的數(shù)據(jù)。第90頁,共105頁，2