羅玲,段振華

(1.西安電子科技大學(xué)計算理論與技術(shù)研究所, 710071, 西安;2.西安電子科技大學(xué)ISN國家重點實驗室, 710071, 西安)

擴(kuò)展π演算對時間相關(guān)移動并發(fā)系統(tǒng)的建模與推演

羅玲1,2,段振華1,2

(1.西安電子科技大學(xué)計算理論與技術(shù)研究所, 710071, 西安;2.西安電子科技大學(xué)ISN國家重點實驗室, 710071, 西安)

針對π演算難于對時間相關(guān)移動并發(fā)系統(tǒng)進(jìn)行建模和推演,提出了一種采用擴(kuò)展π演算p-π對時間相關(guān)移動并發(fā)系統(tǒng)進(jìn)行形式化建模與推演的方法。該方法首先采用區(qū)間動作前綴和瞬時動作前綴分別描述系統(tǒng)的時間相關(guān)行為和交互行為,并通過操作算子將子進(jìn)程進(jìn)行復(fù)合,然后利用操作規(guī)則構(gòu)造出系統(tǒng)的時間相關(guān)標(biāo)記遷移系統(tǒng)和可接受的執(zhí)行路徑,最后基于上述遷移系統(tǒng)和執(zhí)行路徑完成對系統(tǒng)性質(zhì)的推演。對移動車輛控制系統(tǒng)的分析表明,所提方法可對時間相關(guān)移動并發(fā)系統(tǒng)進(jìn)行有效建模和推演,保證時間相關(guān)移動并發(fā)系統(tǒng)的可靠性。

π演算;時間相關(guān)移動并發(fā)系統(tǒng);形式化建模;推演

近年來,隨著Software-as-a-Service(SaaS)[1]和Cloud Computing[2]等新型網(wǎng)絡(luò)計算的發(fā)展,以并發(fā)性、移動性、時間相關(guān)性和異構(gòu)性等為主要特征的時間相關(guān)移動并發(fā)系統(tǒng)得到人們的普遍關(guān)注,人們越來越認(rèn)識到,在動態(tài)網(wǎng)絡(luò)環(huán)境中構(gòu)建時間相關(guān)移動并發(fā)系統(tǒng)不僅難度大、效率低,且難以發(fā)現(xiàn)其中隱含的缺陷和錯誤[3]。對于安全攸關(guān)的時間相關(guān)移動并發(fā)系統(tǒng),如移動支付系統(tǒng)、移動通信系統(tǒng)、交通控制系統(tǒng)等,其失誤和崩潰可能造成重大損失,因此時間相關(guān)移動并發(fā)系統(tǒng)的正確性、安全性和時間相關(guān)性等屬性受到人們的重視。形式化方法以嚴(yán)格的數(shù)學(xué)理論為支撐,被認(rèn)為是行之有效的減少設(shè)計錯誤、保證軟件質(zhì)量的重要方法。目前,該領(lǐng)域的研究主要集中在形式化建模和推演上?；诓煌碚?各種形式化方法被相繼提出,如進(jìn)程代數(shù)、時序邏輯[4]以及Petri網(wǎng)等。π演算[5-6]作為進(jìn)程代數(shù)的一個重要分支,是由Milner等人在CCS的基礎(chǔ)上提出的,由于可以描述拓?fù)浣Y(jié)構(gòu)動態(tài)變化的移動通信系統(tǒng),因而被廣泛應(yīng)用于移動并發(fā)系統(tǒng)的建模和推演中。然而,由于它的動作前綴未考慮時間因素,因而不適合于描述時間相關(guān)系統(tǒng)。近年來,已有一些研究對π演算進(jìn)行相應(yīng)的擴(kuò)展[3,7],使其便于對時間相關(guān)系統(tǒng)進(jìn)行建模,但這些方法基本都是直接加入時間變量,導(dǎo)致時間和動作前綴分開,不能反映時間相關(guān)系統(tǒng)的本質(zhì)特點。因此,本文通過加入?yún)^(qū)間動作前綴[8]將π演算擴(kuò)展為p-π,由于區(qū)間動作前綴隱含了動作消耗時間,使得p-π更適用于時間相關(guān)移動并發(fā)系統(tǒng)的建模和推演。

