協(xié)議形式化技術的應用研究.pdf

1、協(xié)議工程就是一體化、形式化的協(xié)議開發(fā)過程。協(xié)議工程的目的是用來減少協(xié)議開發(fā)中潛在的錯誤，提高協(xié)議開發(fā)的效率，促進標準化的發(fā)展。協(xié)議的形式化理論是協(xié)議工程的核心。它運用形式化方法進行協(xié)議工程學的研究，研究內(nèi)容包括：協(xié)議分析、協(xié)議設計、協(xié)議描述、協(xié)議驗證、協(xié)議實現(xiàn)和協(xié)議測試的理論和方法。協(xié)議形式化描述是協(xié)議實現(xiàn)和協(xié)議測試的重要前提，協(xié)議驗證保證協(xié)議設計的正確性和完整性，協(xié)議測試是保證協(xié)議實現(xiàn)滿足協(xié)議規(guī)范的重要手段。 本文以協(xié)議工程的

2、理論為依據(jù)，并以AB協(xié)議為研究對象，首先從協(xié)議分析開始，研究了協(xié)議分析技術，并且對協(xié)議的上層用戶及底層用戶的環(huán)境要求進行了討論分析；然后根據(jù)有限狀態(tài)機的理論基礎，研究了AB協(xié)議的有限狀態(tài)機模型，并根據(jù)該模型通過SDL技術實現(xiàn)了對協(xié)議的描述和仿真；最后，進一步研究了協(xié)議驗證的相關概念，本文討論了幾種驗證方法，并對其中的一種方法提出改進，在此基礎上采用改進的方法對AB協(xié)議的狀態(tài)機模型進行了驗證。通過驗證結果的對比，顯示了改進方法的優(yōu)越性。