協(xié)議形式化技術(shù)的應(yīng)用研究.pdf

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

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