第11章凈室軟件工程基本概念凈室策略功能規(guī)格說明凈室設(shè)計凈室測試認(rèn)證11.1基本概念凈室軟件工程(Cleanroomsoftwareengineering)是一種在軟件開發(fā)過程中強調(diào)在軟件中建立正確性要求的方法。與傳統(tǒng)的分析、設(shè)計、編碼、測試和調(diào)試的周期觀點有所不同。凈室方法的觀點：

通過在第一次正確地書寫代碼增量，并在測試前驗證它們的正確性來避免成本很高的缺陷消除過程。它的過程模型是在代碼增量集成到系統(tǒng)的同時，進行代碼增量的統(tǒng)計質(zhì)量驗證。11.1基本概念與形式化方法技術(shù)一樣，凈室過程強調(diào)規(guī)格說明和設(shè)計上的嚴(yán)格性，并且使用基于數(shù)學(xué)的正確性證明來對結(jié)果設(shè)計模型的每個元素進行形式化驗證。凈室方法不是先制造一個產(chǎn)品，然后再去消除缺陷，而是要求在規(guī)格說明和設(shè)計中消除錯誤，然后以“干凈”的方式進行制造。凈室方法還對形式化方法進行了擴展，強調(diào)統(tǒng)計質(zhì)量控制技術(shù)，包括基于客戶對軟件的預(yù)期使用的測試。11.1基本概念“第一次就將事情做正確”是軟件工程最重要的哲學(xué)。凈室軟件工程是這樣一個過程：它強調(diào)在程序構(gòu)造開始前進行正確性的數(shù)學(xué)驗證，并且將軟件可靠性認(rèn)證作為軟件測試的一部分。其底線是極低的故障率，這是使用非形式化方法難于或不可能達到的。11.1基本概念20世紀(jì)80年代，Mills、Dyer、及Linger最先建議將凈室原理應(yīng)用于軟件工程。雖然在軟件開發(fā)的早期，人們對其抱以很大的希望，但它并沒有得到廣泛的使用。

11.1基本概念

Henderson提出了沒有得到廣泛使用的三個原因：

1.凈室方法學(xué)太理論化、太數(shù)學(xué)化、太激進，難于在實際的軟件開發(fā)中使用。

2.它提倡開發(fā)者不需要進行單元測試，而是進行正確性驗證和統(tǒng)計質(zhì)量控制，這些觀念與當(dāng)前大多數(shù)軟件開發(fā)方式有很大的偏離。11.1基本概念3.軟件開發(fā)產(chǎn)業(yè)的成熟度不高。使用凈室過程需要在整個生命周期階段嚴(yán)格按照定義的過程進行。由于大多數(shù)軟件企業(yè)的運作還處于過程成熟度中的較低級別，軟件工程師還沒有準(zhǔn)備應(yīng)用凈室技術(shù)。11.1基本概念“程序中出現(xiàn)錯誤的唯一方式是作者將錯誤引入進去的。沒有其他方式……正確實踐的目標(biāo)是：設(shè)法避免引入錯誤，如果引入了錯誤，通過測試或任何其他運行程序的方式來消除錯誤?！?/p>

HarlanMills11.1基本概念11.2凈室策略凈室方法使用增量過程模型。一個“軟件增量的流水線”由若干小的、獨立的軟件團隊開發(fā)。每當(dāng)一個軟件增量通過認(rèn)證，它就被集成到整體系統(tǒng)中。因此，系統(tǒng)的功能隨時間增加。

一旦將功能分配給系統(tǒng)的軟件元素，則可啟動凈室增量的流水線。需要完成的任務(wù)如下：

(1)增量策劃。制定一個采用增量策略的項目計劃，確定每個增量的功能、預(yù)計規(guī)模、及凈室開發(fā)進度。

(2)需求收集。為每個增量開發(fā)更詳細(xì)的客戶級需求描述。