綜上所述,鑒于p-π和時間相關(guān)移動并發(fā)系統(tǒng)的特點,本文提出采用p-π為時間相關(guān)移動并發(fā)系統(tǒng)建模和推演的方法。為了說明p-π能夠?qū)r間相關(guān)系統(tǒng)進(jìn)行有效建模和推演,文中結(jié)合實例進(jìn)行了展示。

1 擴(kuò)展π演算p-π

1.1 語法

設(shè)N是名字集合,Prop是原子命題集合,是非負(fù)整數(shù)集合。p-π的語法定義如下

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

A〈a1,…,an〉

進(jìn)程表達(dá)式P中出現(xiàn)的名字記作n(P),分為自由名和受限名,分別記作fn(P)和bn(P)。其中受限名又包括兩種:νaP中的a和x(y).P中的y。除此之外的都是自由名。建模時:.0常被省略;νaνbP簡記為νa,bP。操作符.、[]和ν的優(yōu)先級高于+和|。下面給出一些派生定義

skip0?ε

skipn?skip.skipn-1,n≥1

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

式中:n∈;await(P)中的P為發(fā)送動作前綴監(jiān)視進(jìn)程或接收動作前綴監(jiān)視進(jìn)程。導(dǎo)出進(jìn)程主要用于實現(xiàn)引入?yún)^(qū)間動作后的進(jìn)程同步通信。

1.2 語義

定義1進(jìn)程同余。設(shè)?為p-π進(jìn)程集合P上的等價關(guān)系,?被稱為進(jìn)程同余當(dāng)且僅當(dāng),若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結(jié)構(gòu)同余。設(shè)≡為P上的等價關(guān)系,它由以下16個等式定義,它被稱為結(jié)構(gòu)同余當(dāng)且僅當(dāng)它是進(jìn)程同余。

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)

易證得≡是進(jìn)程同余,故≡是P上的結(jié)構(gòu)同余。對于任意的P,Q∈P,若能通過多次應(yīng)用以上等式將P轉(zhuǎn)換為Q,就說P和Q是結(jié)構(gòu)同余的,記作P≡Q。

2 時間相關(guān)移動并發(fā)系統(tǒng)建模實例

時間相關(guān)移動并發(fā)系統(tǒng)是一類以移動性、并發(fā)性為主要特征并對系統(tǒng)行為的時序性要求嚴(yán)格的系統(tǒng)。移動車輛控制系統(tǒng)(MVCS)最早出現(xiàn)于文獻(xiàn)[5],常被作為表現(xiàn)系統(tǒng)移動性的實例,但以往的分析中,都未對系統(tǒng)的時間相關(guān)行為建模和推演,本節(jié)以MVCS為例,展示p-π對時間相關(guān)移動并發(fā)系統(tǒng)的建模。

2.1MVCS的系統(tǒng)描述

MVCS的移動通信網(wǎng)絡(luò)通常包括控制中心、站點和車輛,控制中心負(fù)責(zé)與站點通信,站點負(fù)責(zé)與控制中心和與其處于連接狀態(tài)的車輛通信。通常,系統(tǒng)結(jié)構(gòu)的移動性[5]包括很多方式,如建立或銷毀通信連接、建立或銷毀通信進(jìn)程等。在移動性方面,本例關(guān)注通信連接的建立和銷毀,即隨著車輛的移動,它將銷毀與初始站點的連接,繼而建立與新站點的連接的過程。

圖1給出了MVCS移動通信的網(wǎng)絡(luò)拓?fù)浣Y(jié)構(gòu)圖。該系統(tǒng)只考慮控制中心C,3個站點T1、T2和T3,2輛車B1和B2。Ti(i=1,2,3)表現(xiàn)為兩種狀態(tài):當(dāng)與Bj(j=1,2)連接時表現(xiàn)為Ti;當(dāng)與Bj斷開時表現(xiàn)為IDTi。圖1和系統(tǒng)建模所需名字的定義和用途如表1所示,其中:i=1,2,3;j=1,2;1≤k≤15。

