增量開發中的活動圖精化研究

文浩

（福建師范大學,福建 福州350007）

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

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

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

對于活動圖的研究由來以及,但之前的一些研究因為缺乏形式化方法的支撐,導致其可靠性和正確性難以保證,從而無法應用于實際開發中。形式化方法是基于嚴格數學基礎,對計算機軟（硬）件系統進行形式規約、開發和驗證的技術[4]。其中,形式驗證是證明不同形式規約之間的邏輯關系,這些邏輯關系反映了處在不同開發階段的軟件的各類正確性需求。所以,結合增量開發的背景,適當的使用形式化方法可以確保最終產品的可靠性、安全性。特別是對于正確性而言,雖然軟件中的一些錯誤可以被傳統的軟件測試方法發現,但是對于人工上難以察覺潛在的軟件缺陷,只能通過嚴謹的數學方法來發現及解決。所以本文中對于形式化方法的引用也是極其有必要的。

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

1 活動圖的形式語義

活動圖在視覺上的呈現類似于流程圖或數據流程圖。但與這些不同的是,活動圖在建模工作流或模擬業務流程上有更出色的表現[3]。它可以建模順序的,并發的以及選擇的活動,并且基于開始（初始狀態）和結束（最終狀態）來描述活動的執行過程?；顒訄D的節點可以分為活動節點、控制節點和對象節點。本文為了簡化表達,將對象節點也視為活動節點。

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

定義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 而言,如果存在任意兩個活動節點,都存在有與其對應的活動圖,可以替換原活動圖中的對應節點,那么兩次替換交換順序后,最后得到的精化后的活動圖都是同樣的?；诙x2 和定義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 結論

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