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

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

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

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