11.2凈室策略(3)盒結(jié)構(gòu)規(guī)格說明。運用盒結(jié)構(gòu)的規(guī)格說明方法描述功能規(guī)格說明。遵從操作分析原則，盒結(jié)構(gòu)“在每一個精化級別上使行為、數(shù)據(jù)及過程的創(chuàng)造性定義獨立”。(4)形式化設(shè)計。使用盒結(jié)構(gòu)方法，凈室設(shè)計是規(guī)格說明的自然、無縫擴展。對規(guī)格說明(稱為黑盒)進行迭代求精(在一個增量內(nèi))類似于體系結(jié)構(gòu)設(shè)計和構(gòu)件級設(shè)計(分別稱為“狀態(tài)盒”和“清晰盒”)。

11.2凈室策略

(5)正確性驗證。凈室團隊對設(shè)計及代碼進行一系列嚴(yán)格的正確性驗證活動。驗證從最高層次的盒結(jié)構(gòu)(規(guī)格說明)開始，然后移向設(shè)計細(xì)節(jié)和代碼。正確性驗證的第一層次通過應(yīng)用一組“正確性問題”來進行，如果這些沒有證明規(guī)格說明是正確的，則使用更形式化的(數(shù)學(xué)的)驗證方法。

11.2凈室策略(6)代碼生成、檢查和驗證。以某種專門語言表示的盒結(jié)構(gòu)規(guī)格說明被翻譯為適當(dāng)?shù)某绦蛟O(shè)計語言。然后，使用標(biāo)準(zhǔn)的走查或檢查技術(shù)來保證代碼和盒結(jié)構(gòu)的語義相符性，以及代碼的語法正確性。最后，對源代碼進行正確性驗證。

11.2凈室策略(7)統(tǒng)計測試規(guī)劃。分析軟件的預(yù)計使用情況，規(guī)劃并設(shè)計一組測試用例，以測試使用情況的“概率分布”

。

11.2凈室策略

(8)統(tǒng)計使用測試。對計算機軟件進行窮舉測試是不可能的，因此，設(shè)計有限數(shù)量的測試用例總是必要的。統(tǒng)計使用技術(shù)執(zhí)行由統(tǒng)計樣本導(dǎo)出的一系列測試，這里的統(tǒng)計樣本是從來自目標(biāo)人群的所有用戶對程序的所有可能執(zhí)行中抽取的。11.2凈室策略

(9)認(rèn)證。一旦完成驗證、檢查和使用測試(并且所有錯誤被改正)，則對增量進行集成前的認(rèn)證工作。

11.2凈室策略凈室方法的特異之處

明確使用統(tǒng)計質(zhì)量控制。使用基于數(shù)學(xué)的正確性證明來驗證設(shè)計規(guī)格說明。實現(xiàn)了一些測試技術(shù)，這些測試技術(shù)最有可能揭示具有嚴(yán)重影響的錯誤。

凈室軟件工程和傳統(tǒng)軟件實踐的差別在于：它不再強調(diào)(有些人稱取消)單元測試和調(diào)試的作用，從而大量地減少(或取消)由軟件開發(fā)者所承擔(dān)的測試工作量。在凈室軟件工程中，單元測試和調(diào)試被正確性驗證和基于統(tǒng)計的測試所替代。凈室方法的特異之處

11.3功能規(guī)格說明不管選擇哪種分析方法，操作分析原理總是適用的。對數(shù)據(jù)、功能和行為建模，并對結(jié)果模型進行分解,提供更進一步的詳細(xì)信息。總體目標(biāo)是從捕獲問題實質(zhì)的規(guī)格說明(模型)移向提供重要實現(xiàn)細(xì)節(jié)的規(guī)格說明。凈室軟件工程通過使用盒結(jié)構(gòu)規(guī)格說明的方法來遵從操作分析原則。一個“盒”在某個細(xì)節(jié)層次上封裝系統(tǒng)(或系統(tǒng)的某些方面)。通過逐步求精的過程，盒被精化為層次?！懊總€盒規(guī)格說明的信息內(nèi)容足以定義其精化，不需要依賴任何其他盒的實現(xiàn)”。這使得分析員能夠按層次劃分一個系統(tǒng)——從頂層的基本表示到底層實現(xiàn)的特定細(xì)節(jié)。11.3功能規(guī)格說明有三種類型的盒：黑盒，狀態(tài)盒，清晰盒

