龔潔靜 ，張廣泉 ，肖剛

0 引言

需求工程出現(xiàn)于上個世紀80年代中期，目前已發(fā)展成為軟件工程的一個獨立研究分支。需求獲取技術是需求工程中一個非常重要的研究內容。如何用適當?shù)姆椒?，把軟件需求詳細精確地描述出來，這不僅影響著開發(fā)人員之間，對軟件系統(tǒng)的理解和的交流，更影響到最終軟件產品的成敗，尤其是在安全悠關系統(tǒng)的開發(fā)中。

目前主流的軟件需求描述方法有兩類：自然語言描述和半形式化描述，自然語言描述是目前工程實踐中使用的主要方法，半形式化描述以UML/OCL為代表。自然語言存在著二義性和不一致性等缺陷，而UML/OCL的建模元素，同樣缺乏精確的形式化語義，也不可避免地產生多義性，盡管輔之以OCL可以在一定程度上減少歧義性，但仍不能從根本上解決UML需求模型歧義性的問題。以這兩類方法為基礎的軟件需求描述和構造過程，往往潛藏著大量的錯誤和缺陷，錯誤在一定程度上可以依靠測試來解決，軟件需求中的缺陷，測試是無能為力的。形式化方法作為一種以數(shù)學為基礎的方法，能夠清晰、精確、抽象、簡明地描述和驗證軟件系統(tǒng)及其性質，能夠發(fā)現(xiàn)軟件需求中的缺陷，極大地提高軟件的安全性和可靠性，但在需求獲取過程中，尚無形式化方法成功應用的案例。

1 公平離散系統(tǒng)模型

在需求構建過程中，離散系統(tǒng)模型是對問題系統(tǒng)的抽象，在實現(xiàn)過程中，離散系統(tǒng)模型是對程序的抽象（它的語義等價于轉移系統(tǒng)模型），離散系統(tǒng)應能很好的描述系統(tǒng)或程序的性質，通過前面的討論知道，離散系統(tǒng)模型應能描述系統(tǒng)和程序的安全性和活性。對于并發(fā)系統(tǒng)、反應系統(tǒng)和分布系統(tǒng)，離散系統(tǒng)模型還應能準確地描述系統(tǒng)事件被選中執(zhí)行的方式，即離散系統(tǒng)模型應能準確地描述系統(tǒng)事件之間的公平性。

通過前面的描述，可以對基本離散系統(tǒng)模型作如下擴充，作為軟件開發(fā)過程中使用的統(tǒng)一框架模型，公平離散系統(tǒng)模型包含如下幾個組成部分：狀態(tài)變量的集合、狀態(tài)變量定義域和常量的集合、狀態(tài)之間的轉移的集合、初始化條件的集合、公平約束的集合。用符號 FDSM（U，V，INIT，T,MP,WF,SF）,下面就說明一下這幾個符號的意義（約定本文用FDSM表示公平離散系統(tǒng)模型）

U＝{u1,u2,．．．．．un}模型內一組有窮的狀態(tài)變量的集合，針對有限狀態(tài)系統(tǒng)，所有的狀態(tài)變量定義域是有限的。無窮狀態(tài)系統(tǒng)狀態(tài)變量的取值范圍是無限的。本文僅討論有窮狀態(tài)系統(tǒng)，狀態(tài)變量的類型，一定要和其定義域中的元素的類型一致。假設在一個狀態(tài)s上給狀態(tài)變量u賦值的形式是s[u] 。用U代表整個系統(tǒng)的狀態(tài)空間。

V＝{v1,v2,……vn}是狀態(tài)變量定義域及常量的集合，表示整個狀態(tài)變量的取值范圍和在這模型中所必需的常量。

INIT是模型的初始條件的集合，這些條件定義出所有FDSM 的初始狀態(tài)，如果一個狀態(tài)滿足條件 INIT，那么就稱其為初始狀態(tài)。

T―模型中事件的集合，如果一個事件t∈T,那么一定有ρt?V×V，ρt表示從一個狀態(tài)到另一個狀態(tài)之間的轉移。

MP＝{m1,m2,……,mn}是 MP公平的集合,其中 mi∈T,直觀的解釋如果 m?MP,在一定的狀態(tài)下 m中的事件的衛(wèi)條件為真，那么一定有部分的事件發(fā)生，且轉移到下一個狀態(tài)。

