協議工程

隨着計算機網絡快速發展，網絡影響的範圍越來越廣，網絡應用也越來越多，網絡已經成為現代生活中不可或缺的一部分。網絡中不同計算機系統之間的數據交互、協同工作都是由網絡協議來控制的。可以説，協議是網絡間實時、有序、有效通訊的基礎保證。據統計，現在的網絡中超過有600個網絡協議，2000個網絡應用程序在工作，並且還在不斷增加。 ^[2] 

在20多年的時間裏，協議工程的研究有了長足的進步，大致可分為三個階段。

(1)研究各種形式描述階段(1968年~1979年)

這個階段人們提出各種描述協議的模型，主要包括這樣幾種:有窮自動機，形式語言，Petri網，高級程序設計語言以及一些混合模型。此外還有用時態邏輯和抽象代數語言描述協議。各種形式描述技術都得到了實際應用。

(2)協議及其形式描述的標準化階段(1979年~1985年)

人們在驗證協議正確性的過程中發現協議實現中的錯誤主要是由於協議文本本身的描述(用自然語言形式)就存在着二義性或矛盾之處。1976年由CCITT確認的SDL，經多年廣泛的修改和提高，是一種基於擴展狀態變躍圖和抽象數據類型(ACT ONE)的混合技術。SDL已被電信公司廣泛用於描述電子交換系統。ISO在1988年公佈了兩個國際標準文本Estelle與LOTOS，並提供了用它們描述的運輸層和會話層等協議文本，為協議工程打下基礎。Estelle也基於擴展的狀態變躍模型，但使用PASCAL語法和數據類型。80年代初有人試圖協調Estelle和SDL，終因不能有共同的語義模型而失敗。

(3)協議工程階段(1985年以後)

這一階段人們開始研究基於ISO或CCITT建議的協議開發方法。然而，協議工程目前主要的問題仍是形式技術和方法的研究和開發，許多專家學者按照協議工程的形式方法，經過一輪或幾輪協議軟件系統的實現後，都感到形式技術的重新研究是當前協議工程深入的關鍵。 ^[3] 

協議工程系統的主要組成部分及其關係，它大體上可歸納成以下幾個方面內容:協議設計、協議描述、協議驗證與分析、協議實現、協議測試。

協議開發的第一步是構造一個協議，提出協議文本初稿。這包括:協議環境分析，協議功能設計，協議元素的構造，協議組織形式的確定及協議文本的編寫。

協議可以用自然語言、程序設計語言、形式描述語言或專用語言描述。用自然語言描述的協議可讀性好，因此，ISO是採用自然語言描述並公佈協議標準的。

協議驗證是對通信協議本身的邏輯性進行驗證的過程，其主要目的是，在協議開發的前期，最大限度地檢測和糾正協議錯誤和缺陷，包括死鎖、活鎖、不可執行的行動、不符合要求的協議外部性能等。

協議實現的目的是要產生與機器無關的可執行的協議目標代碼。而所謂的半自動實現，是指通過編譯器，將Estell, Lotos等形式描述語言描述的協議規範文本直接轉換成協議代碼(C , Pascal等程序設計語言)。

協議的測試是協議開發的最後一個階段。由於協議實現採用的是半自動代碼生成技術.與機器相關的協議代碼是手工編寫的，協議實現者對協議的理解各不相同，這就難以保證協議實現與協議規範之間的一致性，而在0SI的環境下，與標準不一致的實現是沒有任何意義的。因此，協議的一致性測試對實現來説是至關重要的。 ^[4] 

TCP/IP協議簇是Internet網絡體系結構的核心協議,已成為實際上的計算機網絡工業標準.隨着計算機網絡的發展,網絡協議的數量越來越多,內容也越來越複雜,如何設計出正確可靠的協議已成為一個挑戰性的課題。為此,協議工程學應運而生。 ^[3]