文浩

（福建師范大學(xué),福建 福州350007）

增量模型在軟件開發(fā)過程中被廣泛使用。開發(fā)人員根據(jù)客戶的反饋和需求,對軟件進(jìn)行不斷的迭代,并且在當(dāng)前的版本基礎(chǔ)上進(jìn)行增量開發(fā),以此作為下次交付的新版本。與一些經(jīng)典模型相比,增量模型結(jié)合了瀑布模型的基本組成部分與原型模型的迭代特征,將復(fù)雜的系統(tǒng)分解為一個一個的小模塊,再逐步進(jìn)行處理[1,2]。當(dāng)開發(fā)人員面臨一些軟件開發(fā)中的常見問題時,例如因為某些因素,需要回到軟件先前的某個版本,我們就會因為逐步開發(fā)的策略,從而很好地解決這些問題。因此,迭代的增量模型在軟件開發(fā)過程中是不可或缺的。

增量開發(fā)中最主要的操作之一就是精化（refinement）。精化是對于軟件中的某一具體功能進(jìn)行進(jìn)一步的開發(fā),即使原來的功能更加具體。例如對于一個ATM機(jī)而言,如果初始系統(tǒng)中的取款功能僅僅是根據(jù)用戶輸入的金額,進(jìn)行出鈔,那么當(dāng)用戶輸入的金額超出ATM里剩余的金額總量,就可能會出現(xiàn)問題,或者當(dāng)用戶需要在出鈔的同時,打印賬單,那么原系統(tǒng)也是無法做到的。此時就可以對原系統(tǒng)的取款功能進(jìn)行精化,從而達(dá)到客戶的需求。

本文選擇使用UML 中的活動圖對系統(tǒng)進(jìn)行建模,描述軟件開發(fā)中的增量過程。UML 是一種復(fù)雜的可視化語言,其中有14種不同的圖表類型,具體又可以分為結(jié)構(gòu)和行為兩種大類[3]?；顒訄D是行為圖中的一種,它可以體現(xiàn)軟件系統(tǒng)的控制流和數(shù)據(jù)流,并且可以清晰地描述每個活動的執(zhí)行順序。相比于類似的狀態(tài)圖,活動圖可以簡要地描述并發(fā)并且不用區(qū)分全局或者局部的狀態(tài),所以在建模復(fù)雜系統(tǒng)時,活動圖是一種更優(yōu)的選擇。本文中,我們除了給出了活動圖的形式語義,還對活動圖間的精化過程進(jìn)行了形式化表達(dá),并且討論了一些重要的性質(zhì)。

對于活動圖的研究由來以及,但之前的一些研究因為缺乏形式化方法的支撐,導(dǎo)致其可靠性和正確性難以保證,從而無法應(yīng)用于實際開發(fā)中。形式化方法是基于嚴(yán)格數(shù)學(xué)基礎(chǔ),對計算機(jī)軟（硬）件系統(tǒng)進(jìn)行形式規(guī)約、開發(fā)和驗證的技術(shù)[4]。其中,形式驗證是證明不同形式規(guī)約之間的邏輯關(guān)系,這些邏輯關(guān)系反映了處在不同開發(fā)階段的軟件的各類正確性需求。所以,結(jié)合增量開發(fā)的背景,適當(dāng)?shù)氖褂眯问交椒梢源_保最終產(chǎn)品的可靠性、安全性。特別是對于正確性而言,雖然軟件中的一些錯誤可以被傳統(tǒng)的軟件測試方法發(fā)現(xiàn),但是對于人工上難以察覺潛在的軟件缺陷,只能通過嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)方法來發(fā)現(xiàn)及解決。所以本文中對于形式化方法的引用也是極其有必要的。

本文的結(jié)構(gòu)如下：本文第1 節(jié)對活動圖進(jìn)行了建模。第2 節(jié)基于活動圖的模型,提出了精化過程的形式化表達(dá)。第3 節(jié)定義了精化關(guān)系并且討論了精化關(guān)系的常見性質(zhì)。最后總結(jié)全文,并對未來的研究方向進(jìn)行初步探討。

1 活動圖的形式語義

活動圖在視覺上的呈現(xiàn)類似于流程圖或數(shù)據(jù)流程圖。但與這些不同的是,活動圖在建模工作流或模擬業(yè)務(wù)流程上有更出色的表現(xiàn)[3]。它可以建模順序的,并發(fā)的以及選擇的活動,并且基于開始（初始狀態(tài)）和結(jié)束（最終狀態(tài)）來描述活動的執(zhí)行過程。活動圖的節(jié)點可以分為活動節(jié)點、控制節(jié)點和對象節(jié)點。本文為了簡化表達(dá),將對象節(jié)點也視為活動節(jié)點。

下面給出了活動圖的形式語義。

定義1：一個活動圖是一個九元組AD=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞,其中

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

