形式化方法

定義

用於開發計算機系統的形式化方法是描述系統性質的基於數學的技術，這樣的形式化方法提供了乙個框架，可以在框架中以系統的而不是特別的方式刻劃、開發和驗證系統。如果乙個方法有良好的數學基礎，那麼它就是形式化的，典型地以形式化規約語言給出。這個基礎提供一系列精確定義的概念，如：一致性和完整性，以及定義規範的實現和正確性。形式化方法的本質是基於數學的方法來描述目標軟體系統屬性的一種技術。不同的形式化方法的數學基礎是不同的，有的以集合論和一階謂詞演算為基礎（如z和 vdm），有的則以時態邏輯為基礎。形式化方法需要形式化規約說明語言的支援。

根據說明目標軟體系統的方式，形式化方法可以分為兩類：

1）面向模型的形式化方法。面向模型的方法通過構造乙個數學模型來說明系統的行為。2）面向屬性的形式化方法。面向屬性的方法通過描述目標軟體系統的各種屬性來間接定義系統行為。

根據表達能力，形式化方法可以分為五類：1）基於模型的方法：通過明確定義狀態和操作來建立乙個系統模型（使系統從乙個狀態轉換到另乙個狀態）。用這種方法雖可以表示非功能性需求（諸如時間需求），但不能很好地表示併發性。如：z語言，vdm，b方法等。

2）基於邏輯的方法：用邏輯描述系統預期的效能，包括底層規約、時序和可能性行為。採用與所選邏輯相關的公理系統證明系統具有預期的效能。用具體的程式設計構造擴充邏輯從而得到一種廣譜形式化方法，通過保持正確性的細化步驟集來開發系統。如：itl（區間時序邏輯），區段演算（dc），hoare 邏輯，wp演算，模態邏輯，時序邏輯，tam（時序**模型），rttl（實時時序邏輯）等。

3）代數方法：通過將未定義狀態下不同的操作行為相聯絡，給出操作的顯式定義。與基於模型的方法相同的是，沒有給出併發的顯式表示。如：obj， larch族代數規約語言等；

4）程序代數方法：通過限制所有容許的可觀察的過程間通訊來表示系統行為。此類方法允許併發過程的顯式表示。如：通訊順序過程（csp），通訊系統演算（ccs），通訊過程代數（acp），時序排序規約語言（lotos），計時csp(tcsp），通訊系統計時可能性演算（tpccs）等。

5）基於網路的方法：由於圖形化表示法易於理解，而且非專業人員能夠使用，因此是一種通用的系統確定表示法。該方法採用具有形式語義的圖形語言，為系統開發和再工程帶來特殊的好處。如 petri圖，計時petri圖，狀態圖等。

在電腦科學和軟體工程領域，形式化方法是基於數學的特種技術，適合於軟體和硬體系統的描述、開發和驗證。將形式化方法用於軟體和硬體設計，是期望能夠像其它工程學科一樣，使用適當的數學分析以提高設計的可靠性和魯棒性。但是，由於採用形式化方法的成本高意味著它們通常只用於開發注重安全性的高度整合的系統。

形式化方法在古代就運用了,而在現代邏輯中又有了進一步的發展和完善。這種方法特別在數學、電腦科學、人工智慧等領域得到廣泛運用。它能精確地揭示各種邏輯規律,制定相應的邏輯規則,使各種理論體系更加嚴密。同時也能正確地訓練思維、提高思維的抽象能力。

形式化方法

形式化方法

形式化方法

形式化方法

相關推薦