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

罗玲 1; 2; 段振华 1; 2

doi:10.7652/xjtuxb201409006

您当前的位置：

首页 >

文章列表页 >

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

更新时间：2025-07-09

- 扩展π演算对时间相关移动并发系统的建模与推演
- Modeling and Reasoning of Time-Dependent Concurrent Mobile Systems Based on an Extended π-Calculus
- 西安交通大学学报 2014年48卷第9期页码：30-36
- 作者机构：
  
  1. 西安电子科技大学计算理论与技术研究所,西安,710071
  2. 西安电子科技大学ISN国家重点实验室,西安,710071
- 作者简介：
- 基金信息：
  
  : 2014-01-20。作者简介: 罗玲(1986—),女,博士生;段振华(通信作者),男,教授,博士生导师。基金项目: 国家“973”重点基础研究发展规划资助项目(2010CB328102);国家自然科学基金资助项目(61003078);综合业务网理论及关键技术国家重点实验室基金资助项目(ISN1102001)
- DOI：10.7652/xjtuxb201409006
  中图分类号： TP393
- 网络首发：2014-09-10，
  
  纸质出版：2014
- 稿件说明：
移动端阅览
罗玲 1, 2, 段振华 1, 等. 扩展π演算对时间相关移动并发系统的建模与推演[J]. 西安交通大学学报, 2014,48(9):30-36.

Modeling and Reasoning of Time-Dependent Concurrent Mobile Systems Based on an Extended π-Calculus[J]. 2014, 48(9): 30-36.
罗玲 1, 2, 段振华 1, 等. 扩展π演算对时间相关移动并发系统的建模与推演[J]. 西安交通大学学报, 2014,48(9):30-36. DOI： 10.7652/xjtuxb201409006.

Modeling and Reasoning of Time-Dependent Concurrent Mobile Systems Based on an Extended π-Calculus[J]. 2014, 48(9): 30-36. DOI： 10.7652/xjtuxb201409006.

摘要

针对π演算难于对时间相关移动并发系统进行建模和推演

提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为

并通过操作算子将子进程进行复合

然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径

最后基于上述迁移系统和执行路径完成对系统性质的推演。对移动车辆控制系统的分析表明

所提方法可对时间相关移动并发系统进行有效建模和推演

保证时间相关移动并发系统的可靠性。

Abstract

A method based on an extended π-Calculus

called p-π

is presented to formally model and reason time-dependent concurrent mobile systems by considering the fact that π-calculus has difficulty in modeling and reasoning time-dependent concurrent mobile systems. Both the interval action prefixes and the instantaneous action prefixes are employed to respectively describe the time-dependent behaviors and communications of systems. Operators are used to composite sub-processes

and then operational rules are utilized to construct a time-dependent labeled transition system and acceptable executive paths of the system. The properties of the system are then deduced by means of the transition system and the acceptable executive paths. Experimental analyses on a mobile vehicle control system(MVCS)show that the approach effectively models and reasons time-dependent concurrent mobile systems

and improves the reliability of time-dependent concurrent mobile systems.

关键词

Keywords

references

KIM W, LEE J H, HONG C, et al. An innovative method for data and software integration in SaaS[J]. Computers & Mathematics with Applications, 2012, 64(5): 1252-1258.

SUBASHINI S, KAVITHA V. A survey on security issues in service delivery models of cloud computing[J]. Journal of Network and Computer Applications, 2011, 34(1): 1-11.

BERGER M F. Towards abstractions for distributed systems[D]. London, UK: University of Imperial College, 2002.

王小兵, 段振华. 面向扩展投影时序逻辑的Web服务模型检测[J]. 西安交通大学学报, 2009, 43(4): 39-44.

WANG Xiaobing, DUAN Zhenhua. Projection temporal logic oriented model checking for web services[J]. Journal of Xi'an Jiaotong University, 2009, 43(4): 39-44.

MILNER R. Communicating and mobile systems: the π-calculus[M]. Cambridge, UK: Cambridge University Press, 1999: 87-112.

MILNER R, PARROW J, WALKER D. A calculus of mobile processes[J]. Journal of Information and Computation, 1992, 100(9): 41-77.

LEE J, ZIC J. On modeling real-time mobile processes[C]∥Proceedings of 25th Australian Computer Science Communications. Piscataway, NJ, USA: IEEE, 2002: 139-147.

LUO Ling, DUAN Zhenhua. An extended π-calculus[C]∥Proceedings of 2th International Conference on Computers, Networks, Systems and Industrial Applications. Sandy Bay, Tasmania, Australia: SERSC, 2012: 632-637.

ALPERN B, SCHNEIDER F B. Recognizing safety and liveness[J]. Distributed Computing, 1987, 2(3): 117-126.

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

隧道内燃料电池汽车氢气泄漏扩散特性及影响因素

水蒸气掺混对氨裂解气旋流燃烧与排放特性的影响研究

离子液体改性燃料的电流体动力学效应研究

采用试验设计方法的第三代CO2气体箔轴承箔片几何参数敏感性分析

多工况下离心压气机叶轮-机匣一体联合设计优化