May測(cè)試語義前同余性的研究

南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院　鄧鵬輝　張晉津

?

May測(cè)試語義前同余性的研究

南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院鄧鵬輝張晉津

【摘要】在面向服務(wù)器的進(jìn)程代數(shù)理論中，為了描述服務(wù)器和客戶之間的并發(fā)行為，Bernardi和Hennessy等人提出了三種must-testing語義，并對(duì)它們的前同余性以及公理系統(tǒng)進(jìn)行了研究。但是關(guān)于may-testing語義并未涉及，本文將對(duì)可能測(cè)試語義的前同余性進(jìn)行研究。

【關(guān)鍵詞】進(jìn)程代數(shù)；并發(fā)行為；may-testing語義；前同余性

0　引言

在進(jìn)程代數(shù)理論中，Nicola和Hennessy早期提出三種測(cè)試語義(may,must,may&must)用來描述精化關(guān)系，基于被測(cè)試進(jìn)程與環(huán)境間的相互作用誘導(dǎo)出的計(jì)算路徑序列，分析其行為[1][2]。近幾年，Barbanera, Liguoro, Castagna等人提出面向網(wǎng)絡(luò)服務(wù)器的必須測(cè)試?yán)碚揫3]，Bernardi和Hennessy提出了面向網(wǎng)絡(luò)服務(wù)器的CLT語義以及SVR語義用于描述必然測(cè)試(must-testing)語義精化關(guān)系[4]。它介紹了兩種子行為關(guān)系：服務(wù)器(server)和客戶(client)，它們的語法一致，都可以看成進(jìn)程，并描述了它們之間的相互作用。而基于網(wǎng)絡(luò)服務(wù)器的may-testing語義在文獻(xiàn)[4]中并未涉及。本文基于網(wǎng)絡(luò)服務(wù)器的概念，對(duì)may-testing測(cè)試語義的前同余性進(jìn)行研究。

1　預(yù)備知識(shí)

本節(jié)簡(jiǎn)單介紹may-testing測(cè)試語義的語法及其結(jié)構(gòu)化操作語義規(guī)則，CLT測(cè)試前序的語法以及語義定義，以及飽和集的概念。關(guān)于may-testing測(cè)試語義的更多詳細(xì)介紹可以參考文獻(xiàn)[2]。本文所使用的符號(hào)都是常用符號(hào)，其基本含義與Milner在文獻(xiàn)[4][5]中使用的意義一致。

定義1[3]May-testing語義的項(xiàng)(進(jìn)程)由BNF范式定義如下：

表1羅列了 May-testing語義的結(jié)構(gòu)化操作語義規(guī)則，表中。

表1　結(jié)構(gòu)操作語義規(guī)則

具有如下形式的轉(zhuǎn)換序列稱為p||r的一條計(jì)算路徑p||r=p0||r0→p1||r1→…→pk||rk→…。如果它是無限的或者它的最終狀態(tài)pn||rn滿足pn||rn，則稱它是極大的；如果存在滿足rk，則稱它是成功的。如果存在一條p||r的極大計(jì)算路徑是客戶成功的，則稱p可能滿足 r，記為p may r。

2　may-testing前序的語法定義

本節(jié)給出may-testing語義的兩種語義定義，并證明它們是等價(jià)的。

定義2 給定進(jìn)程r1、r2，如果對(duì)任意進(jìn)程p，使得p may r1蘊(yùn)涵p may r2，則稱r1是r2的精化，記為。

定義3 給定進(jìn)程r1、r2，，如果對(duì)s的任意前綴，使得蘊(yùn)涵，則稱r1是r2的精煉，記為。

定理1 對(duì)任意客戶r1、r2，當(dāng)且僅當(dāng)。

3　may-testing前序的前同余性

在前面一節(jié)介紹了兩種等價(jià)的may-testing前序的語法定義，而同余性是組合推理的基礎(chǔ)，這節(jié)我們將證明該測(cè)試前序具有同余性。

情形1 前綴算子a。

情形2 選擇算子+。

假設(shè)r1+r2并且a.是a.并且是s的前綴使得。從而r1或者r2，不是一般性，假設(shè)r1，從而。由r1可知存在s的前綴使得，所以r1+r2。

4　結(jié)束語

本文基于網(wǎng)絡(luò)服務(wù)器的概念，提出兩種等價(jià)的may-testing前序，并證明了該測(cè)試前序具有前同余性本文的研究工作只是相關(guān)領(lǐng)域的一部分，針對(duì)不同問題還有許多值得研究的方向，如：本文只討論了進(jìn)程的有限行為，可以在此基礎(chǔ)上加入遞歸算子，用以刻畫無限的行為。該語義中含遞歸算子的最大前同余性，方程唯一解和最大解等等研究領(lǐng)域都未涉及。

參考文獻(xiàn)

[1]Nicola D,Hennessy M.Testing equivalences for processes[J]. ELSEVIER,1983,34(1-2):83-133.

[2]Hennessy M.Algebraic Theory ofProcesses[J].MIT Press, 1988,1-272.

[3]Castagna G,Gelbert N,Padovani L.A theory of contracts for web services [J].ACM Trans.,2009,31(5):1-61.

[4]Bernardi G,Hennessy M.Mutually testing processes[J].ACM, 2015,11(2:1):1-23.

[5]Milner R.Communication and Concurrency[J].Prentice Hall, 1989,1-260.

鄧鵬輝（1986－），男，江西鷹潭人，南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院研究生，研究領(lǐng)域：進(jìn)程代數(shù)、計(jì)算機(jī)科學(xué)中的邏輯學(xué)等。

張晉津（1981－），男，山西曲沃人，講師，博士，研究領(lǐng)域：形式化方式、計(jì)算機(jī)科學(xué)中的邏輯學(xué)等。

作者簡(jiǎn)介：

基金項(xiàng)目：國家自然科學(xué)基金（編號(hào)：11426136，60973045）；江蘇省高校自然科學(xué)基金（編號(hào)：13KJB520012）。