【摘要】：針對(duì)π演算難于對(duì)時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行建模和推演,提出了一種采用擴(kuò)展π演算p-π對(duì)時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行形式化建模與推演的方法。該方法首先采用區(qū)間動(dòng)作前綴和瞬時(shí)動(dòng)作前綴分別描述系統(tǒng)的時(shí)間相關(guān)行為和交互行為,并通過操作算子將子進(jìn)程進(jìn)行復(fù)合,然后利用操作規(guī)則構(gòu)造出系統(tǒng)的時(shí)間相關(guān)標(biāo)記遷移系統(tǒng)和可接受的執(zhí)行路徑,最后基于上述遷移系統(tǒng)和執(zhí)行路徑完成對(duì)系統(tǒng)性質(zhì)的推演。對(duì)移動(dòng)車輛控制系統(tǒng)的分析表明,所提方法可對(duì)時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)進(jìn)行有效建模和推演,保證時(shí)間相關(guān)移動(dòng)并發(fā)系統(tǒng)的可靠性。
[Abstract]:Aiming at the difficulty of 蟺 calculus in modeling and deducing time-dependent mobile concurrent systems, a formal modeling and deduction method for time-dependent mobile concurrent systems using extended 蟺 calculus p- 蟺 is proposed. In this method, interval action prefix and instantaneous action prefix are used to describe the time-dependent behavior and interaction behavior of the system, respectively, and the sub-processes are recomposed by the operator. Then the time-dependent label migration system and the acceptable execution path are constructed by using the operation rules. Finally, the properties of the system are derived based on the above migration system and the execution path. The analysis of the mobile vehicle control system shows that the proposed method can effectively model and deduce the time-dependent mobile concurrent system and ensure the reliability of the time-dependent mobile concurrent system.
【作者單位】： 西安電子科技大學(xué)計(jì)算理論與技術(shù)研究所;西安電子科技大學(xué)ISN國(guó)家重點(diǎn)實(shí)驗(yàn)室;
【基金】：國(guó)家“973”重點(diǎn)基礎(chǔ)研究發(fā)展規(guī)劃資助項(xiàng)目(2010CB328102) 國(guó)家自然科學(xué)基金資助項(xiàng)目(61003078) 綜合業(yè)務(wù)網(wǎng)理論及關(guān)鍵技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室基金資助項(xiàng)目(ISN1102001)
【分類號(hào)】：TP393.09

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 張冠華,張連華,白英彩;基于進(jìn)程代數(shù)EACSR-VP的通信模型的實(shí)現(xiàn)[J];計(jì)算機(jī)應(yīng)用與軟件;2005年09期

2 李楊;程建華;房鼎益;陳曉江;馮健;;并發(fā)系統(tǒng)的安全性與活性的驗(yàn)證方法[J];計(jì)算機(jī)工程與應(yīng)用;2008年04期

3 蔣昌俊，鄭應(yīng)平，疏松桂;并發(fā)系統(tǒng)建模與分析研究[J];高技術(shù)通訊;1996年06期

4 李夢(mèng)君;李舟軍;陳火旺;;基于進(jìn)程代數(shù)的安全協(xié)議分析與驗(yàn)證[J];計(jì)算機(jī)科學(xué);2003年06期

5 應(yīng)宏;Petri網(wǎng)格構(gòu)建探討[J];微型電腦應(yīng)用;2005年09期

6 王金雙;楊華兵;張興元;王元元;張毓森;;SAODV協(xié)議在Isabelle/HOL中的正確性驗(yàn)證[J];解放軍理工大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年05期

7 王一飛;李迎春;許迅;;基于TLA的Web服務(wù)組合研究[J];微型機(jī)與應(yīng)用;2010年04期

8 董玉梅,張立臣;擴(kuò)展的模糊時(shí)間Petri網(wǎng)[J];微電子學(xué)與計(jì)算機(jī);2005年06期

9 龐士煥;朱相冰;張琦;湯萍萍;;基于TLA的正確性驗(yàn)證方法[J];計(jì)算機(jī)技術(shù)與發(fā)展;2009年03期

10 顧永跟;傅育熙;;基于進(jìn)程演算和知識(shí)推理的安全協(xié)議形式化分析[J];計(jì)算機(jī)研究與發(fā)展;2006年05期

相關(guān)會(huì)議論文 前4條

1 蔡元沛;邢薇;沙寧;;面向RIA的離線并發(fā)控制的研究[A];黑龍江省計(jì)算機(jī)學(xué)會(huì)2009年學(xué)術(shù)交流年會(huì)論文集[C];2010年

2 文靜華;張梅;張煥國(guó);;電子支付協(xié)議的博弈邏輯模型與形式化分析[A];2007年全國(guó)開放式分布與并行計(jì)算機(jī)學(xué)術(shù)會(huì)議論文集(上冊(cè))[C];2007年

3 王美姣;錢彥軍;姚紹文;余正祥;;服務(wù)組合語言在SOA中的應(yīng)用[A];云南省機(jī)械工程學(xué)會(huì)2010年年會(huì)論文集[C];2010年

4 吳亮;袁兆山;;基于模糊Petri網(wǎng)的語義Web服務(wù)組合[A];全國(guó)第20屆計(jì)算機(jī)技術(shù)與應(yīng)用學(xué)術(shù)會(huì)議（CACIS·2009）暨全國(guó)第1屆安全關(guān)鍵技術(shù)與應(yīng)用學(xué)術(shù)會(huì)議論文集（上冊(cè)）[C];2009年

相關(guān)博士學(xué)位論文 前2條

1 龍慧云;基于進(jìn)程代數(shù)的Web服務(wù)數(shù)據(jù)和組合的形式化方法研究[D];貴州大學(xué);2009年

2 陳靖;帶實(shí)時(shí)的傳值與移動(dòng)系統(tǒng)研究[D];中國(guó)科學(xué)院研究生院（軟件研究所）;2003年

相關(guān)碩士學(xué)位論文 前10條

1 付興尊;基于進(jìn)程代數(shù)的多路訪問協(xié)議模型研究與實(shí)現(xiàn)[D];華東師范大學(xué);2010年

2 張健;MMORPG服務(wù)器關(guān)鍵技術(shù)研究[D];浙江大學(xué);2006年

3 劉勇;有限PI演算的Petri網(wǎng)語義轉(zhuǎn)換研究[D];吉林大學(xué);2009年

4 康智輝;基于屬性的層次移動(dòng)IPv6（HMIPv6）協(xié)議的驗(yàn)證[D];內(nèi)蒙古大學(xué);2011年

5 張帆;基于異步π-演算的兩階段提交協(xié)議的形式化描述和驗(yàn)證[D];國(guó)防科學(xué)技術(shù)大學(xué);2006年

6 朱恒亮;SOA中服務(wù)與服務(wù)組合的形式化研究[D];福建師范大學(xué);2010年

7 宮雪強(qiáng);基于行為的Web服務(wù)相容性與可替換性研究[D];華東師范大學(xué);2010年

8 李軼，

本文編號(hào)：2137244