文浩

（福建师范大学,福建 福州350007）

增量模型在软件开发过程中被广泛使用。开发人员根据客户的反馈和需求,对软件进行不断的迭代,并且在当前的版本基础上进行增量开发,以此作为下次交付的新版本。与一些经典模型相比,增量模型结合了瀑布模型的基本组成部分与原型模型的迭代特征,将复杂的系统分解为一个一个的小模块,再逐步进行处理[1,2]。当开发人员面临一些软件开发中的常见问题时,例如因为某些因素,需要回到软件先前的某个版本,我们就会因为逐步开发的策略,从而很好地解决这些问题。因此,迭代的增量模型在软件开发过程中是不可或缺的。

增量开发中最主要的操作之一就是精化（refinement）。精化是对于软件中的某一具体功能进行进一步的开发,即使原来的功能更加具体。例如对于一个ATM机而言,如果初始系统中的取款功能仅仅是根据用户输入的金额,进行出钞,那么当用户输入的金额超出ATM里剩余的金额总量,就可能会出现问题,或者当用户需要在出钞的同时,打印账单,那么原系统也是无法做到的。此时就可以对原系统的取款功能进行精化,从而达到客户的需求。

本文选择使用UML 中的活动图对系统进行建模,描述软件开发中的增量过程。UML 是一种复杂的可视化语言,其中有14种不同的图表类型,具体又可以分为结构和行为两种大类[3]。活动图是行为图中的一种,它可以体现软件系统的控制流和数据流,并且可以清晰地描述每个活动的执行顺序。相比于类似的状态图,活动图可以简要地描述并发并且不用区分全局或者局部的状态,所以在建模复杂系统时,活动图是一种更优的选择。本文中,我们除了给出了活动图的形式语义,还对活动图间的精化过程进行了形式化表达,并且讨论了一些重要的性质。

对于活动图的研究由来以及,但之前的一些研究因为缺乏形式化方法的支撑,导致其可靠性和正确性难以保证,从而无法应用于实际开发中。形式化方法是基于严格数学基础,对计算机软（硬）件系统进行形式规约、开发和验证的技术[4]。其中,形式验证是证明不同形式规约之间的逻辑关系,这些逻辑关系反映了处在不同开发阶段的软件的各类正确性需求。所以,结合增量开发的背景,适当的使用形式化方法可以确保最终产品的可靠性、安全性。特别是对于正确性而言,虽然软件中的一些错误可以被传统的软件测试方法发现,但是对于人工上难以察觉潜在的软件缺陷,只能通过严谨的数学方法来发现及解决。所以本文中对于形式化方法的引用也是极其有必要的。

本文的结构如下：本文第1 节对活动图进行了建模。第2 节基于活动图的模型,提出了精化过程的形式化表达。第3 节定义了精化关系并且讨论了精化关系的常见性质。最后总结全文,并对未来的研究方向进行初步探讨。

1 活动图的形式语义

活动图在视觉上的呈现类似于流程图或数据流程图。但与这些不同的是,活动图在建模工作流或模拟业务流程上有更出色的表现[3]。它可以建模顺序的,并发的以及选择的活动,并且基于开始（初始状态）和结束（最终状态）来描述活动的执行过程。活动图的节点可以分为活动节点、控制节点和对象节点。本文为了简化表达,将对象节点也视为活动节点。

下面给出了活动图的形式语义。

定义1：一个活动图是一个九元组AD=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞,其中

A=AO∪Dn∪Mn∪Fn∪Jn∪Ia∪Fa,

AO,活动节点和对象节点的集合,

Dn,选择节点的集合,

Mn,合并节点的集合,

Fn,分叉节点的集合,

Jn,汇合节点的集合,

R⊆A×A,活动和节点间关系的集合,

Ia,初始节点的集合,

Fa,终止节点的集合。

集合A 中存放的是活动图中的所有节点和边,R 则是定义在A 上的关系,其中的元素是A 通过自身的笛卡尔积所得到的序偶。上述的定义可参照我们之前的一些工作[5,6,7]。

此外,为了方便后续对精化过程的讨论,我们对于任意x∈A,将其前置集记为