WF＝{w1,w2,……,wn}是弱公平的集合，其中wi∈T，直觀的解釋如下：如果在模型的一個無窮計算序列中wi的衛(wèi)條件一直為真，那么在這個計算序列中wi一定能被無限多次選中運行。

SF＝{s1,s2,……,sn}是弱公平的集合，其中 si∈T,直觀的解釋如下：如果模型中的無窮計算序列中 si的衛(wèi)條件無窮多次為真，那么在這個計算序列中 si一定能被無限多次的選中運行。

一個公平離散系統(tǒng)模型所有的計算序列必需滿足以下幾個條件：

(1) 初始化 s0是初始狀態(tài)，那么 s0一定是滿足條件INIT的狀態(tài)之一。

(2) 連續(xù)性

公平離散系統(tǒng)模型中事件的發(fā)生是非確定，事件發(fā)生方式受到公平性的約束，在一個狀態(tài)下可能多個事件的衛(wèi)條件均為真，最終是那一個事件發(fā)生是不確定。當所有事件的衛(wèi)條件均為真時，不能確定那些事件真實的執(zhí)行。公平離散系統(tǒng)模型的可終止性不是必需的。事實上用這個模型研究的系統(tǒng)大多數(shù)都是不終止的，比如鍋爐控制系統(tǒng)、核電廠控制系統(tǒng)。

2 需求獲取過程中復雜性控制方法

利用公平離散系統(tǒng)模型構建系統(tǒng)需求模型是一個步進的過程，在構建系統(tǒng)的需求時，首先開始構建一個最簡單的系統(tǒng)模型，這個模型只具備一些大粒度的事件，驗證最初的模型。驗證完成之后，在個模型的基礎上，進一步考察系統(tǒng)對獲得的需求，在驗證中擴充。這個過程和從規(guī)約到程序的過程有點類似，仿造從規(guī)約到程序演化過程的概念，把這過程也稱之為求精。求精之后的需求更接近實際系統(tǒng)，需求求精過程和規(guī)約的演化過程有本質的區(qū)別，在規(guī)約到程序的演化過程中，涉及到數(shù)據(jù)類型和語言概念上的變化，而在需求的獲取過程中數(shù)據(jù)類型是一致的，且不存在語言概念上的變化，在需求求精過程中使用的語言是完全相同。更直觀的講，需求的求精過程有點類似于觀察一個事物，當距離較遠時，看到的系統(tǒng)的特征較大，能看見的系統(tǒng)的行為很少，當距離近一些時，看到的特征粒度就會小些，能看見的系統(tǒng)行為就比之前多些，這樣逐步拉近和觀察事物的距離，看到的細節(jié)就越來越多，直到最終獲取所觀察事物的所有細節(jié)，在這個觀察的過程中，使用方法和借助的工具均是相同的。

在需求的求精過程中，隨著觀察系統(tǒng)的細節(jié)越來越多，獲得的系統(tǒng)需求模型在空間量和時序量上均有擴張，空間量上的擴張表現(xiàn)為系統(tǒng)狀態(tài)的增多，因為求精后更接近實際系統(tǒng)，故求精后的系統(tǒng)的需求模型的狀態(tài)肯定多于求精前。隨著狀態(tài)的增加，狀態(tài)之間的事件亦隨之增多，許多事件在抽象模型中是看不見的，因為新事件在抽象模型中不存在，故新事件不能修改從抽象模型中繼承的狀態(tài)變量，新事件可以引用原有變量，但僅能修改新引入的狀態(tài)變量。需求的求精就是在更細粒度的空間和時序下觀察系統(tǒng)，時序量的擴張表現(xiàn)在隨著系統(tǒng)狀態(tài)增多和事件的增多。需求求精過程和從規(guī)約到程序的求精過程一樣，包含：操作求精和數(shù)據(jù)求精，不過這兩類求精的表現(xiàn)完全不同。數(shù)據(jù)求精在后者中設計的數(shù)據(jù)類型和數(shù)據(jù)表述方式的變化，可能與求精前后使用的數(shù)據(jù)類型和數(shù)據(jù)的表述方式完全不同，而數(shù)據(jù)求精在前者中，只是增加或減少變量來表述系統(tǒng)的行為，兩者的語言相同類型相同，可能在特定場合中也有數(shù)據(jù)類型的變化，但求精前后表述的語句的語法方式是完全相同的。操作求精在兩者中也有區(qū)別，在后者中求精越來越接近程序設計語言，從最初的抽象規(guī)約到程序兩者的描述體系與語法完全不同，而需求求精只是在操作中增加更多的描述細節(jié)，而不改變原有變量的類型和值及數(shù)據(jù)表述方式，最初的需求模型和最終的需求模型，在描述體系和語法上完全相同。

