基于ε-互模擬的軟件近似正確性模型

1.淮北師范大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，安徽 淮北 235000

2.上海市高可信計(jì)算重點(diǎn)實(shí)驗(yàn)室，上海 200062

3.淮北師范大學(xué) 數(shù)學(xué)科學(xué)學(xué)院，安徽 淮北 235000

1.淮北師范大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，安徽 淮北 235000

2.上海市高可信計(jì)算重點(diǎn)實(shí)驗(yàn)室，上海 200062

3.淮北師范大學(xué) 數(shù)學(xué)科學(xué)學(xué)院，安徽 淮北 235000

1 引言

軟件正確性是軟件工程的重要內(nèi)容，是軟件可信性的重要屬性。對(duì)軟件正確性進(jìn)行研究可以為提高軟件質(zhì)量提供保證。軟件正確性主要表現(xiàn)為軟件的執(zhí)行能否符合人們的預(yù)期。一般地，軟件的執(zhí)行抽象為軟件的實(shí)現(xiàn)，人們的預(yù)期抽象為軟件的規(guī)范。進(jìn)而軟件正確性表示為軟件的實(shí)現(xiàn)與規(guī)范之間的關(guān)系。這種關(guān)系借助于進(jìn)程代數(shù)中的各種理論來(lái)描述：如ACP[1]，Communicating Sequential Process（CSP）[2]，Calculus of Communicating Systems（CCS）[3]等。在R.Milner提出的CCS語(yǔ)言（也稱為通信系統(tǒng)演算）中，各種進(jìn)程之間的等價(jià)關(guān)系是其主要內(nèi)容，如強(qiáng)互模擬和弱互模擬、跡等價(jià)及觀測(cè)等價(jià)等。把規(guī)范（specification）和實(shí)現(xiàn)（implementation）抽象為兩個(gè)進(jìn)程，如果軟件規(guī)范和實(shí)現(xiàn)之間存在某種等價(jià)關(guān)系，則軟件是正確的。在文獻(xiàn)[4]中，應(yīng)明生給出了這些等價(jià)關(guān)系的無(wú)限演化過(guò)程，定義了強(qiáng)互模擬極限、弱互模擬極限和跡極限等，從而建立了CCS語(yǔ)言的極限理論。為了描述在一定環(huán)境下軟件實(shí)現(xiàn)的無(wú)限演化，在文獻(xiàn)[5-6]中，作者基于ε-參數(shù)化互模擬，提出了ε-參數(shù)化極限互模擬和參數(shù)化互模擬極限，建立了ε-參數(shù)化互模擬的極限理論和拓?fù)淅碚摗榱硕攘吭诰芙^環(huán)境下軟件實(shí)現(xiàn)與規(guī)范之間的近似程度，在文獻(xiàn)[7]中作者建立了三分之二互模擬的度量理論。

