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

罗玲,段振华

(1.西安电子科技大学计算理论与技术研究所, 710071, 西安;2.西安电子科技大学ISN国家重点实验室, 710071, 西安)

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

罗玲1,2,段振华1,2

(1.西安电子科技大学计算理论与技术研究所, 710071, 西安;2.西安电子科技大学ISN国家重点实验室, 710071, 西安)

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

π演算;时间相关移动并发系统;形式化建模;推演

近年来,随着Software-as-a-Service(SaaS)[1]和Cloud Computing[2]等新型网络计算的发展,以并发性、移动性、时间相关性和异构性等为主要特征的时间相关移动并发系统得到人们的普遍关注,人们越来越认识到,在动态网络环境中构建时间相关移动并发系统不仅难度大、效率低,且难以发现其中隐含的缺陷和错误[3]。对于安全攸关的时间相关移动并发系统,如移动支付系统、移动通信系统、交通控制系统等,其失误和崩溃可能造成重大损失,因此时间相关移动并发系统的正确性、安全性和时间相关性等属性受到人们的重视。形式化方法以严格的数学理论为支撑,被认为是行之有效的减少设计错误、保证软件质量的重要方法。目前,该领域的研究主要集中在形式化建模和推演上。基于不同理论,各种形式化方法被相继提出,如进程代数、时序逻辑[4]以及Petri网等。π演算[5-6]作为进程代数的一个重要分支,是由Milner等人在CCS的基础上提出的,由于可以描述拓扑结构动态变化的移动通信系统,因而被广泛应用于移动并发系统的建模和推演中。然而,由于它的动作前缀未考虑时间因素,因而不适合于描述时间相关系统。近年来,已有一些研究对π演算进行相应的扩展[3,7],使其便于对时间相关系统进行建模,但这些方法基本都是直接加入时间变量,导致时间和动作前缀分开,不能反映时间相关系统的本质特点。因此,本文通过加入区间动作前缀[8]将π演算扩展为p-π,由于区间动作前缀隐含了动作消耗时间,使得p-π更适用于时间相关移动并发系统的建模和推演。

综上所述,鉴于p-π和时间相关移动并发系统的特点,本文提出采用p-π为时间相关移动并发系统建模和推演的方法。为了说明p-π能够对时间相关系统进行有效建模和推演,文中结合实例进行了展示。

1 扩展π演算p-π

1.1 语法

设N是名字集合,Prop是原子命题集合,是非负整数集合。p-π的语法定义如下

P::=0|π.P|P1+P2|P1|P2|[a1=a2]P|νaP|

A〈a1,…,an〉

进程表达式P中出现的名字记作n(P),分为自由名和受限名,分别记作fn(P)和bn(P)。其中受限名又包括两种:νaP中的a和x(y).P中的y。除此之外的都是自由名。建模时:.0常被省略;νaνbP简记为νa,bP。操作符.、[]和ν的优先级高于+和|。下面给出一些派生定义

skip0≜ε

skipn≜skip.skipn-1,n≥1

await(P) ≜ε.P+skip.P+…+skipn.P,n≥0

式中:n∈;await(P)中的P为发送动作前缀监视进程或接收动作前缀监视进程。导出进程主要用于实现引入区间动作后的进程同步通信。

1.2 语义

定义1进程同余。设≅为p-π进程集合P上的等价关系,≅被称为进程同余当且仅当,若P≅Q,则π.P≅π.Q,P+R≅Q+R,R+P≅R+Q,P|R≅Q|R,R|P≅R|Q,[a1=a2]P≅[a1=a2]Q,且νaP≅νaQ。

定义2结构同余。设≡为P上的等价关系,它由以下16个等式定义,它被称为结构同余当且仅当它是进程同余。

S1:νxP≡νy{y/x}P, ify∉fn(P)

S2:x(y).P≡x(z).{z/y}P, ifz∉fn((y)P)

S3:νx(P|Q)≡P|νxQ, ifx∉fn(P)

S4:A〈a1,…,an〉≡{a/x}PA, ifA(x1,…,xn)≜PA

S5:P|0≡PS6:P+Q≡Q+P