表1 系統(tǒng)名字定義及用途

圖1 MVCS的移動通信過程

系統(tǒng)功能包括5部分:①控制信號的接收和發(fā)送,C接到控制信號后,將該信號傳送到相應(yīng)站點Ti,繼而由該站點傳給Bj,Bj在接收到該信號后執(zhí)行該信號;②連接站點的切換,假設(shè)B1先與T1連接,則C會先將用于完成B1與新站點T2通信的通道通過T1傳給B1,再將該通道傳給IDT2,這樣就建立了T2和B1的連接,即完成了站點切換,如圖1所示;③路況信息的監(jiān)測,站點Ti可監(jiān)測路況信息,當(dāng)出現(xiàn)擁塞時,Ti會將監(jiān)測到的局部擁塞信息發(fā)送給C;④擁塞信息的廣播,C接收來自各個站點的局部擁塞信息,然后對信息處理后將全局擁塞信息通過站點廣播給與各站點相連接的車輛;⑤車輛間通信連接的建立,假設(shè)B1需要與B2進(jìn)行通信連接,那么B1先發(fā)出建立連接的申請,該申請會通過T1、C和T3傳遞給B2,B2接收申請后,若同意建立連接,則將應(yīng)答信息反饋回B1,即完成通信連接的建立。該系統(tǒng)涉及的時間相關(guān)約束為:切換信息的傳輸占用1到2個時間單元;斷開和建立連接的過程占用2個時間單元;車輛在接收建立連接的應(yīng)答時最多等待5個時間單元,超過5個時間單元將執(zhí)行超時處理;站點處理局部擁塞信息占用1個時間單元,控制中心處理全局擁塞信息占用3個時間單元;通過自由名的發(fā)送和接收動作是異步交互,故其執(zhí)行不需要等待時間;通過受限名的發(fā)送和接收動作是同步交互,故要等待與之同步的接收和發(fā)送動作。

2.2MVCS的建模

依據(jù)系統(tǒng)描述,該系統(tǒng)由6個子進(jìn)程并行構(gòu)成

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

B1〈nb1〉|B2〈nb2〉)

鑒于表1名字的定義,C的進(jìn)程定義為

C2?skip2.C7

C6?await(d1.C11)

C11?await(d3.C14)

C12?skip2.C〈n2〉

C15?skip3.(C16|C17)

T1與T2的定義類似,差別在于所涉及的具體通道名的標(biāo)號不同,故在此只給出T1和T3的具體定義

IDTi的進(jìn)程定義如下

Bj的進(jìn)程定義如下

3 時間相關(guān)移動并發(fā)系統(tǒng)推演實例

為便于推演進(jìn)程,首先介紹可觀察動作πo和操作規(guī)則。

πt::=IP|skip

3.1 基于操作規(guī)則的系統(tǒng)遷移

依據(jù)操作規(guī)則,可得到系統(tǒng)的時間相關(guān)標(biāo)記遷移系統(tǒng)TDLTS的定義。

定義3對于任意的p-π進(jìn)程P,P的TDLTS由四元組(P,P0,L,T)表示,其中P是p-π進(jìn)程集合,P0是初始進(jìn)程,L是可觀察動作集合,T是遷移集合。元組構(gòu)造如下:

(1)P0=P且P0∈P;

(3)有限次地應(yīng)用(1)和(2),生成P的TDLTS。

MVCS的TDLTS如圖2所示,該圖部分描述了系統(tǒng)的時間相關(guān)遷移過程,其中Pi(0≤i≤57)是形如νn(C〈nc〉|T1〈nt1〉|IDT2〈nt2〉|T3〈nt3〉|B1〈nb1〉|B2〈nb2〉)的進(jìn)程。

圖2 MVCS的部分TDLTS

由于TDLTS的四元組定義中不包括可接受進(jìn)程,即終止進(jìn)程,考慮到系統(tǒng)推演的可終止性,本文確定終止進(jìn)程集合為{0,P0},即可接受的執(zhí)行路徑或到達(dá)0,或經(jīng)過循環(huán)過程到達(dá)初始進(jìn)程P0,考察的可接受的有窮和無窮路徑定義如下。

