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

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

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

3.淮北師范大學 數學科學學院，安徽 淮北 235000

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

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

3.淮北師范大學 數學科學學院，安徽 淮北 235000

1 引言

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

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

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

2 預備知識

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

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

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

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

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

3 ε-極限互模擬

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

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

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

例3.1令規范P=0.4a.0+0.6b.0，獲得的一系列實現為：

如，第一次獲得的實現：

第二次修改獲得的實現：

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

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

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

證明“?”顯然。

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

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

4 ε-互模擬極限

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

定義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是臨時存儲消息的數量。若緩沖器不滿，即k＜n，發送者可以一直以概率pk給Buffn(k)發送消息，當緩沖器不空時，即k＞0，接收者可以一直從緩沖器Buffn(k)上以概率1-pk接收到消息。下面證明在ε-互模擬下有界概率緩沖器的極限是無界概率緩沖器。定義無界概率緩沖器Buff∞(k)。令

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

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

命題4.4給出了ε-互模擬極限的唯一性。也表明了在實際開發中開發實現必須依據一個規范，不能依據不同的規范開發同一個軟件。

5 結論

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

[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]馬艷芳，張敏，陳儀香.基于環境的軟件正確性形式化描述[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

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

可信性；正確性；形式化；進程代數

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—），通訊作者，男，博士，副教授，主要從事數值計算等方面的研究。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