黑盒。黑盒刻畫系統(tǒng)行為或系統(tǒng)部件的行為。通過運用由觸發(fā)映射到反應(yīng)的一組轉(zhuǎn)換規(guī)則，系統(tǒng)(或部件)對特定的觸發(fā)(事件)做出反應(yīng)。

狀態(tài)盒。狀態(tài)盒以類似于對象的方式封裝狀態(tài)數(shù)據(jù)和服務(wù)(操作)。在這種規(guī)格說明視圖中，表示出狀態(tài)盒的輸入(觸發(fā))和輸出(反應(yīng))。清晰盒。在清晰盒中定義狀態(tài)盒所蘊含的轉(zhuǎn)換功能，簡單地說，清晰盒包含了對狀態(tài)盒的過程設(shè)計。11.3功能規(guī)格說明黑盒規(guī)格說明

黑盒規(guī)格說明描述一種抽象、觸發(fā)和反應(yīng)。函數(shù)f被應(yīng)用到輸入(觸發(fā))S的序列S*，并將它們變換為輸出(反應(yīng))R。對于簡單的軟件構(gòu)件，f可以是一個數(shù)學(xué)函數(shù)，但一般情況下，使用自然語言(或形式化規(guī)格說明語言)描述f。黑盒規(guī)格說明為面向?qū)ο笙到y(tǒng)引入的很多概念也適用于黑盒。黑盒封裝數(shù)據(jù)抽象和操縱抽象數(shù)據(jù)的操作。和類層次一樣，黑盒規(guī)約可以展示使用層次，其中，低層盒從樹結(jié)構(gòu)中的高層盒繼承屬性。

黑盒規(guī)格說明

狀態(tài)盒規(guī)格說明

一個狀態(tài)是某個可觀查到的系統(tǒng)行為的模型。當(dāng)進行處理時，一個系統(tǒng)對事件(觸發(fā))作出反應(yīng)，從當(dāng)前狀態(tài)轉(zhuǎn)換到某一新的狀態(tài)。當(dāng)進行轉(zhuǎn)換時，可能發(fā)生某個動作。狀態(tài)盒使用數(shù)據(jù)抽象來確定到下一個狀態(tài)的轉(zhuǎn)換、以及狀態(tài)轉(zhuǎn)換后將要發(fā)生的動作(反應(yīng))。

狀態(tài)盒同黑盒協(xié)作。來自某外部源及一組內(nèi)部系統(tǒng)狀態(tài)T的觸發(fā)S被輸入到黑盒中。包含在狀態(tài)盒內(nèi)的黑盒的函數(shù)g的數(shù)學(xué)描述：

g∶S*×T*→R×T

這里g是和特定狀態(tài)t連接的子函數(shù)。當(dāng)整體地考慮時，狀態(tài)—子函數(shù)對(t，g)定義了黑盒函數(shù)f。狀態(tài)盒規(guī)格說明

狀態(tài)盒規(guī)格說明

清晰盒規(guī)格說明

清晰盒規(guī)格說明是與過程設(shè)計及結(jié)構(gòu)化編程緊密關(guān)聯(lián)的。狀態(tài)盒中的子函數(shù)g被實現(xiàn)g的結(jié)構(gòu)化編程結(jié)構(gòu)所替代。

清晰盒規(guī)格說明11.4凈室設(shè)計凈室軟件工程中使用的設(shè)計方法主要運用結(jié)構(gòu)化程序設(shè)計的原理?；镜奶幚砗瘮?shù)(在規(guī)格說明的早期求精中描述)被精化，其方法是“將數(shù)學(xué)函數(shù)逐步擴展為邏輯連接詞(如，if-then-else)和子函數(shù)構(gòu)成的結(jié)構(gòu)，這種擴展一直進行下去，直到所有標(biāo)識出來的子函數(shù)可以用程序設(shè)計語言直接表達”。

設(shè)計求精與驗證

每個清晰盒規(guī)格說明代表了一個完成狀態(tài)盒轉(zhuǎn)換所需的過程(子函數(shù))的設(shè)計。對清晰盒規(guī)格說明，使用結(jié)構(gòu)化程序設(shè)計結(jié)構(gòu)和逐步求精。一個程序函數(shù)f被細(xì)化為子函數(shù)g和h的序列，這些又被進一步細(xì)化為條件結(jié)構(gòu)(if-then-else和do-while)。進一步的求精給出了連續(xù)的邏輯細(xì)化。

