馬艷芳

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

基于軟件的環(huán)境量化模型

馬艷芳

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

在一些特殊領(lǐng)域中需要建立一定的實(shí)驗(yàn)環(huán)境對(duì)軟件性能進(jìn)行測(cè)試,因此實(shí)驗(yàn)環(huán)境與實(shí)際環(huán)境之間的近似程度對(duì)軟件的性能起到關(guān)鍵作用。為建立環(huán)境之間的近似度量,在進(jìn)程代數(shù)理論基礎(chǔ)上,根據(jù)軟件與環(huán)境的交互程度,利用拓?fù)涠攘亢驼撚蚶碚撝械钠蜿P(guān)系,建立實(shí)驗(yàn)環(huán)境之間近似程度的量化模型。根據(jù)軟件與環(huán)境之間的部分交互,建立實(shí)驗(yàn)環(huán)境之間近似程度的度量模型。通過(guò)實(shí)例對(duì)度量模型進(jìn)行說(shuō)明,并證明度量模型的代數(shù)性質(zhì)。

:交互;環(huán)境;進(jìn)程代數(shù);度量;論域理論

1 概述

網(wǎng)絡(luò)的發(fā)展使得軟件的運(yùn)行環(huán)境逐漸轉(zhuǎn)向了開(kāi)放動(dòng)態(tài)的環(huán)境,從而環(huán)境對(duì)軟件可信性起到越來(lái)越重要的作用[1-3]。在一些特殊領(lǐng)域中,如生物工程領(lǐng)域、航空航天領(lǐng)域以及一些生命攸關(guān)的領(lǐng)域中,有時(shí)需要構(gòu)造一定的實(shí)驗(yàn)環(huán)境,將軟件放在實(shí)驗(yàn)環(huán)境下運(yùn)行,來(lái)評(píng)估軟件的性能。由此,實(shí)驗(yàn)環(huán)境與實(shí)際環(huán)境之間的近似程度對(duì)軟件的性能起到關(guān)鍵作用。因此,如何度量軟件運(yùn)行環(huán)境的相似性是需要解決的問(wèn)題。

軟件在環(huán)境下運(yùn)行,主要體現(xiàn)在與環(huán)境的交互。軟件與環(huán)境的基本交互主要有2種,如文獻(xiàn)[4]提出的參數(shù)化互模擬,用一個(gè)標(biāo)號(hào)轉(zhuǎn)換系統(tǒng)描述環(huán)境,清晰地給出了環(huán)境的變化過(guò)程。將軟件抽象為進(jìn)程,軟件與環(huán)境的交互體現(xiàn)在環(huán)境所能允許的變化,軟件也能允許,從而從接收角度描述了交互。文獻(xiàn)[5-6]為了建立基于環(huán)境的軟件正確性,提出了參數(shù)化互模擬極限,建立了參數(shù)化互模擬的無(wú)限演化理論和拓?fù)淅碚?。文獻(xiàn)[7]在測(cè)試語(yǔ)義的基礎(chǔ)上,用一個(gè)包含表示成功動(dòng)作的進(jìn)程表示環(huán)境[8],軟件與環(huán)境能否成功交互體現(xiàn)在軟件與環(huán)境并發(fā)執(zhí)行時(shí)能否執(zhí)行到表示成功的動(dòng)作。利用進(jìn)程來(lái)描述環(huán)境是一種非常嚴(yán)格的描述方式,當(dāng)環(huán)境發(fā)生一些微小變化時(shí),對(duì)軟件與環(huán)境的交互將會(huì)產(chǎn)生很大的影響。

