基于软件的环境量化模型

马艳芳

(淮北师范大学计算机科学与技术学院,安徽淮北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