°x={y∈A|（y,x）∈R},后置集记为x°={y∈A|（x,y）∈R}。

下面给出一个具体的例子用于解释上述定义。

例1：图1 是一个活动图,可以表示为AD=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞,其中A={i,a,b,c,d,e,j,g,h,dn,fn,jn,mn,f},AO={a,b,c,d,e,g,h,j},Dn={dn},Mn={mn},Fn={fn},Jn={jn},R={（i,a）,（a,dn）,（dn,b）,（b,fn）,（fn,d）,（fn,e）,（d,jn）,（e,jn）,（jn,g）,（g,mn）,（dn,c）,（c,j）,（j,mn）,（mn,h）,（h,f）},Ia={i},Fa={f}。此外,我们可以得到,对于a∈A,°a={i},a°={dn}。

通过例1,我们得知,可以通过上述的方法简单明了地表示一个活动图。

图1 一个活动图的实例

2 活动图间的精化

在软件开发的初期,因为需求不清等诸多因素,开发人员往往是根据个人经验对系统进行建模,这就导致最初的模型处于一个高抽象的层次,即该模型往往存在功能缺失或实现功能不明确等等问题,那么随着需求的逐渐清晰,软件的功能也需要逐渐完善。而精化,也正就是使得高抽象系统不断具体化的一种操作[8]。

为了形式化的表达活动图的精化过程,本文首先给出了一个精化函数。设AO 为活动节点的集合,AD 为活动图的集合,称ref：AO→AD-{Ø}为“精化函数”。

简单来说,活动图间的精化过程就是对于初始的活动图,选择该图中的某一个或者某些活动节点,再用与这些活动节点一一对应的活动图替换之前的节点。下面是精化过程的定义。

定义2：AD=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞是一个活动图。其中存在x∈AO 并且ref（x）=＜A1,AO1,Dn1,Mn1,Fn1,Jn1,R1,Ia1,Fa1＞。此外,需要满足A∩A1=Ø。

那么经过ref（x）精化的活动图AD 就可以被表示为

AD[x/ref（x）]=＜A2,AO2,Dn2,Mn2,Fn2,Jn2,R2,Ia2,Fa2＞,其中

A2=（A∪A1）（{x}∪Ia1∪Fa1）,

AO2=（AO∪AO1）{x},

Dn2=Dn∪Dn1,

Mn2=Mn∪Mn1,

Fn2=Fn∪Fn1,

Jn2=Jn∪Jn1,

R2=R∪R1∪{（m,n）|m∈°x, b ∈ Ia1,n ∈ b°}∪{（k,l）|c∈Fa1,k∈° c,l∈x°}{（m, n）∈R1|m∈Ia1∨n∈Fa1},

Ia2=Ia,

Fa2=Fa。

下面给出一个具体的例子用于解释定义2,例2 中的AD1和AD2分别见图2（a）（b）。

例2：对于图1 中的活动图AD,存在活动节点c∈AO。令AD1=ref（c）=＜A1,AO1,Dn1,Mn1,Fn1,Jn1,R1,Ia1,Fa1＞,其中A1={k,p,q,s,dn’,mn’,i’,f’},AO1= {k,p,q,s},Dn1={dn’},Mn1={mn’},Fn1=Ø,Jn1=Ø,R1= {（i’,k）,（k,dn’）,（dn’,p）,（dn’,q）,（p,mn’）,（q,mn’）,（mn’,s）,（s,f’）},Ia1= {i’},Fa1={f’}。那么基于定义2,就可以得到AD2=AD[c/ref（c）]=＜A2,AO2,Dn2,Mn2,Fn2,Jn2,R2,Ia2,Fa2＞,其中A2={i,a,b,d,e,j,g,h,dn,fn,jn,mn,k,p,q,s,dn’ ,mn’ ,f},AO2= {a,b,d,e,g,h,j,k,p,q,s},Dn2={dn,dn’},Mn2={mn,mn’},Fn2={fn},Jn2={jn},R2={（i,a）,（a,dn）,（dn,b）,（b,fn）,（fn,d）,（fn,e）,（d,jn）,（e,jn）,（jn,g）,（g,mn）,（dn,k）,（k,dn’）,（dn’,p）,（p,mn’）,（dn’,q）,（q,mn’）,（mn’,s）,（s,j）,（j,mn）,（mn,h）,（h,f）},Ia2={i},Fa2={f}。