文獻(xiàn)[9-10]提出了進(jìn)程失敗語(yǔ)義,其中用動(dòng)作集合來(lái)描述環(huán)境。由于集合中的元素是無(wú)序的,因此把環(huán)境表示為動(dòng)作的集合是一種很寬松的環(huán)境刻畫。如在線服務(wù)系統(tǒng)中,每個(gè)客戶都可以看作是系統(tǒng)運(yùn)行的環(huán)境。但是當(dāng)用集合表示環(huán)境時(shí),如何來(lái)描述和度量軟件與環(huán)境的交互以及環(huán)境之間的度量,文獻(xiàn)[11]在完整跡語(yǔ)義的基礎(chǔ)上,提出了可觀測(cè)完整跡語(yǔ)義,并在此基礎(chǔ)上建立了軟件與環(huán)境交互的{0,1}-模型。其基本思想是考察軟件的任意執(zhí)行是否是環(huán)境所允許的執(zhí)行。若軟件的一個(gè)執(zhí)行路徑上的動(dòng)作都是環(huán)境允許的,則當(dāng)軟件選擇這條路徑運(yùn)行時(shí),可以與環(huán)境成功交互。若有一個(gè)動(dòng)作不被環(huán)境允許,則不能與環(huán)境交互。只有當(dāng)軟件的所有路徑都是環(huán)境所允許的,軟件才能與環(huán)境成功交互。{0,1}-模型對(duì)軟件與環(huán)境交互的刻畫是非常嚴(yán)格的。然而,在實(shí)際應(yīng)用中,有時(shí)軟件與環(huán)境可能交互一段時(shí)間后才會(huì)出現(xiàn)錯(cuò)誤,導(dǎo)致軟件在環(huán)境下運(yùn)行終止。為了描述這種交互,文獻(xiàn)[12]等一般化了{(lán)0,1}-模型,提出了部分交互模型。

在實(shí)際應(yīng)用中,有時(shí)需要建立環(huán)境之間的量化模型關(guān)系,以此比較環(huán)境的好壞。而對(duì)同一軟件來(lái)說(shuō),在不同的環(huán)境下運(yùn)行,其效果不同,所以對(duì)環(huán)境的比較,不能只單純地考察環(huán)境,應(yīng)結(jié)合軟件進(jìn)行比較。對(duì)環(huán)境的量化分析已經(jīng)存在一些研究成果。當(dāng)把環(huán)境用進(jìn)程表示時(shí),對(duì)環(huán)境的比較可以用進(jìn)程之間的度量模型來(lái)建立,如文獻(xiàn)[13]在強(qiáng)/弱互模擬基礎(chǔ)上,建立了強(qiáng)/弱互模擬索引,進(jìn)而建立了進(jìn)程之間近似程度的量化模型。文獻(xiàn)[14-15]在標(biāo)號(hào)轉(zhuǎn)換系統(tǒng)的基礎(chǔ)上,對(duì)進(jìn)程之間的近似程度進(jìn)行了量化描述。文獻(xiàn)[16]建立反應(yīng)模型(reactive model)的量化模型。為了對(duì)已有量化模型進(jìn)行比較分析,文獻(xiàn)[17]利用game理論建立了這些度量的譜結(jié)構(gòu)。由于軟件與環(huán)境之間的依賴關(guān)系,這些量化模型中沒(méi)有考慮軟件對(duì)環(huán)境的影響。另一方面,當(dāng)用集合表示環(huán)境時(shí),如何來(lái)描述環(huán)境之間的度量還沒(méi)有很好研究成果。本文在軟件與環(huán)境部分交互模型的基礎(chǔ)上,建立了環(huán)境之間近似程度的度量描述。

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

2.1 CCS基礎(chǔ)

定義1(進(jìn)程表達(dá)式)[9]進(jìn)程表達(dá)式集合ε是包含?,R和下列表達(dá)式的最小集合,其中,E,Ei∈ε:

其中,L?L;f是重新標(biāo)號(hào)函數(shù)。

若一個(gè)進(jìn)程表達(dá)式中不含變量,稱這個(gè)表達(dá)式是一個(gè)進(jìn)程。用P表示所有進(jìn)程構(gòu)成的集合,P,Q,…表示其中的元素。

