形式化方法

形式化方法（formal methods）在邏輯科學中是指分析、研究思維形式結構的方法。它把各種具有不同內容的思維形式(主要是命題和推理)加以比較，找出其中各個部分相互聯結的方式，如命題中包含概念彼此間的聯結，推理中則是各個命題之間的聯結，抽取出它們共同的形式結構；再引入表達形式結構的符號語言，用符號與符號之間的聯絡表達命題或推理的形式結構。

例如，把全稱肯定命題，用符號形式化為「sap」；把聯言命題、假言命題分別形式化為：「p∧q、「p→q」。

又例如：乙個具體的假言聯言推理「如果這種金屬是純鋁，那麼它的物理性質必與純鋁相同；如果這種金屬是純鋁，那麼它的化學性質必與純鋁相同；但這種金屬的物理性質和化學性質與純鋁不相同；所以，它不是純鋁。」這個推理的形式結構是：「如果p，則q；如果p，則r；非q且非r；所以非p。」可進而形式化為下列公式：((p→q)∧(p→r)）∧┐q∧┐r→┐p。

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

1.面向模型的形式化方法

面向模型的方法通過構造乙個數學模型來說明系統的行為。

2.面向屬性的形式化方法

面向屬性的方法通過描述目標軟體系統的各種屬性來間接定義系統行為。

- 根據表達能力，形式化方法可以分為五類：

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

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

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

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

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

形式化方法

形式化方法

形式化方法

形式化方法

相關推薦