基于部分交互的軟件近似度量模型

馬艷芳，陳 亮

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

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

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

基于部分交互的軟件近似度量模型

馬艷芳1，2，陳 亮3

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

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

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

1 引言

隨著信息技術的發(fā)展，軟件系統(tǒng)變得越來越龐大和復雜，缺陷和漏洞難以避免，人們開始對軟件的質量進行研究。軟件可信性是評價軟件質量的重要標準。近年來，軟件的可信性模型越來越得到關注。如，陳儀香等，根據(jù)軟件的各種屬性，建立了基于屬性和權值的軟件可信性量化模型[1-3]。徐峰等建立了軟件服務協(xié)議的可信性評估模型[4]。隨著網(wǎng)絡的發(fā)展和服務意識的增強，計算模式逐漸轉向以網(wǎng)絡為中心和面向服務的體系結構，從而軟件的運行環(huán)境（包括網(wǎng)絡環(huán)境、物理環(huán)境）逐漸轉向開放、動態(tài)的環(huán)境[5-7]。軟件的運行環(huán)境對軟件的可信性有著很大影響。在實際應用中，由于環(huán)境資源的有限性等原因，有時軟件在環(huán)境下執(zhí)行到一定程度可能出現(xiàn)錯誤信息，從而軟件與環(huán)境未必成功交互。為了保證軟件在環(huán)境下繼續(xù)執(zhí)行，需要找出軟件與環(huán)境交互出錯的原因，而計算軟件與環(huán)境的交互程度可以幫助找到出錯的原因，進而為改進軟件與環(huán)境的交互提供一定的依據(jù)。

為了研究軟件與環(huán)境的交互，首先需要對環(huán)境進行描述。根據(jù)Milner提出的通信系統(tǒng)演算[8-9]（Communication and Compuation of Systems，CCS），從測試角度出發(fā)，環(huán)境可以用進程表示。如Larsen提出的參數(shù)化互模擬[10]，用一個標號轉換系統(tǒng)（labeled transition system）表示環(huán)境，明確地給出環(huán)境的變化過程。Smolka等也將環(huán)境表示成進程，其中包含一個表示成功的動作[11-13]。若軟件與環(huán)境并發(fā)執(zhí)行時能夠執(zhí)行到這個動作，則表明軟件與環(huán)境可以成功交互。而隨著網(wǎng)絡和服務的發(fā)展，軟件的運行環(huán)境逐漸開放，從而使得軟件對環(huán)境的要求越來越寬松，由此用進程表示環(huán)境不能適應計算模式的發(fā)展。更加一般地，環(huán)境可以用動作集合來表示。在動作之間沒有先后順序。如文獻[14-15]中所提到的進程失敗語義，從拒絕環(huán)境的角度來考慮進程之間的關系，此時的環(huán)境是一些動作構成的集合。當用集合表示環(huán)境時，集合中的元素由能夠引起軟件變化的信息或事件構成。從軟件方面上，可以是軟件的內部結構，如程序中聲明的全局變量。從硬件方面上，可以是軟件運行的硬件設備或網(wǎng)絡環(huán)境等。

為了描述當把環(huán)境作為一個集合考慮時進程與環(huán)境的交互，馬艷芳等建立了進程與環(huán)境交互的{0，1}-模型[16]。其研究交互的基本思想是：考察軟件的所有執(zhí)行路徑，當軟件選擇一條路徑執(zhí)行時，運行環(huán)境能提供其需要的所有信息，則這條路徑與環(huán)境交互的結果賦值為“1”，否則賦值為“0”。這種軟件與環(huán)境的交互是非常嚴格的交互。若軟件與環(huán)境成功交互，環(huán)境必須提供軟件所需要的所有信息。然而，在軟件的實際運行中，環(huán)境未必能夠提供軟件所需要的所有信息，軟件在環(huán)境下可能運行到某個地點而停滯，那么如何建立這種軟件與環(huán)境的交互模型，本文將以CCS模型為基礎，一般化{0，1}模型。