定義2(標(biāo)號(hào)轉(zhuǎn)換系統(tǒng))[9]三元組表示Act集合上的標(biāo)號(hào)轉(zhuǎn)換系統(tǒng),(α∈Act)由下面規(guī)則給出:

2.2 進(jìn)程與環(huán)境交互[0,1]-模型

馬艷芳等為了描述軟件與環(huán)境的部分交互,一般化了{(lán)0,1}-模型,提出了部分交互模型。首先介紹可觀測(cè)完整跡語(yǔ)義。

定義3(可觀測(cè)完整跡)[15]若,則P是一個(gè)進(jìn)程。如果存在P′∈P使得且init(P′)=?,則稱σ是進(jìn)程P的可觀測(cè)完整跡。用OCT(P)表示進(jìn)程P所有可觀測(cè)完整跡構(gòu)成的集合;表示P可觀測(cè)完整跡的個(gè)數(shù)。

令Env表示所有環(huán)境的集合,Env={H|H?L},Env?ρ(L),其中ρ(L)表示L的冪集。

定義4令H∈Env,σ∈OCT(P),σ=λ1λ2…λt,則。若,則稱可觀測(cè)完整跡σ滿足環(huán)境,用σ?H表示[15]。

令H∈Env,σ∈OCT(P),且σ=λ1λ2…λt。若任意1≤i≤k≤t,λi?H,但i=k+1,λk+1?H,則記。意思是:yi(1≤i≤k)都是環(huán)境允許的,當(dāng)執(zhí)行到y(tǒng)k+1時(shí),其不被環(huán)境允許,所以軟件將停止。由此,軟件與環(huán)境只能交互k步,下面介紹可觀測(cè)完整跡與環(huán)境部分交互的形式化描述。

定義5 設(shè)P∈P,H∈Env,進(jìn)程P與環(huán)境H交互的結(jié)果函數(shù):OCT(P)→[0,1]定義為[17]:對(duì)任意σ∈OCT(P):

定義6設(shè)P∈P,H∈Env。進(jìn)程P與環(huán)境H部分交互的度量定義為[17]:

3 基于軟件的環(huán)境近似度量

3.1 環(huán)境度量

一個(gè)軟件在不同環(huán)境下運(yùn)行其效果不同。若軟件的運(yùn)行環(huán)境非常相似,則其運(yùn)行結(jié)果也應(yīng)該相差不大。而在實(shí)際應(yīng)用中,對(duì)于給定的軟件,有時(shí)需要對(duì)其運(yùn)行的環(huán)境進(jìn)行比較,如構(gòu)建了2個(gè)實(shí)驗(yàn)環(huán)境,需要比較軟件在哪個(gè)實(shí)驗(yàn)環(huán)境下運(yùn)行的更好。由此,需要建立在給定軟件下,環(huán)境之間的近似程度。根據(jù)軟件與環(huán)境的部分交互,下面將給出特定軟件下環(huán)境之間的近似度量模型。

定義7設(shè)P∈P,H1,H2∈Env,則:Env×Env→[0,1],定義為:

下面介紹實(shí)例對(duì)環(huán)境度量進(jìn)行分析。

例1:若存在一段程序,其用進(jìn)程代數(shù)語(yǔ)言(CCS)可以抽象表示為進(jìn)程:P=a.b.0+b.c.0。假定其執(zhí)行環(huán)境有H1={a,b,d,e},H2={a,c},則根據(jù)定義5可得:

在通信系統(tǒng)演算(CCS)的實(shí)際應(yīng)用中,一般地,對(duì)于具體的程序采用狀態(tài)轉(zhuǎn)換圖來(lái)表示。每條邊表示一個(gè)事件,即一個(gè)語(yǔ)句,每個(gè)節(jié)點(diǎn)表示狀態(tài)。執(zhí)行這個(gè)語(yǔ)句可以引起一個(gè)狀態(tài)到另一個(gè)狀態(tài)的轉(zhuǎn)換.在轉(zhuǎn)換過(guò)程中需要與環(huán)境進(jìn)行交互才能完成狀態(tài)的改變。下面列舉一個(gè)用C語(yǔ)言程序的例子說(shuō)明環(huán)境的度量模型。