3.2 基于系統(tǒng)遷移的系統(tǒng)推演

本小節(jié)將通過系統(tǒng)的TDLTS和可接受執(zhí)行路徑來分析系統(tǒng)的行為和期望性質(zhì)。本文關(guān)注活性、安全性、時間約束性、及時性以及移動性,其中:活性指在一定條件下系統(tǒng)期望的行為終究會發(fā)生;安全性指在任何條件下系統(tǒng)避免的行為都不會發(fā)生[9];時間約束性指系統(tǒng)行為的發(fā)生要滿足一定時間約束;及時性指進(jìn)程能發(fā)生瞬時動作時,優(yōu)先選擇瞬時動作,而丟棄區(qū)間動作[7];移動性指系統(tǒng)拓?fù)浣Y(jié)構(gòu)的變化性[5]。

對于該系統(tǒng),進(jìn)行以下推演。

(2)安全性:對于TDLTS中的所有進(jìn)程,除了0進(jìn)程外不存在不能進(jìn)行遷移的進(jìn)程,即死進(jìn)程。遍歷TDLTS的所有進(jìn)程,可得到系統(tǒng)中的進(jìn)程都存在可遷移的執(zhí)行動作,故系統(tǒng)滿足該性質(zhì)。

(4)及時性:對于TDLTS的所有進(jìn)程,若該進(jìn)程能夠發(fā)生瞬時動作,將優(yōu)先執(zhí)行瞬時動作,而不會發(fā)生區(qū)間動作,直到所有可執(zhí)行的瞬時動作都執(zhí)行完才執(zhí)行區(qū)間動作;遍歷TDLTS的所有進(jìn)程可得,不存在進(jìn)程使得該進(jìn)程可執(zhí)行的遷移既包括區(qū)間動作,又包括瞬時動作,故系統(tǒng)滿足該性質(zhì)。

4 結(jié) 論

針對時間相關(guān)移動并發(fā)系統(tǒng)需要同時對系統(tǒng)交互行為和時間相關(guān)行為進(jìn)行建模和分析的需求,本文提出了一種采用擴(kuò)展π演算p-π對時間相關(guān)移動并發(fā)系統(tǒng)建模和推演的方法,并結(jié)合移動車輛控制系統(tǒng)實例進(jìn)行了說明。結(jié)果表明:采用區(qū)間動作前綴將時間與動作前綴綁定的方法來對時間相關(guān)行為建模,從理論上來說,更符合進(jìn)程代數(shù)的演算范疇,故使得部分適用于瞬時動作的規(guī)則可在區(qū)間動作上實現(xiàn)復(fù)用,因而便于系統(tǒng)推演;在對時間相關(guān)行為建模時,并未引入額外操作符,而只擴(kuò)展了動作前綴,使得基于π演算的豐富的代數(shù)理論經(jīng)過細(xì)微的更改便可適用于時間相關(guān)移動并發(fā)系統(tǒng)的推演;在對系統(tǒng)行為推演時,本文不僅對常用的安全性和活性等性質(zhì)進(jìn)行了推演,還對時間約束性、及時性以及移動性等重要但一般不易于推演的性質(zhì)進(jìn)行了推演。因此,該方法在對時間相關(guān)移動并發(fā)系統(tǒng)建模和推演方面是可行、有效的,保證了時間相關(guān)移動并發(fā)系統(tǒng)的可靠性。

[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] 王小兵, 段振華. 面向擴(kuò)展投影時序邏輯的Web服務(wù)模型檢測 [J]. 西安交通大學(xué)學(xué)報, 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—),女,博士生;段振華(通信作者),男,教授,博士生導(dǎo)師。

國家“973”重點基礎(chǔ)研究發(fā)展規(guī)劃資助項目(2010CB328102);國家自然科學(xué)基金資助項目(61003078);綜合業(yè)務(wù)網(wǎng)理論及關(guān)鍵技術(shù)國家重點實驗室基金資助項目(ISN1102001)。

10.7652/xjtuxb201409006

TP393

:A

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