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

馬艷芳

(淮北師范大學計算機科學與技術學院,安徽淮北235000)

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

馬艷芳

(淮北師范大學計算機科學與技術學院,安徽淮北235000)

在一些特殊領域中需要建立一定的實驗環(huán)境對軟件性能進行測試,因此實驗環(huán)境與實際環(huán)境之間的近似程度對軟件的性能起到關鍵作用。為建立環(huán)境之間的近似度量,在進程代數(shù)理論基礎上,根據軟件與環(huán)境的交互程度,利用拓撲度量和論域理論中的偏序關系,建立實驗環(huán)境之間近似程度的量化模型。根據軟件與環(huán)境之間的部分交互,建立實驗環(huán)境之間近似程度的度量模型。通過實例對度量模型進行說明,并證明度量模型的代數(shù)性質。

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

1 概述

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

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

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

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

2 預備知識

2.1 CCS基礎

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

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

若一個進程表達式中不含變量,稱這個表達式是一個進程。用P表示所有進程構成的集合,P,Q,…表示其中的元素。

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

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

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

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

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

定義4令H∈Env,σ∈OCT(P),σ=λ1λ2…λt,則。若,則稱可觀測完整跡σ滿足環(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)境允許的,當執(zhí)行到y(tǒng)k+1時,其不被環(huán)境允許,所以軟件將停止。由此,軟件與環(huán)境只能交互k步,下面介紹可觀測完整跡與環(huán)境部分交互的形式化描述。

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

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

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

3.1 環(huán)境度量

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

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

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

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

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

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

該段程序的狀態(tài)轉換圖如圖1所示。當在Win-TC編譯器下運行時,沒能實現(xiàn)要求的功能。

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

而當改變全局變量的聲明時,則可以得到下面的程序P2,其能夠實現(xiàn)要求的功能。狀態(tài)轉換圖如圖2所示。

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

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

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

證明:由定義7可證。

證明:由命題1可證。

3.2 環(huán)境的偏序

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

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

證明:由定義8可知。

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

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

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

4 結束語

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

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

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

[3] 沈昌祥,張煥國,王懷民,等.可信計算的研究與發(fā)展[J].中國科學F輯:信息科學,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] 馬艷芳,張 敏,陳儀香.軟件動態(tài)正確性的形式化描述[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].山東大學學報:理學版,2013,48(7):33-38.

[12] 馬艷芳,陳 亮.基于部分交互的軟件近似量化模型[J].計算機工程與應用,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].計算機工程,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

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

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

2014-07-24

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