基于Pi-演算的移動自助服務(wù)系統(tǒng)的建模與驗(yàn)證.pdf

1、移動自助服務(wù)系統(tǒng)通過有線或無線網(wǎng)絡(luò)實(shí)現(xiàn)了對其自助服務(wù)終端的遠(yuǎn)程監(jiān)視和控制，方便公司內(nèi)部管理，并且為用戶提供了方便的途徑完成繳費(fèi)和其他基礎(chǔ)業(yè)務(wù)。由于系統(tǒng)的復(fù)雜性，對于系統(tǒng)的分析和驗(yàn)證顯得尤為重要，這時就需要建立一種精確的可模擬系統(tǒng)動態(tài)運(yùn)行的模型。
　　在移動自助服務(wù)系統(tǒng)中，與進(jìn)程交互的外部環(huán)境也在動態(tài)地改變，具有隨機(jī)性、動態(tài)性、計算的復(fù)雜性和應(yīng)用的廣泛性。1992年，英國著名的科學(xué)家和圖靈獎獲得者Robin Miler建立和提出了P

2、i-演算理論。Pi-演算可以描述結(jié)構(gòu)不斷變化的分布式并發(fā)系統(tǒng)，是一種新的通信建模方法。所以本文采用了Pi-演算形式化方法為系統(tǒng)建模。
　　本文在對移動自助服務(wù)系統(tǒng)的繳費(fèi)流程進(jìn)行建模時，采用自頂向下的建模方法，首先在分析系統(tǒng)繳費(fèi)流程的基礎(chǔ)上，提取出其中的主要活動模塊，建立頂層的Pi-演算模型;然后細(xì)化這些模塊，詳細(xì)地分析每一個模塊包含的細(xì)節(jié)活動，繼而得出完整的Pi-演算模型;最后使用Pi-演算的形式化驗(yàn)證工具M(jìn)WB驗(yàn)證了模型的正確性

3、（如有無死鎖），而且用step命令模擬了自助服務(wù)系統(tǒng)平臺的交互運(yùn)行情況，可以看出它滿足了預(yù)期設(shè)計的要求。移動自助服務(wù)系統(tǒng)所采用的通信協(xié)議是TCP/IP協(xié)議，本文為了達(dá)到對協(xié)議進(jìn)行安全性驗(yàn)證的目的，主要分析了其中的傳輸控制協(xié)議TCP。在分析TCP協(xié)議中的數(shù)據(jù)報格式、連接的建立和釋放以及快速重傳算法的基礎(chǔ)上，對TCP建立連接時采取的三次握手協(xié)議建立了Pi-演算模型，并在MWB工具中用step命令模擬了三次握手的動態(tài)運(yùn)行，從理論的角度分析了快