另一方面，為了測試不同軟件在環(huán)境下的性能，在實際應用中，有時需要對軟件進行比較。在一些特殊領域，例如航空航天領域，生物工程領域等，有時無法把軟件放在實際環(huán)境下運行，需要先建立一個實驗環(huán)境，在該環(huán)境下測試軟件的性能。而在該環(huán)境下開發(fā)出來的軟件，對其正確性等要求非?？量?，經(jīng)常利用不同的方法開發(fā)軟件，為了開發(fā)出更加適合于該實驗環(huán)境的軟件，需要對不同的開發(fā)版本進行比較。對軟件的比較已經(jīng)有了很多方法，如應明生等在CCS理論基礎上，將軟件抽象為進程，利用進程之間的強/弱互模擬關系，建立軟件之間近似程度的量化模型[17]。Smolka等為了說明帶有概率信息軟件之間的近似程度，提出了ε-互模擬等價，并建立了兩個概率進程之間近似程度的度量模型[18]。鄧玉欣等在概率CSP模型基礎上，根據(jù)概率進程執(zhí)行相同跡的概率和折扣因子建立了進程之間的度量。這個折扣因子反應了當軟件執(zhí)行相同跡的深度越大，他們之間越近似[19]。馬艷芳等基于ε-互模擬提出了軟件近似正確性模型[20]。但是考慮到環(huán)境對軟件的影響，對軟件進行比較時，需要考慮軟件與環(huán)境的交互能力。上述軟件之間的近似度量模型，沒有反映環(huán)境對軟件的影響。本文將以CCS模型為基礎，從軟件與環(huán)境的交互能力方面，建立軟件近似程度的量化模型。

2 預備知識

2.1 CCS基礎

令Δ表示動作名集合，用小寫字母a，b，c，…表示其中的元素。={aˉ|a∈Δ}表示補動作名的集合。規(guī)定表示動作a。用L=Δ∪表示標號集合，λ，μ，…表示其中的元素。τ表示不可觀測動作，。用Act表示所有動作的集合，Act=L∪{τ}，α，β，…表示其中的元素。令映射 f∶L→L，若滿足=，稱 f為重新標號函數(shù)。若令 f(τ)=τ，則 f可以延拓到集合Act上。同時，令X是L的子集。定義{∈X}，X∪{τ}。進一步，用表示所有進程變量構成的集合，X，Y，…表示其中的元素。R表示所有進程常量構成的集合，A，B，…表示其中的元素。I或J是索引集合。進程表達式的集合定義如下。

定義1（進程表達式）[8]進程表達式集合ε是包含，R和下列表達式的最小集合，其中E，Ei∈ε：

其中L?L，f是重新標號函數(shù)。

若一個進程表達式中不含變量，稱這個表達式是一個進程。用P 表示所有進程構成的集合，P，Q，…表示其中的元素。若A∈R，則A表示一個常量，其定義如下，其中PA∈P 。例如，。在通信系統(tǒng)演算中，常量提供了一種遞歸機制。

定義2（標號轉換系統(tǒng)）[8]三元組(ε，Act，{|α∈Act})表示Act集合上的標號轉換系統(tǒng)，(α∈Act)由下面規(guī)則給出。

2.2 進程的跡和完整跡語義

為了建立軟件與環(huán)境交互模型，馬艷芳等在文獻[16]中提出了完整跡語義。下面回顧一下完整跡語義的定義及性質。

定義3（可觀測完整跡）[16]令 P∈P 。如果存在P′∈P 使得P?σP′且init(P′)=?，其中σ∈L*，則稱σ是進程P的可觀測完整跡。用OCT(P)表示進程P的所有可觀測完整跡構成的集合。若OT(P)=OT(Q)且OCT(P)=OCT(Q)，則稱進程P和Q是可觀測完整跡等價，用P≈OCTQ表示，其中OP(T)表示進程的完整跡，具體定義參考文獻[15]。

可以根據(jù)進程的結構求出可觀測完整跡。

性質1[16]令P，Q∈P，l∈L，L?L，f∶Act→Act是集合Act上的雙射。則

若進程是一個遞歸進程，如 A=∑li.Pi.A。令 A= F(A)，則OCT(A)=OCT(Fn(0))，其中F是一個單調函數(shù)，而0是零進程。

根據(jù)通信系統(tǒng)演算，軟件可描述為進程，所以軟件的每個執(zhí)行路徑可以描述成一個可觀測完整跡。要研究軟件與環(huán)境的交互，首先要描述軟件的執(zhí)行路徑與環(huán)境之間的交互。令Env表示所有環(huán)境的集合，Env= {H|H?L}，所以Env?ρ(L)，其中ρ(L)表示L的冪集。

