第六講軟件工程的形式化說明技術軟件工程使用的描述技術有三類：非形式化技術、半形式化技術和形式化技術。所謂非形式化技術的代表方法是用自然語言描述的需求規格說明；所謂半形式化技術的代表方法有數據流圖、E-R圖和UML等；所謂形式化技術的方法有很多，其中具有代表性的方法包括有：時序邏輯語言、有窮狀態機、Petri網系統和Z語言等；所謂形式化規格說明語言的關鍵思想是把軟件開發過程中的需求規格說明階段和軟件設計說明階段分開，在需求規格說明階段精確地描述軟件“做什么”，而不涉及“怎么做”。編寫規格說明與編寫計算機程序的不同之處在于規格說明是對目標軟件系統的功能描述，而計算機系統則是實現目標軟件系統功能的過程描述。形式化和非形式化描述方法各有優缺點形式化描述的優點：使用形式化方法可以嚴格準確地描述出系統對象；使用形式化方法描述的系統可以向任意具體系統進行映射轉換；可以對形式化描述的系統進行嚴格的數學證明分析；形式化描述的缺點：形式化描述方法難以使用；使用形式化描述一個龐大的實際系統存在許多困難，在實際應用中有許多問題本身就是模糊或非確定的無法使用嚴格的形式化方法進行描述；3.形式化描述的模型對于那些沒有經過專門的訓練用戶來說很難理解；形式化說明的正確性證明費時費力；尚未出現支持形式化風格全過程的軟件環境；非形式化方法的優點：描述的模型直觀，容易理解；非形式的描述技術比較簡單，容易學習；許多的應用只能使用非形式化的方法描述；非形式化方法的缺點：非形式化的描述可能存在矛盾、二意性和含糊性等問題；難以進行嚴格的證明工作；對于高可靠性的系統，使用該方法描述存在潛在的問題；本文介紹三種形式化方法：有窮狀態機、Petri網、Z語言有窮狀態機：使用一個六元組來準確地描述系統狀態的變化的一種形式化方法。當前狀態+事件+謂詞=＞下一個狀態Petri網：Petri的背景：Petri網的首次提出是由德國科學家Petri于1962年在他的博士論文《用自動機通訊》中提出的使用網狀結構模擬通訊系統。Petri網有時又被稱為網論。Petri的知識結構包括有基本網系統為主的特殊網論和通用網論。Petri網的本質是：將系統的動態行為表現為資源的流動。程序系統的動態特性分為兩類：安全性和進展性。安全性要求所有可能的狀態均具有一定的性質，并要求變化服從給定的規律，其關心的是可能性；進展性要求某些特定的狀態一定能夠達到的，其關心的是必然性；有時人們也提到描述系統性質的活性，其等同于進展性；基本網論（EN_系統）基本網系統中的狀態元素被稱為條件，變遷元素被稱為事件。事件的發生改變條件的狀態，引起信息在網上的流動。條件/事件系統（C/E_系統）非形式地說，滿足一定要求的基本網系統就是一個C/E—系統；為簡單網；每個條件都有機會成真，也有機會成假；每個事件都有機會發生；C/E—系統是通用網論的基礎。基本網論和條件/事件網論是構成其他各級網系統的基礎，C/E—系統是通用網論的基礎。庫所/變遷系統（P/T_系統）P表示庫所，T代表變遷，該系統是最早期的Petri網的形式，主要以研究資源流動為特征。是以孤立的網系統為對象，以尋求分析技術和應用方法為目標的“特殊”網系統。P_元被稱為庫所（place）；T_元被稱為變遷；P_元中的黑點個數被稱為資源的數量，每個黑點被稱為托肯（token）又被稱為標記和令牌；帶箭頭的連線表示資源流動的方向；箭頭上的數字表示組裝所需或產生該種資源的數量，稱為弧上的權；K表示庫所的容量；

實例一：火車調度系統設計實例二：處理兩個進程的同步問題進程得到資源占用資源運行釋放資源不使用資源運行PR1廠LOCKR—處理11tUNLOCKR—處理12—PR2廠LOCKR—處理21—UNLOCKR—處理22—j實例三：生產流水線系統（來分析什么是沖突、餓死和死鎖）通用網論Petri網的通用網論主要研究內容是：以網系統的全體作為研究對象，研究其分類及各分類之間的關系，發展了以并發論，同步論和網邏輯、網拓撲和信息流結構為主要研究內容的理論體系。網邏輯（enlogy）:是以推論為基礎的直觀語義框架。研究的系統中不能夠發生的事件與系統行為的關系。這些事件是由于一完備化操作構造而得的。同步論：為各種同步現象（發送、傳遞和接收信息的這些動作之間的同步）提供定量的描述，與網邏輯結合使用是一種有效的系統規范設計工具。信息流結構：通俗地說就是信息流圖的網表示，是溝通網論和其他學科的界面網拓撲（nettopology）:空間的拓撲結構是區分離散數學和連續數學的基礎。拓撲空間的連續映射既是連續數學的主要研究工具，同時又是連續數學的主要研究對象。由于實際應用中的網系統一般都只有有限多個節點，在通常的拓撲意義下不可能連續的。必須有適用于網系統拓撲，即網拓撲。并發論：如果ab和ba的后果是一樣的，a和b就并行，或a與b并行則ab和ba效果一樣。Z語言：背景Z語言是70年代末至80年代初由英國Oxford大學研究組PRG的JeanRaym