S7:P|Q≡Q|PS8:P|(Q|R)≡(P|Q)|R

S11:ε.P≡PS12:P+(Q+R)≡(P+Q)+R

S13:P+0≡PS14:[x=y]P≡0,ifx≠y

S15:νxyP≡νyxPS16:skip.P+skip.Q≡skip.(P+Q)

易证得≡是进程同余,故≡是P上的结构同余。对于任意的P,Q∈P,若能通过多次应用以上等式将P转换为Q,就说P和Q是结构同余的,记作P≡Q。

2 时间相关移动并发系统建模实例

时间相关移动并发系统是一类以移动性、并发性为主要特征并对系统行为的时序性要求严格的系统。移动车辆控制系统(MVCS)最早出现于文献[5],常被作为表现系统移动性的实例,但以往的分析中,都未对系统的时间相关行为建模和推演,本节以MVCS为例,展示p-π对时间相关移动并发系统的建模。

2.1MVCS的系统描述

MVCS的移动通信网络通常包括控制中心、站点和车辆,控制中心负责与站点通信,站点负责与控制中心和与其处于连接状态的车辆通信。通常,系统结构的移动性[5]包括很多方式,如建立或销毁通信连接、建立或销毁通信进程等。在移动性方面,本例关注通信连接的建立和销毁,即随着车辆的移动,它将销毁与初始站点的连接,继而建立与新站点的连接的过程。

图1给出了MVCS移动通信的网络拓扑结构图。该系统只考虑控制中心C,3个站点T1、T2和T3,2辆车B1和B2。Ti(i=1,2,3)表现为两种状态:当与Bj(j=1,2)连接时表现为Ti;当与Bj断开时表现为IDTi。图1和系统建模所需名字的定义和用途如表1所示,其中:i=1,2,3;j=1,2;1≤k≤15。

表1 系统名字定义及用途

图1 MVCS的移动通信过程

系统功能包括5部分:①控制信号的接收和发送,C接到控制信号后,将该信号传送到相应站点Ti,继而由该站点传给Bj,Bj在接收到该信号后执行该信号;②连接站点的切换,假设B1先与T1连接,则C会先将用于完成B1与新站点T2通信的通道通过T1传给B1,再将该通道传给IDT2,这样就建立了T2和B1的连接,即完成了站点切换,如图1所示;③路况信息的监测,站点Ti可监测路况信息,当出现拥塞时,Ti会将监测到的局部拥塞信息发送给C;④拥塞信息的广播,C接收来自各个站点的局部拥塞信息,然后对信息处理后将全局拥塞信息通过站点广播给与各站点相连接的车辆;⑤车辆间通信连接的建立,假设B1需要与B2进行通信连接,那么B1先发出建立连接的申请,该申请会通过T1、C和T3传递给B2,B2接收申请后,若同意建立连接,则将应答信息反馈回B1,即完成通信连接的建立。该系统涉及的时间相关约束为:切换信息的传输占用1到2个时间单元;断开和建立连接的过程占用2个时间单元;车辆在接收建立连接的应答时最多等待5个时间单元,超过5个时间单元将执行超时处理;站点处理局部拥塞信息占用1个时间单元,控制中心处理全局拥塞信息占用3个时间单元;通过自由名的发送和接收动作是异步交互,故其执行不需要等待时间;通过受限名的发送和接收动作是同步交互,故要等待与之同步的接收和发送动作。

2.2MVCS的建模

依据系统描述,该系统由6个子进程并行构成

νn(C〈nc〉|T1〈nt1〉|IDT2〈nt2〉|T3〈nt3〉|

B1〈nb1〉|B2〈nb2〉)

鉴于表1名字的定义,C的进程定义为

C2≜skip2.C7

C6≜await(d1.C11)

C11≜await(d3.C14)

C12≜skip2.C〈n2〉

C15≜skip3.(C16|C17)

T1与T2的定义类似,差别在于所涉及的具体通道名的标号不同,故在此只给出T1和T3的具体定义

IDTi的进程定义如下

Bj的进程定义如下

3 时间相关移动并发系统推演实例

为便于推演进程,首先介绍可观察动作πo和操作规则。

