扩展π演算对时间相关移动并发系统的建模与推演

发布时间：2018-07-22 11:07

【摘要】：针对π演算难于对时间相关移动并发系统进行建模和推演,提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,最后基于上述迁移系统和执行路径完成对系统性质的推演。对移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。
[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.
【作者单位】： 西安电子科技大学计算理论与技术研究所;西安电子科技大学ISN国家重点实验室;
【基金】：国家“973”重点基础研究发展规划资助项目(2010CB328102) 国家自然科学基金资助项目(61003078) 综合业务网理论及关键技术国家重点实验室基金资助项目(ISN1102001)
【分类号】：TP393.09

【相似文献】

相关期刊论文 前10条

1 张冠华,张连华,白英彩;基于进程代数EACSR-VP的通信模型的实现[J];计算机应用与软件;2005年09期

2 李杨;程建华;房鼎益;陈晓江;冯健;;并发系统的安全性与活性的验证方法[J];计算机工程与应用;2008年04期

3 蒋昌俊，郑应平，疏松桂;并发系统建模与分析研究[J];高技术通讯;1996年06期

4 李梦君;李舟军;陈火旺;;基于进程代数的安全协议分析与验证[J];计算机科学;2003年06期

5 应宏;Petri网格构建探讨[J];微型电脑应用;2005年09期

6 王金双;杨华兵;张兴元;王元元;张毓森;;SAODV协议在Isabelle/HOL中的正确性验证[J];解放军理工大学学报(自然科学版);2008年05期

7 王一飞;李迎春;许迅;;基于TLA的Web服务组合研究[J];微型机与应用;2010年04期

8 董玉梅,张立臣;扩展的模糊时间Petri网[J];微电子学与计算机;2005年06期

9 庞士焕;朱相冰;张琦;汤萍萍;;基于TLA的正确性验证方法[J];计算机技术与发展;2009年03期

10 顾永跟;傅育熙;;基于进程演算和知识推理的安全协议形式化分析[J];计算机研究与发展;2006年05期

相关会议论文 前4条

1 蔡元沛;邢薇;沙宁;;面向RIA的离线并发控制的研究[A];黑龙江省计算机学会2009年学术交流年会论文集[C];2010年

2 文静华;张梅;张焕国;;电子支付协议的博弈逻辑模型与形式化分析[A];2007年全国开放式分布与并行计算机学术会议论文集(上册)[C];2007年

3 王美姣;钱彦军;姚绍文;余正祥;;服务组合语言在SOA中的应用[A];云南省机械工程学会2010年年会论文集[C];2010年

4 吴亮;袁兆山;;基于模糊Petri网的语义Web服务组合[A];全国第20届计算机技术与应用学术会议（CACIS·2009）暨全国第1届安全关键技术与应用学术会议论文集（上册）[C];2009年

相关博士学位论文 前2条

1 龙慧云;基于进程代数的Web服务数据和组合的形式化方法研究[D];贵州大学;2009年

2 陈靖;带实时的传值与移动系统研究[D];中国科学院研究生院（软件研究所）;2003年

相关硕士学位论文 前10条

1 付兴尊;基于进程代数的多路访问协议模型研究与实现[D];华东师范大学;2010年

2 张健;MMORPG服务器关键技术研究[D];浙江大学;2006年

3 刘勇;有限PI演算的Petri网语义转换研究[D];吉林大学;2009年

4 康智辉;基于属性的层次移动IPv6（HMIPv6）协议的验证[D];内蒙古大学;2011年

5 张帆;基于异步π-演算的两阶段提交协议的形式化描述和验证[D];国防科学技术大学;2006年

6 朱恒亮;SOA中服务与服务组合的形式化研究[D];福建师范大学;2010年

7 宫雪强;基于行为的Web服务相容性与可替换性研究[D];华东师范大学;2010年

8 李轶，

本文编号：2137244