文浩

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

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

增量開發(fā)中最主要的操作之一就是精化（refinement）。精化是對于軟件中的某一具體功能進(jìn)行進(jìn)一步的開發(fā),即使原來的功能更加具體。例如對于一個(gè)ATM機(jī)而言,如果初始系統(tǒng)中的取款功能僅僅是根據(jù)用戶輸入的金額,進(jìn)行出鈔,那么當(dāng)用戶輸入的金額超出ATM里剩余的金額總量,就可能會出現(xiàn)問題,或者當(dāng)用戶需要在出鈔的同時(shí),打印賬單,那么原系統(tǒng)也是無法做到的。此時(shí)就可以對原系統(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ù)流,并且可以清晰地描述每個(gè)活動的執(zhí)行順序。相比于類似的狀態(tài)圖,活動圖可以簡要地描述并發(fā)并且不用區(qū)分全局或者局部的狀態(tài),所以在建模復(fù)雜系統(tǒng)時(shí),活動圖是一種更優(yōu)的選擇。本文中,我們除了給出了活動圖的形式語義,還對活動圖間的精化過程進(jìn)行了形式化表達(dá),并且討論了一些重要的性質(zhì)。

對于活動圖的研究由來以及,但之前的一些研究因?yàn)槿狈π问交椒ǖ闹?導(dǎo)致其可靠性和正確性難以保證,從而無法應(yīng)用于實(shí)際開發(fā)中。形式化方法是基于嚴(yán)格數(shù)學(xué)基礎(chǔ),對計(jì)算機(jī)軟（硬）件系統(tǒng)進(jìn)行形式規(guī)約、開發(fā)和驗(yàn)證的技術(shù)[4]。其中,形式驗(yàn)證是證明不同形式規(guī)約之間的邏輯關(guān)系,這些邏輯關(guān)系反映了處在不同開發(fā)階段的軟件的各類正確性需求。所以,結(jié)合增量開發(fā)的背景,適當(dāng)?shù)氖褂眯问交椒梢源_保最終產(chǎn)品的可靠性、安全性。特別是對于正確性而言,雖然軟件中的一些錯(cuò)誤可以被傳統(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í)行過程?；顒訄D的節(jié)點(diǎn)可以分為活動節(jié)點(diǎn)、控制節(jié)點(diǎn)和對象節(jié)點(diǎn)。本文為了簡化表達(dá),將對象節(jié)點(diǎn)也視為活動節(jié)點(diǎn)。

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

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

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

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

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

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

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

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

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

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

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

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

此外,為了方便后續(xù)對精化過程的討論,我們對于任意x∈A,將其前置集記為

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

下面給出一個(gè)具體的例子用于解釋上述定義。

例1：圖1 是一個(gè)活動圖,可以表示為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,我們得知,可以通過上述的方法簡單明了地表示一個(gè)活動圖。

圖1 一個(gè)活動圖的實(shí)例

2 活動圖間的精化

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

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

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

定義2：AD=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞是一個(gè)活動圖。其中存在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。

下面給出一個(gè)具體的例子用于解釋定義2,例2 中的AD1和AD2分別見圖2（a）（b）。

例2：對于圖1 中的活動圖AD,存在活動節(jié)點(diǎn)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)兩個(gè)活動圖的形式語義滿足定義2,則稱這兩個(gè)活動圖間存在精化關(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＞為兩個(gè)活動圖并且ref 表示精化函數(shù),當(dāng)且僅當(dāng)存在x∈AO1,使得AD2=AD1[x/ref（x）],則稱AD2是AD1的精化,記作AD2＞AD1。

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

性質(zhì)1：（交換律）令A(yù)D=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞為一個(gè)活動圖并且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）]。

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

需要注意的是,對于精化關(guān)系,傳遞性不一定成立。即如果對 于 三 個(gè) 活 動 圖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）]時(shí),

（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）]（兩者等價(jià),參照性質(zhì)1）。

性質(zhì)2：令A(yù)D=＜A,AO,Dn,Mn,Fn,Jn,R,Ia,Fa＞為一個(gè)活動圖并且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ì)。本文基于形式化方法給出了一套完整的理論框架,給出了活動圖的模型及模型間的精化操作。未來工作則主要集中于如何驗(yàn)證精化前后兩個(gè)不同的活動圖之間的一致性關(guān)系。