需求求精和從規(guī)約到程序的演化過程相同，為了保證求精前后的一致性和完備性，在需求求精過程中，也必需對求精前后的需求模型進行驗證。需求模型求精過程中首先要驗證的是：一是求精過程中需要保持的性質，二是新增事件有關性質的驗證。在第一點關于求精前后的需求模型需要驗證：

(1) 抽象模型中的狀態(tài)在具體需求模型中均可找到其對應的狀態(tài)，當然在具體模型中可能有多個具體狀態(tài)對應與抽象模型中的狀態(tài)。

(2) 抽象模型和具體模型具有相同的死鎖性和可終止性。

(3) 抽象模型和具體模型公平的一致性。

(4) 外部事件的不變性。

第二點中必需驗證如下幾方面：

(1) 新增事件安全性的驗證。這包括新引入事件的可行性、操作不變性、無死鎖性等等。

(2) 新增事件公平下活性的驗證，這包括無活鎖、可終止性。

通過這兩方面的驗證，基本上可以保證需求模型求精的正確性和一致性。

在獲取需求模型的過程中，隨著求精步驟的增加，模型中事件和狀態(tài)變量會大量的增加，當?shù)竭_一定數(shù)量時，模型的控制就變得非常的困難，繼續(xù)利用原模型求精會變得極為復雜和難以處理，這時為了降低模型的復雜度，使模型在求精過程中容易控制，可以借用結構化的分解原理多模型進行分解，把復雜的模型分解成幾個較為容易控制的小模型，分解的原則是模塊化，高內聚和低耦合（在后面的章節(jié)會給出具體的分解算法），模型分解后各個子模型相互之間沒有依賴關系，可以單獨的求精驗證。在分解的過程中應驗證相關的性質，應特別注意特定公平下活性的驗證。分解得到的子模型應是可復原的，可以通過組合這幾個子模型構造出的復合模型應和原模型一致。

3 需求模型復用

在程序的開發(fā)方法尤其是面向對象的開發(fā)方法中，復用在整個方法學中占有很重要的地位，同樣在基于公平離散系統(tǒng)框架下，構造系統(tǒng)需求模型的方法中，也引入復用的概念。在這個方法中，復用第一種情況是可以從別的系統(tǒng)需求模型中，引用與本系統(tǒng)需求有關的需求模型，甚至是整個系統(tǒng)的需求模型。第二種情況是，可以把一些公用的系統(tǒng)或子系統(tǒng)的需求模型模板化，把與業(yè)務邏輯無關的數(shù)據(jù)從需求模型中分離出去。在需要用到時只須給模板賦以具體的參數(shù)，就可實例化出不同業(yè)務系統(tǒng)的需求模型。因為模板模型在構造時已經對其進行了推理驗證，引用到具體的需求中時就不需對其進行驗證，因此引用模板和引用其他需求模型中，已證明的模型可以大量節(jié)約構建系統(tǒng)需求模型的時間。

4 小結

本文在回顧相關概念后，提出了可以適用于軟件生命周期所有階段的模型－公平離散系統(tǒng)模型，并給出了初步的形式化的定義，非形式化地描述了公平離散系統(tǒng)模型，在需求獲取過程中的相關性質的驗證及控制模型復雜性的方法、需求復用。

[1] Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurent Systems Specification [M] . Springer-Verlag New York, INC. 1992.

[2] Manna Z, Pnueli A. Temporal Verification of Reactive Systems [M] . Springer-Verlag New York, INC. 1995.

[3] Back R J R, Xu Q W. Fairness in Action Systems[R] .Technical Report No159,Abo Akademi,Finland,1995.

[4] Back R J R, Xu Q W. Refinement of fair action systems[J] . Acta Informatica ,1998,35:131-165.

[5] Lamport L. The Temporal Logic of Actions [J] . ACM Transactions on Programming Languages and Systems,1994, 16(3):872-923.

[6] L amport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers [M] .Addison-Wesley, 2003.

[7] J.M. Spivey. The Z Notation: A Reference Manual Second Edition [M] . Prentice Hall International (UK) Ltd,1992.