基于軟件的環境量化模型

馬艷芳

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

基于軟件的環境量化模型

馬艷芳

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

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

:交互;環境;進程代數;度量;論域理論

1 概述

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

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

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

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

2 預備知識

2.1 CCS基礎

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

其中,L?L;f是重新標號函數。

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

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

2.2 進程與環境交互[0,1]-模型

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

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

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

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

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

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

3 基于軟件的環境近似度量

3.1 環境度量

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

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

下面介紹實例對環境度量進行分析。

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

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

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

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

圖1 程序P1的狀態轉換圖

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

圖2 程序P2的狀態轉換圖

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

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

證明:由定義7可證。

證明:由命題1可證。

3.2 環境的偏序

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

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

證明:由定義8可知。

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

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

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

4 結束語

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

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

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

[3] 沈昌祥,張煥國,王懷民,等.可信計算的研究與發展[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] 馬艷芳,張 敏,陳儀香.軟件動態正確性的形式化描述[J].計算機研究與發展,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] 馬艷芳,陳 亮.基于交互的環境近似度量模型[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

馬艷芳.基于軟件的環境量化模型[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年安徽省高校優秀青年人才支持計劃基金資助項目。

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

2014-07-24

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