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

2.上海市高可信計算重點實驗室，上海 200062

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

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

2.上海市高可信計算重點實驗室，上海 200062

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

1 引言

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

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

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

2 預備知識

本章主要介紹概率進程代數(shù)（PCCS）的一些基本知識以及拓撲學中網(wǎng)的一些基本內(nèi)容。首先，介紹概率進程代數(shù)的語法和語義，這部分內(nèi)容主要來自文獻[12]。

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

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

若任意α∈Act，P至多有一個類型為α的概率導出，則稱P是確定性概率進程。所有確定性概率進程的集合記為DPr。

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

3 ε-極限互模擬

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

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

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

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

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

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

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

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

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

證明“?”顯然。

“?”假設 (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。一直假設N是增加的，即m1≤m2蘊含N(m1)≤N(m2)。

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

4 ε-互模擬極限

在本章中，為了描述軟件修改過程的收斂機制，提出ε-互模擬極限的定義。指出軟件的規(guī)范在概率互模擬下是其實現(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)的存儲能力是n，k是臨時存儲消息的數(shù)量。若緩沖器不滿，即k＜n，發(fā)送者可以一直以概率pk給Buffn(k)發(fā)送消息，當緩沖器不空時，即k＞0，接收者可以一直從緩沖器Buffn(k)上以概率1-pk接收到消息。下面證明在ε-互模擬下有界概率緩沖器的極限是無界概率緩沖器。定義無界概率緩沖器Buff∞(k)。令

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

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

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

5 結(jié)論

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

[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].山東大學學報：理學版，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

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

可信性；正確性；形式化；進程代數(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.

安徽省自然科學基金（No.1308085QF117）；安徽高校省級自然科學研究重點項目（No.KJ2011A248）；安徽高校省級自然科學研究一般項目（No.KJ2012Z347）；上海市高可信計算重點實驗室開放項目（No.07DZ22304201004）。

馬艷芳（1978—），女，博士，副教授，主要從事可信計算、形式化方法等方面的研究；陳亮（1977—），通訊作者，男，博士，副教授，主要從事數(shù)值計算等方面的研究。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