例2:用C語(yǔ)言編寫一個(gè)程序?qū)崿F(xiàn)下面的功能:先從鍵盤上輸入一個(gè)值,如果輸入的值小于3,將這個(gè)值加1,然后輸出結(jié)果,否則將這個(gè)值加2,最后輸出結(jié)果。某個(gè)程序員給出如下的程序,記為P1。

該段程序的狀態(tài)轉(zhuǎn)換圖如圖1所示。當(dāng)在Win-TC編譯器下運(yùn)行時(shí),沒(méi)能實(shí)現(xiàn)要求的功能。

圖1 程序P1的狀態(tài)轉(zhuǎn)換圖

而當(dāng)改變?nèi)肿兞康穆暶鲿r(shí),則可以得到下面的程序P2,其能夠?qū)崿F(xiàn)要求的功能。狀態(tài)轉(zhuǎn)換圖如圖2所示。

圖2 程序P2的狀態(tài)轉(zhuǎn)換圖

用H2={(x,int),(y,float),(z,int)}來(lái)表示程序段P的環(huán)境。

接下來(lái)討論環(huán)境度量模型的一些代數(shù)性質(zhì)。根據(jù)定義7,可以得到下面的性質(zhì)。

證明:由定義7可證。

證明:由命題1可證。

3.2 環(huán)境的偏序

在實(shí)際應(yīng)用中,除了對(duì)環(huán)境之間的進(jìn)行度量,有時(shí)需要對(duì)環(huán)境進(jìn)行比較,如給定2個(gè)實(shí)驗(yàn)環(huán)境,如何確定哪一個(gè)更加適合于給定的軟件。根據(jù)軟件與環(huán)境的部分交互,若軟件與環(huán)境的部分交互度量值越大,說(shuō)明軟件在這個(gè)環(huán)境下的交互能力越強(qiáng),進(jìn)而軟件在此環(huán)境下成功運(yùn)行的概率越大。由此,根據(jù)軟件與環(huán)境的交互能力,可以建立環(huán)境之間的偏序關(guān)系,進(jìn)而建立評(píng)價(jià)環(huán)境好壞的標(biāo)準(zhǔn)。下面將給出在給定軟件和[0,1]-模型下如何評(píng)價(jià)環(huán)境。

從定義8可知,若軟件與環(huán)境的交互度量越大,說(shuō)明此環(huán)境對(duì)于給定軟件來(lái)說(shuō),在其上運(yùn)行的效果越好。

證明:由定義8可知。

定理2表明,在給定軟件和[0,1]-模型下,軟件運(yùn)行的最好環(huán)境是與Env等價(jià)環(huán)境,由于Env包含了所有的環(huán)境,說(shuō)明在這樣的環(huán)境下,軟件一定能夠與環(huán)境成功交互。最差的環(huán)境是與Φ等價(jià)的環(huán)境,由于空集不包含任何元素,因此在這樣的環(huán)境下,軟件一定不能與環(huán)境成功交互,當(dāng)然這樣的環(huán)境是最差的。

隨著分布式系統(tǒng)的應(yīng)用和發(fā)展,分布式軟件的開(kāi)發(fā)環(huán)境越來(lái)越復(fù)雜。在分布式軟件的開(kāi)發(fā)環(huán)境中,相關(guān)的接口越來(lái)越多,若接口之間是兼容的,則執(zhí)行對(duì)象操作的對(duì)象可以相互通信。根據(jù)進(jìn)程代數(shù)理論,可以將接口之間的兼容用動(dòng)作和動(dòng)作的補(bǔ)進(jìn)行抽象,若一個(gè)動(dòng)作能找到其補(bǔ)動(dòng)作,則這2個(gè)接口是兼容的。另一方面,接口可以看成是系統(tǒng)的環(huán)境,將系統(tǒng)抽象成進(jìn)程,接口抽象為動(dòng)作集合,當(dāng)系統(tǒng)運(yùn)行過(guò)程中,尋找合適的接口,若能匹配,則表示可以交互。同時(shí),對(duì)于不同的開(kāi)發(fā)環(huán)境,其接口配置不同,所以對(duì)這些開(kāi)發(fā)環(huán)境的比較,可以通過(guò)這些接口與系統(tǒng)之間的交互來(lái)進(jìn)行。