而在一些復(fù)雜的軟件系統(tǒng)中，存在一定的概率現(xiàn)象，為了描述這種復(fù)雜系統(tǒng)的概率信息，已經(jīng)出現(xiàn)了很多概率進(jìn)程代數(shù)模型[8-10]。像CCS一樣，每個(gè)模型都有概率互模擬等價(jià)[11]。如 A.Giacalone，C.C.Jou 和 S.A.Smolka提出的 ε-互模擬等價(jià)，其以生長(zhǎng)概率模型（generative probabilistic model）[12]為基礎(chǔ)描述了進(jìn)程之間的幾乎處處相等。例如，一個(gè)軟件的規(guī)范用一個(gè)概率進(jìn)程表示為P=0.4a.0+0.6b.0，其實(shí)現(xiàn)用概率進(jìn)程表示為Q=0.400 1a.0+0.599 9b.0。盡管實(shí)現(xiàn)與規(guī)范直接沒(méi)有完全匹配，但是執(zhí)行相同動(dòng)作的概率是非常接近的。事實(shí)上，在概率情況下進(jìn)程之間的幾乎處處相等比進(jìn)程的等價(jià)更加有用，因?yàn)榈葍r(jià)的要求太嚴(yán)格了，在實(shí)際中很難達(dá)到。在實(shí)際應(yīng)用中，如果規(guī)范中包含一些概率信息，而在開(kāi)發(fā)實(shí)現(xiàn)過(guò)程中，若適當(dāng)?shù)恼`差是被允許的，則可以選擇ε-互模擬來(lái)驗(yàn)證軟件實(shí)現(xiàn)與其規(guī)范的關(guān)系。一般地，初次獲得的實(shí)現(xiàn)未必能夠符合要求，進(jìn)而需要不斷地修改實(shí)現(xiàn)，使其越來(lái)越符合要求。由此得到一個(gè)實(shí)現(xiàn)的進(jìn)化序列。但是，當(dāng)開(kāi)發(fā)過(guò)程由幾個(gè)團(tuán)隊(duì)共同完成，在同一時(shí)間，幾個(gè)團(tuán)隊(duì)都對(duì)實(shí)現(xiàn)進(jìn)行了修改，由此得到的實(shí)現(xiàn)改進(jìn)過(guò)程不再是一個(gè)序列，而是一個(gè)偏序，為了描述這種情況，可以利用拓?fù)渲械木W(wǎng)來(lái)描述進(jìn)程。本文利用ε-互模擬，試圖建立實(shí)現(xiàn)進(jìn)化過(guò)程的收斂機(jī)制。對(duì)實(shí)現(xiàn)的進(jìn)化過(guò)程進(jìn)行抽象刻畫(huà)，可以為實(shí)際的軟件開(kāi)發(fā)提供指導(dǎo)，幫助軟件開(kāi)發(fā)者檢查開(kāi)發(fā)過(guò)程是否朝著正確的方向發(fā)展。同時(shí)在理論上進(jìn)一步豐富了軟件的形式化理論。

在本文中引入ε-極限互模擬和ε-互模擬極限，其刻畫(huà)了軟件的規(guī)范是其實(shí)現(xiàn)的極限。給出ε-極限互模擬的例子，證明ε-互模擬極限的唯一性，ε-互模擬極限與ε-互模擬的相容性等性質(zhì)。

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

本章主要介紹概率進(jìn)程代數(shù)（PCCS）的一些基本知識(shí)以及拓?fù)鋵W(xué)中網(wǎng)的一些基本內(nèi)容。首先，介紹概率進(jìn)程代數(shù)的語(yǔ)法和語(yǔ)義，這部分內(nèi)容主要來(lái)自文獻(xiàn)[12]。

定義2.1[12]概率進(jìn)程表達(dá)式集合ε是包含0，X和下面表達(dá)式的最小集合：

定義2.2[12]PCCS的操作語(yǔ)義是以概率導(dǎo)出為基礎(chǔ)的，由一組推理規(guī)則構(gòu)成，其形式與Plotkin的相同。具體規(guī)則如下：

若任意α∈Act，P至多有一個(gè)類型為α的概率導(dǎo)出，則稱P是確定性概率進(jìn)程。所有確定性概率進(jìn)程的集合記為DPr。

定義2.3（ε-互模擬）[12]令 ε∈[0，1)，在集合 DPr上的一個(gè)二元關(guān)系 Rε?DPr×DPr稱為ε-互模擬，若滿足：如果(P，Q)∈Rε蘊(yùn)含任意 α∈Act。

3 ε-極限互模擬

軟件在設(shè)計(jì)過(guò)程中需要不斷地對(duì)其進(jìn)行修改，在修改過(guò)程中得到一系列實(shí)現(xiàn)版本，每個(gè)版本與規(guī)范之間都可以用ε-互模擬來(lái)刻畫(huà)。但是，修改過(guò)程是一個(gè)無(wú)限過(guò)程，其最終目的是規(guī)范。本章定義ε-極限互模擬，用來(lái)刻畫(huà)軟件實(shí)現(xiàn)的修改過(guò)程中得到這些實(shí)現(xiàn)與規(guī)范之間的關(guān)系，并給出幾個(gè)ε-極限互模擬的例子。

定義3.1 令ε∈[0，1)。DPr和DPrN上的二元關(guān)系Sε? DPr×DPrN被稱為 ε-極限互模擬，若滿足任意α∈Act，(P，{Qn:n ∈ D})∈ Sε。

從定義上可以看出，ε-極限互模擬是ε-互模擬的動(dòng)態(tài)演化形式。若確定性概率進(jìn)程P和確定性概率進(jìn)程網(wǎng){Qn:n∈D}是ε-互模擬相關(guān)，則P是{Qn:n∈D}極限行為。語(yǔ)句（1）表示，若P以概率 p執(zhí)行動(dòng)作α，則{Qn:n∈D}最終能執(zhí)行α且其執(zhí)行α的概率與 p最多相差ε。語(yǔ)句（2）是說(shuō)若{Qn:n∈D}經(jīng)常以概率qn執(zhí)行動(dòng)作α，則P也能執(zhí)行該動(dòng)作且執(zhí)行α的概率與qn的距離不超過(guò)ε。

例3.1令規(guī)范P=0.4a.0+0.6b.0，獲得的一系列實(shí)現(xiàn)為：

如，第一次獲得的實(shí)現(xiàn)：

第二次修改獲得的實(shí)現(xiàn)：

已知在確定概率進(jìn)程上的恒等關(guān)系 Iden是ε-互模擬，下面將此關(guān)系延拓到ε-極限互模擬上。這個(gè)關(guān)系也說(shuō)明了在實(shí)際開(kāi)發(fā)軟件時(shí)，若初次開(kāi)發(fā)獲得的實(shí)現(xiàn)與規(guī)范之間符合要求，則這樣的實(shí)現(xiàn)不需要修改。令

命題3.1 令 ε∈[0，1)，Sε?DPr×DPrN，則 IlimSε是 ε-極限互模擬。

下面的例子說(shuō)明在軟件開(kāi)發(fā)時(shí)，若獲得的一系列實(shí)現(xiàn)與規(guī)范之間滿足要求，則在這些實(shí)現(xiàn)序中必然有一部分滿足要求。

證明“?”顯然。

“?”假設(shè) (P，{Rm:m∈C})∈sub(Sε)，則存在 (P，{Qn: n∈D})∈Sε使得{Rm:m∈C}是{Qn:n∈D}的子網(wǎng)，即存在映射 N:C→D使得(C，N)是 D的共尾且，任意m∈C，Rm=QNm。一直假設(shè)N是增加的，即m1≤m2蘊(yùn)含N(m1)≤N(m2)。

命題3.3 如果Sε是 ε-極限互模擬，則 sub(Sε)也是ε-極限互模擬。

4 ε-互模擬極限

在本章中，為了描述軟件修改過(guò)程的收斂機(jī)制，提出ε-互模擬極限的定義。指出軟件的規(guī)范在概率互模擬下是其實(shí)現(xiàn)的極限形式。

定義4.1（1）令ε∈[0，1)，P∈DPr，{Qn:n∈D}∈DPrN。如果存在 ε-極限互模擬 Sε使得 (P，{Qn:n∈D})∈Sε，則稱

則由命題3.4可知：

是最大的ε-極限互模擬。

例4.1考慮帶有概率信息的緩沖器，Buffn(k)，n∈ω，k≤n。令

緩沖器Buffn(k)的存儲(chǔ)能力是n，k是臨時(shí)存儲(chǔ)消息的數(shù)量。若緩沖器不滿，即k＜n，發(fā)送者可以一直以概率pk給Buffn(k)發(fā)送消息，當(dāng)緩沖器不空時(shí)，即k＞0，接收者可以一直從緩沖器Buffn(k)上以概率1-pk接收到消息。下面證明在ε-互模擬下有界概率緩沖器的極限是無(wú)界概率緩沖器。定義無(wú)界概率緩沖器Buff∞(k)。令

這個(gè)例子是說(shuō)有界概率緩沖器的極限是無(wú)界概率緩沖器。 Buffn(k)和 Buff∞(k)之間的不同在于 Buff∞(k)是無(wú)限的，因此發(fā)送者不需要考慮緩沖器中已有消息的數(shù)量，可以一直發(fā)送消息。

命題4.3表明了ε-互模擬極限與ε-互模的相容性。在實(shí)際中，若兩個(gè)團(tuán)隊(duì)開(kāi)發(fā)時(shí)獲得的實(shí)現(xiàn)非常相似，則他們開(kāi)發(fā)時(shí)所依據(jù)的規(guī)范是同一個(gè)規(guī)范。

命題4.4給出了ε-互模擬極限的唯一性。也表明了在實(shí)際開(kāi)發(fā)中開(kāi)發(fā)實(shí)現(xiàn)必須依據(jù)一個(gè)規(guī)范，不能依據(jù)不同的規(guī)范開(kāi)發(fā)同一個(gè)軟件。

5 結(jié)論

在本文中主要以PCCS語(yǔ)言為基礎(chǔ)，討論了進(jìn)程的ε-互模擬的極限行為，定義了ε-極限互模擬，并在此基礎(chǔ)上建立了ε-互模擬極限。同時(shí)證明了一些性質(zhì)。為了更好地從數(shù)學(xué)角度理解和分析進(jìn)程的動(dòng)態(tài)特性，在接下來(lái)的研究中將給出ε-互模擬的拓?fù)淅碚摗?/p>

[1]Baeten J C，Weijland W P.Process algebra[M].Cambridge：Cambridge University Press，1990.

[2]Hoare C A R.Communicating sequential processes[M].New York：Prentice Hall，1985.

[3]Milner R.Communication and concurrency[M].New York：Prentice Hall，1989.

[4]Ying M S.Topology in process calculus：approximate correctness and infinite evolution of concurrency programs[M].Berlin：Springer-Verlag，2001.

[5]Ma Y F，Zhang M.Topological construction of parameterized bisimulation limit[C]//Electronic Notes in Theoretical Computer Science.Amsterdam：Elsevier Science，2009，257：57-70.

[6]Ma Y F，Zhang M.Parameterized bisimulation infinite evolution mechanism[C]//3rd IEEE International Symposium on Theoretical Aspects of Software Engineering，Tianjin，China.Los Alamitos，CA：IEEE Computer Society，2009：299-300.

[7]馬艷芳，張敏，陳儀香.基于環(huán)境的軟件正確性形式化描述[J].山東大學(xué)學(xué)報(bào)：理學(xué)版，2011，46（9）：22-27.

[8]Frank B，James W.Approximating and computing behavioural distances in probabilistic transition systems[J].Theoretical Computer Science，2006，360（1/3）：373-385.

[9]Song L，Deng Y X，Cai X J.Towards automatic measurement of probabilistic processes[C]//7th International Conference on Quality Software，Portland.Washington：IEEE Computer Society， 2009：50-59.

[10]Deng Y X，Glabbeek R，Hennessy M，et al.Testing finitary probabilistic processes[C]//Lecture Notes in Computer Science 5710：The 20th International Conference on Concurrency Theory，Bologna，Italy.Berlin：Springer-Verlag，2009：274-288.

[11]Larsen K G，Skou A.Bisimulation through probabilistic testing[J]. Information and Computation，1991，94（1）：1-28.

[12]Giacalone A，Jou C C，Smolka S A.Algebraic reasoning for probabilistic concurrenct systems[C]//Lecture Notes in Computer Science 494：IFIP TC2 Working Conference on Programming Concepts and Methods，Tiberias.Berlin：Springer-Verlag，1990：443-458.

[13]Milner R.Calculi for synchrony and asynchrony[J].Theoretical Computer Science，1983，25：267-310.

[14]Kelly J L.General topology[M].Germany：Springer-Verlag，1975.

[15]Engelking R.General topology[M].Poland：Polish Science，1977.

基于ε-互模擬的軟件近似正確性模型

馬艷芳1，2，陳 亮3

MAYanfang1，2,CHEN Liang3

1.School of Computer Science and Technology,Huaibei Normal University,Huaibei,Anhui 235000,China
2.Shanghai Key Laboratory of Trustworthy Computing,Shanghai 200062,China
3.School of Mathematical Sciences,Huaibei Normal University,Huaibei,Anhui 235000,China

The correctness of software is a key attribution for trustworthiness of software.In the real development and design, the software is modified constantly in order to get correctness,and the software is correct more and more.This paper focuses on the dynamic characterization of correctness.Based on ε-bisimulation of probabilistic process algebra,ε-limit bisimulation is defined which reflects the relation between implementation and its specification,and some specialε-limit bisimulations are showed.ε-bisimulation limit is presented,which states that specification is the limit of implementations.Some important properties are proved.

trustworthiness;correctness;formalization;process algebra

軟件正確性是軟件可信性的重要屬性。在實(shí)際軟件開(kāi)發(fā)和設(shè)計(jì)中，需要不斷地對(duì)軟件進(jìn)行修改，從而軟件越來(lái)越正確。為了討論軟件的動(dòng)態(tài)近似正確性，基于概率進(jìn)程代數(shù)的ε-互模擬，建立軟件越來(lái)越正確的形式化描述。定義ε-極限互模擬，用來(lái)反應(yīng)軟件實(shí)現(xiàn)與規(guī)范之間的關(guān)系，給出一些特殊的ε-極限互模擬。提出ε-互模擬極限，用其刻畫(huà)規(guī)范是軟件實(shí)現(xiàn)的極限形式，同時(shí)證明ε-互模擬極限的一些性質(zhì)。

可信性；正確性；形式化；進(jìn)程代數(shù)

A

O159；TP301

10.3778/j.issn.1002-8331.1211-0125

MA Yanfang,CHEN Liang.Model of software approximate correctness underε-bisimulation.Computer Engineering and Applications,2013,49（11）：15-19.

安徽省自然科學(xué)基金（No.1308085QF117）；安徽高校省級(jí)自然科學(xué)研究重點(diǎn)項(xiàng)目（No.KJ2011A248）；安徽高校省級(jí)自然科學(xué)研究一般項(xiàng)目（No.KJ2012Z347）；上海市高可信計(jì)算重點(diǎn)實(shí)驗(yàn)室開(kāi)放項(xiàng)目（No.07DZ22304201004）。

馬艷芳（1978—），女，博士，副教授，主要從事可信計(jì)算、形式化方法等方面的研究；陳亮（1977—），通訊作者，男，博士，副教授，主要從事數(shù)值計(jì)算等方面的研究。E-mail：clmyf2@163.com

2012-11-12

2013-03-04

1002-8331（2013）11-0015-05

CNKI出版日期：2013-03-15 http://www.cnki.net/kcms/detail/11.2127.TP.20130315.1146.001.html