龔潔靜 ，張廣泉 ，肖剛

0 引言

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(2) 連續(xù)性

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

2 需求獲取過程中復(fù)雜性控制方法

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

在需求的求精過程中，隨著觀察系統(tǒng)的細(xì)節(jié)越來越多，獲得的系統(tǒng)需求模型在空間量和時(shí)序量上均有擴(kuò)張，空間量上的擴(kuò)張表現(xiàn)為系統(tǒng)狀態(tài)的增多，因?yàn)榍缶蟾咏鼘?shí)際系統(tǒng)，故求精后的系統(tǒng)的需求模型的狀態(tài)肯定多于求精前。隨著狀態(tài)的增加，狀態(tài)之間的事件亦隨之增多，許多事件在抽象模型中是看不見的，因?yàn)樾率录诔橄竽Ｐ椭胁淮嬖?，故新事件不能修改從抽象模型中繼承的狀態(tài)變量，新事件可以引用原有變量，但僅能修改新引入的狀態(tài)變量。需求的求精就是在更細(xì)粒度的空間和時(shí)序下觀察系統(tǒng)，時(shí)序量的擴(kuò)張表現(xiàn)在隨著系統(tǒng)狀態(tài)增多和事件的增多。需求求精過程和從規(guī)約到程序的求精過程一樣，包含：操作求精和數(shù)據(jù)求精，不過這兩類求精的表現(xiàn)完全不同。數(shù)據(jù)求精在后者中設(shè)計(jì)的數(shù)據(jù)類型和數(shù)據(jù)表述方式的變化，可能與求精前后使用的數(shù)據(jù)類型和數(shù)據(jù)的表述方式完全不同，而數(shù)據(jù)求精在前者中，只是增加或減少變量來表述系統(tǒng)的行為，兩者的語言相同類型相同，可能在特定場(chǎng)合中也有數(shù)據(jù)類型的變化，但求精前后表述的語句的語法方式是完全相同的。操作求精在兩者中也有區(qū)別，在后者中求精越來越接近程序設(shè)計(jì)語言，從最初的抽象規(guī)約到程序兩者的描述體系與語法完全不同，而需求求精只是在操作中增加更多的描述細(xì)節(jié)，而不改變?cè)凶兞康念愋秃椭导皵?shù)據(jù)表述方式，最初的需求模型和最終的需求模型，在描述體系和語法上完全相同。

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

(1) 抽象模型中的狀態(tài)在具體需求模型中均可找到其對(duì)應(yīng)的狀態(tài)，當(dāng)然在具體模型中可能有多個(gè)具體狀態(tài)對(duì)應(yīng)與抽象模型中的狀態(tài)。

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

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

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

第二點(diǎn)中必需驗(yàn)證如下幾方面：

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

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

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

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

3 需求模型復(fù)用

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

4 小結(jié)

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

[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.