根據(jù)進(jìn)程代數(shù)理論,首先需要將環(huán)境和系統(tǒng)抽象表示成進(jìn)程或動(dòng)作集合。文獻(xiàn)[18]開(kāi)發(fā)的UPPAL系統(tǒng)是對(duì)實(shí)時(shí)系統(tǒng)進(jìn)行建模、確認(rèn)和驗(yàn)證的綜合工具平臺(tái)。它將實(shí)時(shí)系統(tǒng)建模為時(shí)間自動(dòng)機(jī),并擴(kuò)展其數(shù)據(jù)類型包括有界整數(shù)、數(shù)組等?？梢宰詣?dòng)實(shí)現(xiàn)實(shí)時(shí)系統(tǒng)中的規(guī)范和安全需求分析。而對(duì)于一般的系統(tǒng)而言,特別是分布式系統(tǒng),目前還沒(méi)有很好的工具將其抽象為進(jìn)程,所以,對(duì)于本文提出的環(huán)境量化模型,目前還沒(méi)有很好的方法從實(shí)踐中找到合適的驗(yàn)證。這也是下一步將要進(jìn)行的工作。

4 結(jié)束語(yǔ)

軟件的運(yùn)行依賴于環(huán)境,不同環(huán)境對(duì)軟件的運(yùn)行效果起到不同的作用。本文結(jié)合軟件本身,建立了環(huán)境之間近似程度的量化模型。同時(shí),為了對(duì)不同環(huán)境進(jìn)行比較,建立環(huán)境之間的偏序關(guān)系,進(jìn)而為評(píng)估環(huán)境的好壞提供了一定的理論依據(jù)。隨著網(wǎng)絡(luò)逐漸轉(zhuǎn)向了開(kāi)放動(dòng)態(tài)的環(huán)境,軟件的運(yùn)行環(huán)境越來(lái)越復(fù)雜,而軟件在這種復(fù)雜環(huán)境下運(yùn)行時(shí),對(duì)其與環(huán)境的交互能力要求越來(lái)越高。在傳統(tǒng)環(huán)境下不能交互時(shí),在開(kāi)放環(huán)境下能夠交互。由此,今后將建立更加寬松的交互模式,以適應(yīng)開(kāi)放動(dòng)態(tài)環(huán)境的發(fā)展。

[1] Galin D.SoftwareQualityassurance:Fromtheoryto Implementation[M].[S.1.]:PearsonEducation Limited,2005.

[2] 劉 克,單志廣,王 戟,等.可信軟件基礎(chǔ)研究重大研究計(jì)劃綜述[J].科學(xué)進(jìn)展與展望,2008,(3): 145-151.

[3] 沈昌祥,張煥國(guó),王懷民,等.可信計(jì)算的研究與發(fā)展[J].中國(guó)科學(xué)F輯:信息科學(xué),2010,40(2): 139-166.

[4] LARSEN K G.Context-dependent Bisimulation Between Process[D].Aalborg University Centre Strandvejen, Doctor of Philosophy University of Edinburgh,1986.

[5] 馬艷芳,張 敏,陳儀香.軟件動(dòng)態(tài)正確性的形式化描述[J].計(jì)算機(jī)研究與發(fā)展,2013,50(3):626-635.

[6] Ma Yanfang,Zhang Min.Topological Construction of Parameterized Bisimulation Limit[J].Electronic Notes in Theoretical Computer Science,2009,257(1):5-70.