在每個求精層次，凈室團隊執(zhí)行一次形式化正確性驗證。為此，將一類正確性條件集合附加到結(jié)構(gòu)化程序設(shè)計結(jié)構(gòu)上。如果函數(shù)f被擴展為序列g(shù)和h，則f所有輸入的正確性條件是：執(zhí)行g(shù)之后再執(zhí)行h能完成f的功能嗎？如果一個函數(shù)p被精化為形為

if＜c＞thenqelser

的條件形式，則對p的所有輸入的正確性條件是：只要條件＜c＞為真，q能完成p的功能嗎？只要條件＜c＞為假，r能完成p的功能嗎？

設(shè)計求精與驗證

如果一個函數(shù)m被細(xì)化為循環(huán)

donwhile＜c＞則對m的所有輸入的正確性條件是：能夠保證循環(huán)終止嗎？只要＜c＞為真，循環(huán)執(zhí)行n之后能完成m的功能嗎？只要＜c＞為假，退出循環(huán)仍能完成m的功能嗎？設(shè)計求精與驗證

每當(dāng)一個清晰盒被精化為下一個詳細(xì)層次時，都應(yīng)用上面給出的正確性條件。值得注意的是：結(jié)構(gòu)化程序設(shè)計結(jié)構(gòu)的使用限制了必須進行的正確性測試的數(shù)量。對順序結(jié)構(gòu)只檢查單個條件，對if-then-else結(jié)構(gòu)只測試兩個條件，對循環(huán)則只驗證三個條件。設(shè)計求精與驗證

例：過程設(shè)計的正確性驗證：設(shè)計并驗證一個小的程序，該程序?qū)δ辰o定的整數(shù)x，找出其平方根的整數(shù)部分y。

yesno設(shè)計求精與驗證

定義入口和出口條件。為了證明設(shè)計的正確性，需要證明圖中表示的條件init、loop、cont、yes和exit在所有情形下都是正確的。設(shè)計求精與驗證

1.條件init要求［x≥0andy=0］。基于問題的需求，假定入口條件是正確的。因此，init條件的第一部分x≥0是滿足的。在流程圖中，在init條件前的語句設(shè)置y=0，因此，init條件的第二部分也是滿足的，因此，init為真。2.條件loop可能以兩種方式之一出現(xiàn)：(1)直接從init(此時loop條件被直接滿足)，或(2)通過穿過條件cont的控制流。因為條件cont與條件loop相同，因此，不管從哪條路徑到達它，條件loop都為真。3.條件cont:只有在y值被遞增1后，才能遇到條件cont。另外，只有在條件yes也為真時，才能調(diào)用到達條件cont的控制流路徑。因此，如果(y+1)2≤x，則y2≤x，條件cont成立。4.條件yes在如圖所示的條件邏輯中被測試，因此，當(dāng)控制流沿著所示的路徑移動時，條件yes一定為真。5.條件exit首先要求x保持不變，對設(shè)計進行檢查可發(fā)現(xiàn)x沒有出現(xiàn)在賦值操作的左邊，沒有使用x的函數(shù)調(diào)用，因此，x保持不變。因為條件測試(y+1)2≤x不成立時，才可能到達條件exit，因此(y+1)2＞x成立。此外，loop條件還必須保持為真(即，y2≤x)，因此，(y+1)2＞x和y2≤x可以組合在一起滿足exit條件。保證循環(huán)終止:

因為y是遞增的，而x≥0，因此，最后(y+1)2≤x不成立，循環(huán)一定終止。

設(shè)計求精與驗證

設(shè)計驗證的優(yōu)點

