马艳芳,陈 亮
1.淮北师范大学 计算机科学与技术学院,安徽 淮北 235000
2.上海市高可信计算重点实验室,上海 200062
3.淮北师范大学 数学科学学院,安徽 淮北 235000
基于部分交互的软件近似度量模型
马艳芳1,2,陈 亮3
1.淮北师范大学 计算机科学与技术学院,安徽 淮北 235000
2.上海市高可信计算重点实验室,上海 200062
3.淮北师范大学 数学科学学院,安徽 淮北 235000
随着信息技术的发展,软件系统变得越来越庞大和复杂,缺陷和漏洞难以避免,人们开始对软件的质量进行研究。软件可信性是评价软件质量的重要标准。近年来,软件的可信性模型越来越得到关注。如,陈仪香等,根据软件的各种属性,建立了基于属性和权值的软件可信性量化模型[1-3]。徐峰等建立了软件服务协议的可信性评估模型[4]。随着网络的发展和服务意识的增强,计算模式逐渐转向以网络为中心和面向服务的体系结构,从而软件的运行环境(包括网络环境、物理环境)逐渐转向开放、动态的环境[5-7]。软件的运行环境对软件的可信性有着很大影响。在实际应用中,由于环境资源的有限性等原因,有时软件在环境下执行到一定程度可能出现错误信息,从而软件与环境未必成功交互。为了保证软件在环境下继续执行,需要找出软件与环境交互出错的原因,而计算软件与环境的交互程度可以帮助找到出错的原因,进而为改进软件与环境的交互提供一定的依据。
为了研究软件与环境的交互,首先需要对环境进行描述。根据Milner提出的通信系统演算[8-9](Communication and Compuation of Systems,CCS),从测试角度出发,环境可以用进程表示。如Larsen提出的参数化互模拟[10],用一个标号转换系统(labeled transition system)表示环境,明确地给出环境的变化过程。Smolka等也将环境表示成进程,其中包含一个表示成功的动作[11-13]。若软件与环境并发执行时能够执行到这个动作,则表明软件与环境可以成功交互。而随着网络和服务的发展,软件的运行环境逐渐开放,从而使得软件对环境的要求越来越宽松,由此用进程表示环境不能适应计算模式的发展。更加一般地,环境可以用动作集合来表示。在动作之间没有先后顺序。如文献[14-15]中所提到的进程失败语义,从拒绝环境的角度来考虑进程之间的关系,此时的环境是一些动作构成的集合。当用集合表示环境时,集合中的元素由能够引起软件变化的信息或事件构成。从软件方面上,可以是软件的内部结构,如程序中声明的全局变量。从硬件方面上,可以是软件运行的硬件设备或网络环境等。
为了描述当把环境作为一个集合考虑时进程与环境的交互,马艳芳等建立了进程与环境交互的{0,1}-模型[16]。其研究交互的基本思想是:考察软件的所有执行路径,当软件选择一条路径执行时,运行环境能提供其需要的所有信息,则这条路径与环境交互的结果赋值为“1”,否则赋值为“0”。这种软件与环境的交互是非常严格的交互。若软件与环境成功交互,环境必须提供软件所需要的所有信息。然而,在软件的实际运行中,环境未必能够提供软件所需要的所有信息,软件在环境下可能运行到某个地点而停滞,那么如何建立这种软件与环境的交互模型,本文将以CCS模型为基础,一般化{0,1}模型。
另一方面,为了测试不同软件在环境下的性能,在实际应用中,有时需要对软件进行比较。在一些特殊领域,例如航空航天领域,生物工程领域等,有时无法把软件放在实际环境下运行,需要先建立一个实验环境,在该环境下测试软件的性能。而在该环境下开发出来的软件,对其正确性等要求非常苛刻,经常利用不同的方法开发软件,为了开发出更加适合于该实验环境的软件,需要对不同的开发版本进行比较。对软件的比较已经有了很多方法,如应明生等在CCS理论基础上,将软件抽象为进程,利用进程之间的强/弱互模拟关系,建立软件之间近似程度的量化模型[17]。Smolka等为了说明带有概率信息软件之间的近似程度,提出了ε-互模拟等价,并建立了两个概率进程之间近似程度的度量模型[18]。邓玉欣等在概率CSP模型基础上,根据概率进程执行相同迹的概率和折扣因子建立了进程之间的度量。这个折扣因子反应了当软件执行相同迹的深度越大,他们之间越近似[19]。马艳芳等基于ε-互模拟提出了软件近似正确性模型[20]。但是考虑到环境对软件的影响,对软件进行比较时,需要考虑软件与环境的交互能力。上述软件之间的近似度量模型,没有反映环境对软件的影响。本文将以CCS模型为基础,从软件与环境的交互能力方面,建立软件近似程度的量化模型。
2.1 CCS基础
令Δ表示动作名集合,用小写字母a,b,c,…表示其中的元素。={aˉ|a∈Δ}表示补动作名的集合。规定表示动作a。用L=Δ∪表示标号集合,λ,μ,…表示其中的元素。τ表示不可观测动作,。用Act表示所有动作的集合,Act=L∪{τ},α,β,…表示其中的元素。令映射 f∶L→L,若满足=,称 f为重新标号函数。若令 f(τ)=τ,则 f可以延拓到集合Act上。同时,令X是L的子集。定义{∈X},X∪{τ}。进一步,用表示所有进程变量构成的集合,X,Y,…表示其中的元素。R表示所有进程常量构成的集合,A,B,…表示其中的元素。I或J是索引集合。进程表达式的集合定义如下。
定义1(进程表达式)[8]进程表达式集合ε是包含,R和下列表达式的最小集合,其中E,Ei∈ε:
其中L⊆L,f是重新标号函数。
若一个进程表达式中不含变量,称这个表达式是一个进程。用P 表示所有进程构成的集合,P,Q,…表示其中的元素。若A∈R,则A表示一个常量,其定义如下,其中PA∈P 。例如,。在通信系统演算中,常量提供了一种递归机制。
定义2(标号转换系统)[8]三元组(ε,Act,{|α∈Act})表示Act集合上的标号转换系统,(α∈Act)由下面规则给出。
2.2 进程的迹和完整迹语义
为了建立软件与环境交互模型,马艳芳等在文献[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]。
可以根据进程的结构求出可观测完整迹。
性质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是一个单调函数,而0是零进程。
根据通信系统演算,软件可描述为进程,所以软件的每个执行路径可以描述成一个可观测完整迹。要研究软件与环境的交互,首先要描述软件的执行路径与环境之间的交互。令Env表示所有环境的集合,Env= {H|H⊆L},所以Env⊆ρ(L),其中ρ(L)表示L的幂集。
接下来给出进程的一个可观测完整迹满足环境的定义。设 P∈P,OCT(P)={σ1,σ2,…,σm}。设 H∈Env是一个环境,用Act(H)表示环境H所包含的所有动作构成的集合。任意σ∈OCT(P),用 Act(σ)表示σ中包含的所有动作构成的集合,用|σ|表示σ中包含动作的个数,称为σ的长度。
在{0,1}-模型中,软件与环境的交互结果要么是“0”要么是“1”。这种交互没办法区分软件与环境之间部分交互的情况:即软件的执行路径中有些需要的信息,运行环境没有提供,但是此时软件可以在环境下运行一段时间,在找不到需要的信息时软件运行出错。换句话说,虽然执行路径中有一个动作未能在环境中找到对应的匹配,而此动作之前的动作都在环境中找到相应的匹配,此时软件至少可以与环境交互到不匹配的动作之前。这时,软件与环境能够部分交互。用这条路径能够与环境部分交互的程度来定义这条路径与环境交互的结果。由此可以看出,此时软件的执行路径与环境的交互结果不再是“0”或“1”,而是[0,1]区间内的某个值,把这种交互结果在[0,1]区间的度量模型,称为[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 ,表示执行路径σ中第一个在环境中找不到匹配的动作,而前面的所有动作都能在环境找到相应的匹配。
定义5设P∈P,H∈Env,进程P与环境H交互的结果函数 R[H0,1](P)∶OCT(P)→[0,1]定义如下,任意σ∈OCT(P),
下面定义进程与环境交互的度量模型如下:
定义6设P∈P,H∈Env,进程P与环境H交互的度量定义为:
定义6考查了软件的所有执行路径中能够与环境进行交互的概率。
例1设有一个卖咖啡和牛奶的自动售货机W。用CCS语言抽象为进程W=1元.(咖啡+牛奶).出口.W。
通过此表达式可知,若想从这台售货机上买一杯咖啡或者牛奶,先要投入1元,然后选择“咖啡”或者“牛奶”按钮,最后从出口取出。根据自动售货机的功能,此表达式是一个递归进程。机器运行一次时,其可观测完整迹有两个,分别是σ1=1元 咖啡 出口和σ2= 1元 牛奶 出口。
在通信系统演算的实际应用中,对于具体的程序采用状态转换系统来表示。每个节点表示状态,每条边表示一个事件,即一个语句。执行这个语句可以引起一个状态到另一个状态的转换。在转换过程中需要与环境进行交互才能完成状态的改变。下面列举一个用C语言编写的程序来说明软件与环境的交互。
例2用C语言编写一个程序,该程序的功能是:先从键盘上输入一个值,如果输入的值小于3,将这个值加1,然后输出结果,否则将这个值加2,然后输出结果。某个程序员给出如下的程序,记为P1,状态转换图如图1所示。
图1 P1的状态转换图
为简单起见,不考虑程序运行的硬件环境,该程序声明的全局变量可以看出是其运行的环境,用动作集合表示为H={(x,int),(y,int),(z,int)}。这段程序的状态转换图如图1所示。当在Win-TC编译器下运行时,其能够实现要求的功能。在这个状态转换图中,从初始状态执行 scanf("\%d",&x),对x=n赋值,获得下一个状态。此时,状态从{(x=0,int),(y=0,int),(z=0,int)}变为{(x=n,int),(y,int),(z,int)},其中只有变量x的值发生了变化。在这个状态转换中,总蕴含着与环境进行交互。这种交互主要是将执行语句所获得的x,y,z的值与环境进行比较。如果是环境允许的,可以正确执行,否则不能得到正确的结果。为了更加方便地描述交互,在计算完整迹时,只考虑变量值改变的过程。在左边的完整迹中,其变化次序为:先是变量x的值发生变化,然后执行“z=x+1”使得变量z的值发生变化,最后执行printf("%d",z),使得变量z的值变化,因此变化次序是{(x,int),(z,int),(z,int)}。同理可得,右边的完整迹中变化次序为{(x,int),(y,int),(y,int)}。而这个执行路径中,变量的变化都是环境允许的,从而根据定义5,对这个执行路径赋值都是“1”,再根据定义6,可得,p[0,1](P1,H)=1。此结果表明这段程序可以与环境成功交互。
有些程序员也可能给出下面的程序,用 P2表示,这个程序也能实现要求的功能。其状态转换图如图2所示。
图2 P2的状态转换图
程序P2与P1的不同之处在于语句“y=x+2.2”将变量y赋值为一个浮点型数据。由于C语言能够进行类型转换,可以将y的类型强制转换为整型。进而程序P2也可以实现要求的功能,环境是H={(x,int),(y,int),(z,int)},可以求出 p[0,1](P2,H)=1。
一些程序员也可能给出下面的程序,用P3来表示,其没有实现要求的功能,标号转换系统如图3所示。
图3 P3的状态转换图
在左边的完整迹中,变量的变化次序是{(x,int),(z,int),(z,int)},赋值为1。而右边的完整迹中,当执行printf("%f",y)时,变量 y类型的变化不是环境运行的,其变化次序{(x,int),(y,int),(y,float)},根据定义5,右边的完整迹赋值为。进一步由定义6,可以计算得到这段程序与环境的交互度量为也就是说此程序没有和环境进行成功交互,其成功交互的概率是。
在实际应用中,经常会遇到在同一环境下对不同的软件进行比较。根据CCS语言,软件可以抽象成进程。特别对实时系统,已经存在相应的建模和验证工具,如UPPAAL。其可以用来对被转换时间自动机网络模型的实时系统进行建模、校验和验证。它是由瑞典Uppsala大学的信息技术学院和丹麦Aalborg大学的计算科学学院联合开发的。而对于一般的软件还没有具体的工具对其进行建模。但是对于规模较小的软件,根据CCS模型,可以用标号转化系统对其建立状态转换图,从而抽象出它的可观测完整迹。例如例2中的程序段,可以抽象成状态转换图。由于软件的运行依赖于环境,在对软件进行比较时,需要考虑环境的因素。而环境对软件的影响主要体现在软件与环境的交互,所以可以从软件与环境的交互能力方面来评价软件的好坏。那么如何来评价这些软件在与环境交互方面的能力呢?由于[0,1]-模型不同于{0,1}-模型,所以在本章中将建立在[0,1]-模型和给定环境下两个软件之间的近似度量模型以及在特定环境下评价软件好坏的标准。首先建立基于环境和[0,1]-模型的软件近似度量。
例3假设某两个程序用CCS语言抽象表示为进程P=a.b.0+a.c.0+a.0,Q=a.b.0+a.c.0。执行环境有E= {a,b,d}。则根据定义5可知:
性质4说明当两个软件是完整迹等价时,它们关于环境H近似度为1。由此可以根据完整迹等价算法来计算软件与环境之间的近似度量。从定义7可知,对于一个给定的环境,当两个软件之间的差距越小,它们与给定环境在[0,1]-模型下的交互能力差距就越小。而当软件的执行路径较多时,将影响软件的运行速度,从而降低了软件与环境交互的能力。由此,可以利用软件与环境成功交互的概率来评价软件与环境交互能力的好坏。接下来根据软件与环境成功交互的概率来比较软件的好坏。
这个定义是说,若软件Q与环境H在模型[0,1]上的交互度量值比P与环境H交互度量值大,那么在环境H下软件Q比P好。
例4设有一个卖咖啡和牛奶的自动售货机W如例1所示。有另一台只卖咖啡的自动售货机P,P=1元.咖啡.出口.P。若某个顾客想买咖啡,用集合H={1元,咖啡,出口}表示,则可知(W,H)=,而(P,H)=1,故(W,H)≤(P,H),所以W⊆。说明对于环境H来说,P比W要好,因为其不需要做任何选择就可以买到想好的咖啡。
例5对例2中的三段程序进行比较,在声明了全局变量H={(x,int),(y,int),(z,int)}下,可以看出(P1,H)= 1=(P2,H),由此程序 P1和 P2一样好。但是由于(P3,H)=,所以P3不如P1和P2好,因为其没有实现所要求的功能。
性质6表示在[0,1]-模型和给定环境H下,与零进程等价的软件都是最差的软件,即什么都没做的软件是最差的。
在本文中主要以CCS语言为基础,建立了软件与环境的部分交互模型,同时,从与环境交互能力方面,讨论了软件的近似程度,以及比较软件好坏的标准,证明一些代数性质。
而在软件的分析和设计过程中,模块化和层次化方法是经常使用的方法。而在讨论软件与环境的部分交互时,是否也能采用模块化的方法来获得软件与环境的交互度量?在接下来的工作中,将对此问题进行研究。
[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]沈昌祥,张焕国,王怀民,等.可信计算的研究与发展[J].中国科学 F辑:信息科学,2010,40(2):139-166.
[7]郑志明,马世龙,李未,等.软件可信复杂性及其动力学统计分析[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]马艳芳,陈亮.基于交互的环境近似度量模型[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
软件对环境的依赖性主要体现在软件与环境的交互。在实际中,有时软件与环境未必成功交互。其交互程度对软件的性能有着很大的影响。为测试不同软件在环境下的性能,需要对软件与环境的交互能力进行比较。在进程代数理论基础上,利用完整迹语义,建立软件近似程度的量化模型。形式化描述软件与环境的部分交互。列举一些例子对模型进行说明。建立软件近似程度的量化模型,证明一些代数性质。进一步,建立评价软件在与环境交互方面好坏的标准。
部分交互;度量;形式化;进程代数
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)。
马艳芳,女,博士,副教授,主要从事进程演算、程序语义、软件可信性等方面的研究;陈亮,通讯作者,男,博士,副教授,主要从事数值计算、矩阵计算、算法等方面的研究。E-mail:clmyf2@163.com
2014-03-26
2014-06-25
1002-8331(2014)24-0032-06
CNKI网络优先出版:2014-09-04,http∶//www.cnki.net/kcms/doi/10.3778/j.issn.1002-8331.1403-0401.html