[7] Cleaveland R,Dsysr Z,Smolka S A,et al.Testing Preorder for Probabilistic Processes[J].Information and Computation,1999,154(1):93-148.

[8] Cheung L,StoelingaM,VaandragerF.ATesting Scenario for Probabilisitic Processes[J].Journal of the ACM,2007,54(6):1-44.

[9] He Jifeng,HoaerT.EquatingBisimulationwith Refinement[R].China,Macau,Technical Report:UNUIIST-282,2003.

[10] Ggabbeek R J.TheLinearTime-branchingTime Spectrum I[EB/OL].(2013-02-03).http://theory. stanford.edu/rvg.

[11] 馬艷芳,陳 亮.基于交互的環(huán)境近似度量模型[J].山東大學(xué)學(xué)報(bào):理學(xué)版,2013,48(7):33-38.

[12] 馬艷芳,陳 亮.基于部分交互的軟件近似量化模型[J].計(jì)算機(jī)工程與應(yīng)用,2014,50(24):32-37.

[13] Ying Mingsheng.BisimulationIndexesandTheir Applications[J].Theoretical Computer Science,2002, 275(1/2):1-68.

[14] Thrane C,Fahrenberg U,LarsenKG.Quantitative Analysis of Weighted Transition Systems[J].Journal of Logic and AlgebraicProgramming,2010,79(7): 689-703.

[15] Larsen K G,Faahrenberg U,Thrane C.Metrics for WeightedTransitionSystems:Axiomatizationand Complexity[J].Theoretical Computer Science,2011, 412(28):3358-3369.

[16] Henzinger T A.QuantitativeReactiveModelingand Verification[J].ComputerScience-researchand Development,2013,28(1):331-344.

[17] Fahrenberg U,LegayA.TheQantitativeLineartimebranching-time Spectrum[J].Theoretical Computer Science,2014,538(5):54-69.

[18] Larsen K G.UPPAL Document[EB/OL].(2013-12-12). http://www.uppaal.com/.

編輯 索書志

Quantitative Model of Environment Based on Software

MA Yanfang
(School of Computer Science and Technology,Huaibei Normal University,Huaibei 235000,China)

With the development of Internet,the environment of software is gradually changed to the open and dynamic environment.So,the results of software executing on different environment affect on the trustworthiness of software.In some special fields,it is necessary to establish an experiment environment in order to test the property of software.So,it is important to evaluate the degree to which experiment environment approximates the real environment.This paper uses measure theory in topology and partial order in domain theory,the quantitative model to describe the approximate degree between environment is proposed based on process algebra.The quantitative model to compute the approximate degree between environments is presented based on the partial iteration between software and its environment.Furthermore,some examples is showed to verify the model and some algebraic properties is proved.

interaction;environment;process algebra;measurement;domain theory

馬艷芳.基于軟件的環(huán)境量化模型[J].計(jì)算機(jī)工程,2015,41(2):47-51,56.

英文引用格式:Ma Yanfang.Quantitative Model of Environment Based on Software[J].Computer Engineering, 2015,41(2):47-51,56.

1000-3428(2015)02-0047-05

:A

:TP301

10.3969/j.issn.1000-3428.2015.02.010

國(guó)家自然科學(xué)基金資助項(xiàng)目(61300048);安徽省自然科學(xué)基金資助項(xiàng)目(1308085QF117);安徽高校省級(jí)自然科學(xué)研究基金資助重點(diǎn)項(xiàng)目(KJ2014A223);安徽省高等教育振興計(jì)劃重大教學(xué)改革研究基金資助項(xiàng)目(2014ZDJY058);2014年安徽省高校優(yōu)秀青年人才支持計(jì)劃基金資助項(xiàng)目。

馬艷芳(1978-),女,副教授、博士,主研方向:可信度量模型,形式化方法。

2014-07-24

:2014-09-02E-mail:clmyf@163.com