图2 活动图的精化过程

3 精化关系的性质

第一章中介绍了活动图的形式语义,第二章则给出了活动图间的精化方法。基于上述内容,我们可以简单的概括,当两个活动图的形式语义满足定义2,则称这两个活动图间存在精化关系,下面给出形式化的表达。

定义3：令AD1=＜A1,AO1,Dn1,Mn1,Fn1,Jn1,R1,Ia1,Fa1＞和AD2=＜A2,AO2,Dn2,Mn2,Fn2,Jn2,R2,Ia2,Fa2＞为两个活动图并且ref 表示精化函数,当且仅当存在x∈AO1,使得AD2=AD1[x/ref（x）],则称AD2是AD1的精化,记作AD2＞AD1。

由定义3 和例2 可知,图2（b）和图1 中的两个活动图间存在上述的精化关系。下面对精化关系中的常见性质进行讨论。

性质1：（交换律）令AD=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞为一个活动图并且ref 表示精化函数。对于∀x,y∈AO,有ref（x）=＜Ax,AOx,Dnx,Mnx,Fnx,Jnx,Rx,Iax,Fax＞和ref（y）=＜Ay,AOy,Dny,Mny,Fny,Jny,Ry,Iay,Fay＞,当AOx∩AOy∩AO=Ø,则有（AD[x/ref（x）]）[y/ref（y）]=（AD[y/ref（y）]）[x/ref（x）]。

对于一个活动图AD 而言,如果存在任意两个活动节点,都存在有与其对应的活动图,可以替换原活动图中的对应节点,那么两次替换交换顺序后,最后得到的精化后的活动图都是同样的。基于定义2 和定义3,可以很简单的证明该性质成立,则本文中省去该性质的形式化证明过程。

需要注意的是,对于精化关系,传递性不一定成立。即如果对 于 三 个 活 动 图AD1=＜A1,AO1,Dn1,Mn1,Fn1,Jn1,R1,Ia1,Fa1＞,AD2=＜A2,AO2,Dn2,Mn2,Fn2,Jn2,R2,Ia2,Fa2＞ 和 AD3=＜A3,AO3,Dn3,Mn3,Fn3,Jn3,R3,Ia3,Fa3＞。如 果 三 者 间 满 足AD2＞AD1且AD3＞AD2,但AD3＞AD1不一定成立。下面分别分两种情况讨论,当存在x∈AO1,使得AD2=AD1[x/ref（x）]时,

（1）如果存在y∈AO1 {x},使得AD3=AD2[y/ref（y）],则AD3＞AD1成立。

（2）如果存在y∈AOx（其中ref（x）=＜Ax,AOx,Dnx,Mnx,Fnx,Jnx,Rx,Iax,Fax＞）,使得AD3=AD2[y/ref（y）],则AD3＞AD1不成立。

也就是说,如果AD3是AD1的精化,那么其充要条件是,存在x,y∈AO1（x≠y）,使得AD3=（AD1[x/ref（x）]）[y/ref（y）]或AD3=（AD1[y/ref（y）]）[x/ref（x）]（两者等价,参照性质1）。

性质2：令AD=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞为一个活动图并且ref 表示精化函数。对于∀x∈AO 如果AD 和ref（x）内均无死锁,则AD[x/ref（x）]内也不存在死锁。

该性质显然成立。在开发过程中,如果原版本内无死锁,且新开发的模块内部也没有死锁,那么替换之后的精化版本的正确性也得到了保障。

4 结论

增量开发中的活动图精化研究主要是以增量开发为背景,研究活动图的形式语义,精化过程及精化关系的一些性质。本文基于形式化方法给出了一套完整的理论框架,给出了活动图的模型及模型间的精化操作。未来工作则主要集中于如何验证精化前后两个不同的活动图之间的一致性关系。