對清晰盒設(shè)計的每一步求精進行嚴(yán)格的正確性驗證有許多顯著的優(yōu)點：(1)將驗證簡化為一個有限的過程。在清晰盒中，以嵌套的、順序的方式組織控制結(jié)構(gòu)，這就自然地定義了一個層次，該層次顯示了必須被驗證的正確性條件。(2)再怎么強調(diào)將驗證簡化為有限過程對質(zhì)量產(chǎn)生的正面效果都不過分。除了那些最微不足道的程序，即使所有程序都具有無限數(shù)目的可執(zhí)行路徑，也可以在有限步驟內(nèi)對它們進行驗證。(3)使得凈室團隊驗證設(shè)計和代碼的每一行。在正確性定理的基礎(chǔ)上，團隊可以通過小組分析和討論來執(zhí)行驗證，并且當(dāng)在生命關(guān)鍵或使命關(guān)鍵的系統(tǒng)中需要額外的信心時，可以生成書面的證明。(4)達到幾乎零缺陷的水平。在團隊的復(fù)審過程中，每個控制結(jié)構(gòu)的每個正確性條件被依次驗證。每個團隊成員必須就每個條件都是正確的達成共識，這樣只有團隊的每個成員均未能正確地驗證某條件時，才有可能出現(xiàn)錯誤。設(shè)計驗證的優(yōu)點(5)具有可伸縮性。每個軟件系統(tǒng)，不管有多大，均具有頂層的由順序、選擇和循環(huán)結(jié)構(gòu)構(gòu)成的清晰盒過程。(6)產(chǎn)生出比采用單元測試更好的代碼。單元測試僅僅檢查從很多可能的路徑中選出的測試路徑的執(zhí)行效果。基于函數(shù)驗證的理論，凈室方法可以驗證所有數(shù)據(jù)的每個可能的結(jié)果，因為雖然一個程序可能有很多可執(zhí)行路徑，但它只有一個函數(shù)。驗證也比單元測試更有效，可以在幾分鐘之內(nèi)檢查大多數(shù)驗證條件，但單元測試要花費大量時間去準(zhǔn)備、執(zhí)行和檢查。設(shè)計驗證的優(yōu)點11.5凈室測試凈室測試的策略在根本上不同于傳統(tǒng)測試方法。傳統(tǒng)測試方法導(dǎo)出一組測試用例發(fā)現(xiàn)設(shè)計和編碼錯誤；凈室測試的目的是：通過證明用例的統(tǒng)計樣本的成功運行來確認(rèn)軟件需求。

統(tǒng)計使用測試計算機程序的用戶沒有必要去了解設(shè)計的技術(shù)細(xì)節(jié)。程序的用戶可見的行為通常是由用戶產(chǎn)生的輸入和事件所驅(qū)動的。在復(fù)雜系統(tǒng)中，輸入和事件的可能的范圍(即用例)是非常廣泛的。什么樣的用例子集能夠充分驗證程序的行為？這是統(tǒng)計使用測試關(guān)注的第一個問題。統(tǒng)計使用測試“等同于以用戶試圖使用軟件的方式來測試軟件”。為了完成測試工作，凈室測試團隊（也稱為認(rèn)證團隊）必須確定軟件的使用概率分布。對軟件的每個增量的規(guī)格說明(黑盒)進行分析，并定義一組使軟件改變其行為的觸發(fā)(輸入或事件)。通過與潛在用戶的交流、使用場景的建立、及對應(yīng)用領(lǐng)域的全面了解，為每個觸發(fā)分配一個使用概率。按照使用概率分布為每個觸發(fā)集合生成測試用例。統(tǒng)計使用測試

例，在家庭保安系統(tǒng)中，使用凈室軟件工程方法開發(fā)一個軟件增量來管理用戶與安全系統(tǒng)鍵區(qū)之間的交互。對這個增量，已經(jīng)標(biāo)識出5個觸發(fā)。通過分析，給出每個觸發(fā)的概率分布百分?jǐn)?shù)。為了更容易地選擇測試用例，這些概率被映射到1至99的數(shù)字區(qū)間。

統(tǒng)計使用測試

為了生成符合使用概率分布的使用測試用例序列，生成1至99之間的隨機數(shù)。每個隨機數(shù)與前面概率分布的一個區(qū)間相對應(yīng)。因此，使用測試用例序列可以隨機定義，但又與觸發(fā)發(fā)生的適當(dāng)概率相對應(yīng)。例如，假定生成