πt::=IP|skip

3.1 基于操作规则的系统迁移

依据操作规则,可得到系统的时间相关标记迁移系统TDLTS的定义。

定义3对于任意的p-π进程P,P的TDLTS由四元组(P,P0,L,T)表示,其中P是p-π进程集合,P0是初始进程,L是可观察动作集合,T是迁移集合。元组构造如下:

(1)P0=P且P0∈P;

(3)有限次地应用(1)和(2),生成P的TDLTS。

MVCS的TDLTS如图2所示,该图部分描述了系统的时间相关迁移过程,其中Pi(0≤i≤57)是形如νn(C〈nc〉|T1〈nt1〉|IDT2〈nt2〉|T3〈nt3〉|B1〈nb1〉|B2〈nb2〉)的进程。

图2 MVCS的部分TDLTS

由于TDLTS的四元组定义中不包括可接受进程,即终止进程,考虑到系统推演的可终止性,本文确定终止进程集合为{0,P0},即可接受的执行路径或到达0,或经过循环过程到达初始进程P0,考察的可接受的有穷和无穷路径定义如下。

3.2 基于系统迁移的系统推演

本小节将通过系统的TDLTS和可接受执行路径来分析系统的行为和期望性质。本文关注活性、安全性、时间约束性、及时性以及移动性,其中:活性指在一定条件下系统期望的行为终究会发生;安全性指在任何条件下系统避免的行为都不会发生[9];时间约束性指系统行为的发生要满足一定时间约束;及时性指进程能发生瞬时动作时,优先选择瞬时动作,而丢弃区间动作[7];移动性指系统拓扑结构的变化性[5]。

对于该系统,进行以下推演。

(2)安全性:对于TDLTS中的所有进程,除了0进程外不存在不能进行迁移的进程,即死进程。遍历TDLTS的所有进程,可得到系统中的进程都存在可迁移的执行动作,故系统满足该性质。

(4)及时性:对于TDLTS的所有进程,若该进程能够发生瞬时动作,将优先执行瞬时动作,而不会发生区间动作,直到所有可执行的瞬时动作都执行完才执行区间动作;遍历TDLTS的所有进程可得,不存在进程使得该进程可执行的迁移既包括区间动作,又包括瞬时动作,故系统满足该性质。

4 结 论

针对时间相关移动并发系统需要同时对系统交互行为和时间相关行为进行建模和分析的需求,本文提出了一种采用扩展π演算p-π对时间相关移动并发系统建模和推演的方法,并结合移动车辆控制系统实例进行了说明。结果表明:采用区间动作前缀将时间与动作前缀绑定的方法来对时间相关行为建模,从理论上来说,更符合进程代数的演算范畴,故使得部分适用于瞬时动作的规则可在区间动作上实现复用,因而便于系统推演;在对时间相关行为建模时,并未引入额外操作符,而只扩展了动作前缀,使得基于π演算的丰富的代数理论经过细微的更改便可适用于时间相关移动并发系统的推演;在对系统行为推演时,本文不仅对常用的安全性和活性等性质进行了推演,还对时间约束性、及时性以及移动性等重要但一般不易于推演的性质进行了推演。因此,该方法在对时间相关移动并发系统建模和推演方面是可行、有效的,保证了时间相关移动并发系统的可靠性。

[1] 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.

[2] 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.

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

[4] 王小兵, 段振华. 面向扩展投影时序逻辑的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.

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

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

[7] 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.

[8] 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.

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

(编辑 赵炜)

ModelingandReasoningofTime-DependentConcurrentMobileSystemsBasedonanExtendedπ-Calculus

LUO Ling1,2,DUAN Zhenhua1,2

(1. Institute of Computing Theory & Technology, Xidian University, Xi’an 710071, China;2. State Key Laboratory of Integrated Service Networks, Xidian University, Xi’an 710071, China)

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.

π-calculus; time-dependent concurrent mobile system; formal modeling; reasoning

2014-01-20。

罗玲(1986—),女,博士生;段振华(通信作者),男,教授,博士生导师。

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

10.7652/xjtuxb201409006

TP393

:A

:0253-987X(2014)09-0030-07