接下來給出進程的一個可觀測完整跡滿足環(huán)境的定義。設 P∈P，OCT(P)={σ1，σ2，…，σm}。設 H∈Env是一個環(huán)境，用Act(H)表示環(huán)境H所包含的所有動作構成的集合。任意σ∈OCT(P)，用 Act(σ)表示σ中包含的所有動作構成的集合，用|σ|表示σ中包含動作的個數(shù)，稱為σ的長度。

3 進程與環(huán)境交互[0，1]-模型

在{0，1}-模型中，軟件與環(huán)境的交互結果要么是“0”要么是“1”。這種交互沒辦法區(qū)分軟件與環(huán)境之間部分交互的情況：即軟件的執(zhí)行路徑中有些需要的信息，運行環(huán)境沒有提供，但是此時軟件可以在環(huán)境下運行一段時間，在找不到需要的信息時軟件運行出錯。換句話說，雖然執(zhí)行路徑中有一個動作未能在環(huán)境中找到對應的匹配，而此動作之前的動作都在環(huán)境中找到相應的匹配，此時軟件至少可以與環(huán)境交互到不匹配的動作之前。這時，軟件與環(huán)境能夠部分交互。用這條路徑能夠與環(huán)境部分交互的程度來定義這條路徑與環(huán)境交互的結果。由此可以看出，此時軟件的執(zhí)行路徑與環(huán)境的交互結果不再是“0”或“1”，而是[0，1]區(qū)間內的某個值，把這種交互結果在[0，1]區(qū)間的度量模型，稱為[0，1]-模型。接下來將具體介紹這個模型的定義及相關的性質。

令OCT(P)={σ1,σ2,…,σm}，H∈Env。設σ∈OCT(P)，且σ=y1y2…yt，記sσH=k使得任意1≤i≤k≤t，yi?H，但i=k+1，yk+1?H ，表示執(zhí)行路徑σ中第一個在環(huán)境中找不到匹配的動作，而前面的所有動作都能在環(huán)境找到相應的匹配。

定義5設P∈P，H∈Env，進程P與環(huán)境H交互的結果函數(shù) R[H0，1](P)∶OCT(P)→[0，1]定義如下，任意σ∈OCT(P)，

下面定義進程與環(huán)境交互的度量模型如下：

定義6設P∈P，H∈Env，進程P與環(huán)境H交互的度量定義為：

定義6考查了軟件的所有執(zhí)行路徑中能夠與環(huán)境進行交互的概率。

例1設有一個賣咖啡和牛奶的自動售貨機W。用CCS語言抽象為進程W=1元.(咖啡+牛奶).出口.W。

通過此表達式可知，若想從這臺售貨機上買一杯咖啡或者牛奶，先要投入1元，然后選擇“咖啡”或者“牛奶”按鈕，最后從出口取出。根據(jù)自動售貨機的功能，此表達式是一個遞歸進程。機器運行一次時，其可觀測完整跡有兩個，分別是σ1=1元 咖啡 出口和σ2= 1元 牛奶 出口。

在通信系統(tǒng)演算的實際應用中，對于具體的程序采用狀態(tài)轉換系統(tǒng)來表示。每個節(jié)點表示狀態(tài)，每條邊表示一個事件，即一個語句。執(zhí)行這個語句可以引起一個狀態(tài)到另一個狀態(tài)的轉換。在轉換過程中需要與環(huán)境進行交互才能完成狀態(tài)的改變。下面列舉一個用C語言編寫的程序來說明軟件與環(huán)境的交互。

例2用C語言編寫一個程序，該程序的功能是：先從鍵盤上輸入一個值，如果輸入的值小于3，將這個值加1，然后輸出結果，否則將這個值加2，然后輸出結果。某個程序員給出如下的程序，記為P1，狀態(tài)轉換圖如圖1所示。

圖1 P1的狀態(tài)轉換圖

