擴展π演算對時間相關移動并發系統的建模與推演

羅玲,段振華

(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