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

Modeling and Reasoning of Time-Dependent Concurrent Mobile Systems Based on an Extendedπ-Calculus

作　　者：罗玲[1,2] 段振华[1,2] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,西安710071 [2]西安电子科技大学ISN国家重点实验室,西安710071

出　　处：《西安交通大学学报》2014年第9期30-36,共7页Journal of Xi'an Jiaotong University

基　　金：国家"973"重点基础研究发展规划资助项目(2010CB328102);国家自然科学基金资助项目(61003078);综合业务网理论及关键技术国家重点实验室基金资助项目(ISN1102001)

摘　　要：针对π演算难于对时间相关移动并发系统进行建模和推演,提出了一种采用扩展π演算p-π对时间相关移动并发系统进行形式化建模与推演的方法。该方法首先采用区间动作前缀和瞬时动作前缀分别描述系统的时间相关行为和交互行为,并通过操作算子将子进程进行复合,然后利用操作规则构造出系统的时间相关标记迁移系统和可接受的执行路径,最后基于上述迁移系统和执行路径完成对系统性质的推演。对移动车辆控制系统的分析表明,所提方法可对时间相关移动并发系统进行有效建模和推演,保证时间相关移动并发系统的可靠性。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 subprocesses,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 timedependent concurrent mobile systems.

关 键 词：Π演算 时间相关移动并发系统 形式化建模 推演 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]