為簡單起見，不考慮程序運行的硬件環(huán)境，該程序聲明的全局變量可以看出是其運行的環(huán)境，用動作集合表示為H={(x，int)，(y，int)，(z，int)}。這段程序的狀態(tài)轉換圖如圖1所示。當在Win-TC編譯器下運行時，其能夠實現(xiàn)要求的功能。在這個狀態(tài)轉換圖中，從初始狀態(tài)執(zhí)行 scanf（"\%d"，&x），對x=n賦值，獲得下一個狀態(tài)。此時，狀態(tài)從{(x=0，int)，(y=0，int)，(z=0，int)}變?yōu)閧(x=n，int)，(y，int)，(z，int)}，其中只有變量x的值發(fā)生了變化。在這個狀態(tài)轉換中，總蘊含著與環(huán)境進行交互。這種交互主要是將執(zhí)行語句所獲得的x，y，z的值與環(huán)境進行比較。如果是環(huán)境允許的，可以正確執(zhí)行，否則不能得到正確的結果。為了更加方便地描述交互，在計算完整跡時，只考慮變量值改變的過程。在左邊的完整跡中，其變化次序為：先是變量x的值發(fā)生變化，然后執(zhí)行“z=x+1”使得變量z的值發(fā)生變化，最后執(zhí)行printf（"%d"，z），使得變量z的值變化，因此變化次序是{(x，int)，(z，int)，(z，int)}。同理可得，右邊的完整跡中變化次序為{(x，int)，(y，int)，(y，int)}。而這個執(zhí)行路徑中，變量的變化都是環(huán)境允許的，從而根據(jù)定義5，對這個執(zhí)行路徑賦值都是“1”，再根據(jù)定義6，可得，p[0，1](P1，H)=1。此結果表明這段程序可以與環(huán)境成功交互。

有些程序員也可能給出下面的程序，用 P2表示，這個程序也能實現(xiàn)要求的功能。其狀態(tài)轉換圖如圖2所示。

圖2 P2的狀態(tài)轉換圖

程序P2與P1的不同之處在于語句“y=x+2.2”將變量y賦值為一個浮點型數(shù)據(jù)。由于C語言能夠進行類型轉換，可以將y的類型強制轉換為整型。進而程序P2也可以實現(xiàn)要求的功能，環(huán)境是H={(x，int)，(y，int)，(z，int)}，可以求出 p[0，1](P2，H)=1。

一些程序員也可能給出下面的程序，用P3來表示，其沒有實現(xiàn)要求的功能，標號轉換系統(tǒng)如圖3所示。

圖3 P3的狀態(tài)轉換圖

在左邊的完整跡中，變量的變化次序是{(x，int)，(z，int)，(z，int)}，賦值為1。而右邊的完整跡中，當執(zhí)行printf（"%f"，y）時，變量 y類型的變化不是環(huán)境運行的，其變化次序{(x，int)，(y，int)，(y，float)}，根據(jù)定義5，右邊的完整跡賦值為。進一步由定義6，可以計算得到這段程序與環(huán)境的交互度量為也就是說此程序沒有和環(huán)境進行成功交互，其成功交互的概率是。

4 基于環(huán)境和[0，1]-模型的進程近似度量

在實際應用中，經(jīng)常會遇到在同一環(huán)境下對不同的軟件進行比較。根據(jù)CCS語言，軟件可以抽象成進程。特別對實時系統(tǒng)，已經(jīng)存在相應的建模和驗證工具，如UPPAAL。其可以用來對被轉換時間自動機網(wǎng)絡模型的實時系統(tǒng)進行建模、校驗和驗證。它是由瑞典Uppsala大學的信息技術學院和丹麥Aalborg大學的計算科學學院聯(lián)合開發(fā)的。而對于一般的軟件還沒有具體的工具對其進行建模。但是對于規(guī)模較小的軟件，根據(jù)CCS模型，可以用標號轉化系統(tǒng)對其建立狀態(tài)轉換圖，從而抽象出它的可觀測完整跡。例如例2中的程序段，可以抽象成狀態(tài)轉換圖。由于軟件的運行依賴于環(huán)境，在對軟件進行比較時，需要考慮環(huán)境的因素。而環(huán)境對軟件的影響主要體現(xiàn)在軟件與環(huán)境的交互，所以可以從軟件與環(huán)境的交互能力方面來評價軟件的好壞。那么如何來評價這些軟件在與環(huán)境交互方面的能力呢?由于[0，1]-模型不同于{0，1}-模型，所以在本章中將建立在[0，1]-模型和給定環(huán)境下兩個軟件之間的近似度量模型以及在特定環(huán)境下評價軟件好壞的標準。首先建立基于環(huán)境和[0，1]-模型的軟件近似度量。