AO,活動節(jié)點和對象節(jié)點的集合,

Dn,選擇節(jié)點的集合,

Mn,合并節(jié)點的集合,

Fn,分叉節(jié)點的集合,

Jn,匯合節(jié)點的集合,

R?A×A,活動和節(jié)點間關(guān)系的集合,

Ia,初始節(jié)點的集合,

Fa,終止節(jié)點的集合。

集合A 中存放的是活動圖中的所有節(jié)點和邊,R 則是定義在A 上的關(guān)系,其中的元素是A 通過自身的笛卡爾積所得到的序偶。上述的定義可參照我們之前的一些工作[5,6,7]。

此外,為了方便后續(xù)對精化過程的討論,我們對于任意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 活動圖間的精化

在軟件開發(fā)的初期,因為需求不清等諸多因素,開發(fā)人員往往是根據(jù)個人經(jīng)驗對系統(tǒng)進(jìn)行建模,這就導(dǎo)致最初的模型處于一個高抽象的層次,即該模型往往存在功能缺失或?qū)崿F(xiàn)功能不明確等等問題,那么隨著需求的逐漸清晰,軟件的功能也需要逐漸完善。而精化,也正就是使得高抽象系統(tǒng)不斷具體化的一種操作[8]。

為了形式化的表達(dá)活動圖的精化過程,本文首先給出了一個精化函數(shù)。設(shè)AO 為活動節(jié)點的集合,AD 為活動圖的集合,稱ref：AO→AD-{?}為“精化函數(shù)”。

簡單來說,活動圖間的精化過程就是對于初始的活動圖,選擇該圖中的某一個或者某些活動節(jié)點,再用與這些活動節(jié)點一一對應(yīng)的活動圖替換之前的節(jié)點。下面是精化過程的定義。

定義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=?。

那么經(jīng)過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,存在活動節(jié)點c∈AO。令A(yù)D1=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 精化關(guān)系的性質(zhì)

第一章中介紹了活動圖的形式語義,第二章則給出了活動圖間的精化方法。基于上述內(nèi)容,我們可以簡單的概括,當(dāng)兩個活動圖的形式語義滿足定義2,則稱這兩個活動圖間存在精化關(guān)系,下面給出形式化的表達(dá)。

定義3：令A(yù)D1=＜A1,AO1,Dn1,Mn1,Fn1,Jn1,R1,Ia1,Fa1＞和AD2=＜A2,AO2,Dn2,Mn2,Fn2,Jn2,R2,Ia2,Fa2＞為兩個活動圖并且ref 表示精化函數(shù),當(dāng)且僅當(dāng)存在x∈AO1,使得AD2=AD1[x/ref（x）],則稱AD2是AD1的精化,記作AD2＞AD1。

由定義3 和例2 可知,圖2（b）和圖1 中的兩個活動圖間存在上述的精化關(guān)系。下面對精化關(guān)系中的常見性質(zhì)進(jìn)行討論。

性質(zhì)1：（交換律）令A(yù)D=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞為一個活動圖并且ref 表示精化函數(shù)。對于?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＞,當(dāng)AOx∩AOy∩AO=?,則有（AD[x/ref（x）]）[y/ref（y）]=（AD[y/ref（y）]）[x/ref（x）]。

對于一個活動圖AD 而言,如果存在任意兩個活動節(jié)點,都存在有與其對應(yīng)的活動圖,可以替換原活動圖中的對應(yīng)節(jié)點,那么兩次替換交換順序后,最后得到的精化后的活動圖都是同樣的?；诙x2 和定義3,可以很簡單的證明該性質(zhì)成立,則本文中省去該性質(zhì)的形式化證明過程。

需要注意的是,對于精化關(guān)系,傳遞性不一定成立。即如果對 于 三 個 活 動 圖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不一定成立。下面分別分兩種情況討論,當(dāng)存在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）]（兩者等價,參照性質(zhì)1）。

性質(zhì)2：令A(yù)D=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞為一個活動圖并且ref 表示精化函數(shù)。對于?x∈AO 如果AD 和ref（x）內(nèi)均無死鎖,則AD[x/ref（x）]內(nèi)也不存在死鎖。

該性質(zhì)顯然成立。在開發(fā)過程中,如果原版本內(nèi)無死鎖,且新開發(fā)的模塊內(nèi)部也沒有死鎖,那么替換之后的精化版本的正確性也得到了保障。

4 結(jié)論

增量開發(fā)中的活動圖精化研究主要是以增量開發(fā)為背景,研究活動圖的形式語義,精化過程及精化關(guān)系的一些性質(zhì)。本文基于形式化方法給出了一套完整的理論框架,給出了活動圖的模型及模型間的精化操作。未來工作則主要集中于如何驗證精化前后兩個不同的活動圖之間的一致性關(guān)系。