基于Pi-演算的無(wú)線自動(dòng)售貨機(jī)系統(tǒng)建模與應(yīng)用.pdf

1、無(wú)線自動(dòng)售貨機(jī)系統(tǒng)通過(guò)無(wú)線網(wǎng)絡(luò)實(shí)現(xiàn)了對(duì)自動(dòng)售貨機(jī)的遠(yuǎn)程監(jiān)視和控制，便于企業(yè)內(nèi)部物流管理及向顧客提供方便的手機(jī)購(gòu)物。為了對(duì)這一復(fù)雜系統(tǒng)形成一致的理解，分析系統(tǒng)的正確性和可靠性，進(jìn)而定量評(píng)估系統(tǒng)的績(jī)效，需要建立一種嚴(yán)謹(jǐn)?shù)目赡M系統(tǒng)動(dòng)態(tài)運(yùn)行的模型。 由于無(wú)線自動(dòng)售貨機(jī)系統(tǒng)屬于離散動(dòng)態(tài)系統(tǒng)，本文采用了描述分布式并發(fā)系統(tǒng)的Pi-演算過(guò)程代數(shù)方法為系統(tǒng)建模。分別對(duì)系統(tǒng)的交易流程和物流配送過(guò)程建立了Pi-演算模型。對(duì)無(wú)線自動(dòng)售貨機(jī)系統(tǒng)的交易流

2、程的建模采用自頂向下的建模方法，首先建立系統(tǒng)的主要活動(dòng)模塊的頂層Pi-演算模型，然后對(duì)這些模塊進(jìn)行細(xì)化，最后得出系統(tǒng)交易流程完整的Pi-演算模型；并用Pi-演算的形式化輔助工具M(jìn)WB驗(yàn)證其正確性。為了能夠?qū)o(wú)線自動(dòng)售貨機(jī)系統(tǒng)物流配送過(guò)程進(jìn)行建模，本文定義了一種帶時(shí)間因素的Pi-演算，對(duì)無(wú)線自動(dòng)售貨機(jī)系統(tǒng)的物流配送過(guò)程建立了含有時(shí)間因素的Pi-演算模型；考慮到績(jī)效分析的需要，還在不同的缺貨情況下同時(shí)模擬兩種系統(tǒng)物流配送過(guò)程的運(yùn)行，通過(guò)選擇