例3假設某兩個程序用CCS語言抽象表示為進程P=a.b.0+a.c.0+a.0，Q=a.b.0+a.c.0。執(zhí)行環(huán)境有E= {a，b，d}。則根據(jù)定義5可知：

性質4說明當兩個軟件是完整跡等價時，它們關于環(huán)境H近似度為1。由此可以根據(jù)完整跡等價算法來計算軟件與環(huán)境之間的近似度量。從定義7可知，對于一個給定的環(huán)境，當兩個軟件之間的差距越小，它們與給定環(huán)境在[0，1]-模型下的交互能力差距就越小。而當軟件的執(zhí)行路徑較多時，將影響軟件的運行速度，從而降低了軟件與環(huán)境交互的能力。由此，可以利用軟件與環(huán)境成功交互的概率來評價軟件與環(huán)境交互能力的好壞。接下來根據(jù)軟件與環(huán)境成功交互的概率來比較軟件的好壞。

這個定義是說，若軟件Q與環(huán)境H在模型[0，1]上的交互度量值比P與環(huán)境H交互度量值大，那么在環(huán)境H下軟件Q比P好。

例4設有一個賣咖啡和牛奶的自動售貨機W如例1所示。有另一臺只賣咖啡的自動售貨機P，P=1元.咖啡.出口.P。若某個顧客想買咖啡，用集合H={1元，咖啡，出口}表示，則可知(W，H)=，而(P，H)=1，故(W，H)≤(P，H)，所以W?。說明對于環(huán)境H來說，P比W要好，因為其不需要做任何選擇就可以買到想好的咖啡。

例5對例2中的三段程序進行比較，在聲明了全局變量H={(x，int)，(y，int)，(z，int)}下，可以看出(P1,H)= 1=(P2，H)，由此程序 P1和 P2一樣好。但是由于(P3，H)=，所以P3不如P1和P2好，因為其沒有實現(xiàn)所要求的功能。

性質6表示在[0，1]-模型和給定環(huán)境H下，與零進程等價的軟件都是最差的軟件，即什么都沒做的軟件是最差的。

5 結論

在本文中主要以CCS語言為基礎，建立了軟件與環(huán)境的部分交互模型，同時，從與環(huán)境交互能力方面，討論了軟件的近似程度，以及比較軟件好壞的標準，證明一些代數(shù)性質。

而在軟件的分析和設計過程中，模塊化和層次化方法是經(jīng)常使用的方法。而在討論軟件與環(huán)境的部分交互時，是否也能采用模塊化的方法來獲得軟件與環(huán)境的交互度量？在接下來的工作中，將對此問題進行研究。

[1]Chen Yixiang，Zhang Min，Zhu Hong，et al.Average transitive trustworthy degrees for trustworthy[C]//LNCS：Rough Sets and Knowledge Technology，2009，5589.

[2]Chen Yixiang，Bu Tianming，Zhang Min，et al.Max-minimum algorithm for turst transitivity in trustworthy networks[C]//Proceedings of the 2009 IEEE/WIC/ACM International Joint Conference on Web Intelligence and Intelligent Agent Technology，2009：62-64.

[3]Tao Hongwei，Chen Yixiang.A metric model for trustworthiness of software[C]//The Proceedings of ACM International Conferences on Web Intelligence and Intelligent Agent Technology，2009：69-71.

[4]Xu F，Zheng W，Cao C.Design of a trust valuation model in software service coordination[J].Journal of Software，2003，14（6）：1043-1051.

[5]劉克，單志廣，王戟，等.可信軟件基礎研究重大研究計劃綜述[J].科學進展與展望，2008（3）：145-151.

[6]沈昌祥，張煥國，王懷民，等.可信計算的研究與發(fā)展[J].中國科學 F輯：信息科學，2010，40（2）：139-166.

[7]鄭志明，馬世龍，李未，等.軟件可信復雜性及其動力學統(tǒng)計分析[J].中國科學 F輯：信息科學，2009，39（10）：1050-1054.

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

[9]Milner R.Communicating and mobile systems：the π-calculus[M].Cambridge：Cambridge University Press，1999.

[10]Larsen K G.Context-dependent bisimulation between process[D].Edinburgh：Aalborg University Centre Strandvejen，1986.

[11]Yuen S，Cleaveland R，Dayar Z，et al.Fully abstract characterizations of testing preorders for probabilisitc processes[C]//The Proceedings of CONCUR’94.Berlin：Springer，1994，836：497-512.

[12]Deng Yunxin，van Glabbeek R，Hennessy M，et al.Remarks on testing probabilistic processes[J].Electronic Notes in Theoretical Computer Science，2007，172：359-397.

[13]Ling Cheung，Stoelinga M，Vaandrager F.A testing scenario for probabilistic processes[J].Journal of the ACM，2007，54（6）：1-44.

[14]He J F，Hoare T.Equating bisimulation with refinement[R]. UNU-IIST，Macau，China，2003.

[15]van Glabbeek R J.The linear time-branching time spectrum I*[EB/OL].[2014-01-03].http：//theory.stanford.edu/rvg.

[16]馬艷芳，陳亮.基于交互的環(huán)境近似度量模型[J].山東大學學報：理學版，2013，48（7）：33-38.

[17]Ying M S.Bisimulation indexes and their applications[J]. Theoretical Computer Science，2002，275（1/2）：1-68.

[18]Giacalone A，Jou C，Smolka S A.Probabilistic in processes：an algebraic/operational framework，Technical Report No.88/20[R].Department of Computer Science，SUNY at Stony Brook，1988.

[19]Deng Y X，Glabbeek R，Hennessy M，et al.Testing finitary probabilistic processes[C]//Lecture Notes in Computer Science，2009，5710：274-288.

[20]馬艷芳，陳亮.基于ε-互模擬的軟件近似正確性模型[J].計算機工程與應用，2013，49（11）：15-19.

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 Mathematics Science,Huaibei Normal University,Huaibei,Anhui 235000,China

The dependence of the software on its environment mainly comes from the interaction.In the real application, sometimes,the interaction may not be successful.The interaction degree will have an effect on the ability of software.In order to test the property of software on the environment,it is necessary to compare the interaction ability of software with environment.In this paper,based on process algebra,the approximate measure model of software will be researched using complete trace semantics.The partial interaction will be formalized using the completed trace semantics.Some examples will be stated.The quantitative model which describes the approximate degree between software will be proposed. Some algebraic properties are proved.The criterion which evaluates the interaction ability with environment will be given.

partial interaction;measure;formalization;process algebra

軟件對環(huán)境的依賴性主要體現(xiàn)在軟件與環(huán)境的交互。在實際中，有時軟件與環(huán)境未必成功交互。其交互程度對軟件的性能有著很大的影響。為測試不同軟件在環(huán)境下的性能，需要對軟件與環(huán)境的交互能力進行比較。在進程代數(shù)理論基礎上，利用完整跡語義，建立軟件近似程度的量化模型。形式化描述軟件與環(huán)境的部分交互。列舉一些例子對模型進行說明。建立軟件近似程度的量化模型，證明一些代數(shù)性質。進一步，建立評價軟件在與環(huán)境交互方面好壞的標準。

部分交互；度量；形式化；進程代數(shù)

A

TP301；O159

10.3778/j.issn.1002-8331.1403-0401

MA Yanfang,CHEN Liang.Approximate measure model of software based on partial interaction.Computer Engineering and Applications,2014,50（24）：32-37.

國家自然科學基金（No.61300048）；安徽省自然科學基金（No.1308085QF117）；安徽省高等學校省級自然科學研究重點項目（No.KJ2011A248，No.KJ2012Z347）；上海市高可信重點實驗室開放課題項目（No.07DZ22304201004）。

馬艷芳，女，博士，副教授，主要從事進程演算、程序語義、軟件可信性等方面的研究；陳亮，通訊作者，男，博士，副教授，主要從事數(shù)值計算、矩陣計算、算法等方面的研究。E-mail：clmyf2@163.com

2014-03-26

2014-06-25

1002-8331（2014）24-0032-06

CNKI網(wǎng)絡優(yōu)先出版：2014-09-04，http∶//www.cnki.net/kcms/doi/10.3778/j.issn.1002-8331.1403-0401.html