凈室軟件工程創始人米爾斯的貢獻研究

斯琴巴圖

（1.內蒙古師范大學科學技術史研究院，呼和浩特010022；2.內蒙古婦女干部學校，呼和浩特010051）

0 引言

軟件的質量對于航空航天、軍工、醫療衛生、自動駕駛等大型系統和實時系統可謂極其重要。例如1978年哈特福德體育館倒塌，1996 年阿利亞納五號火箭發射失敗，2000 年Therac-25 醫療放射治療裝置讓患者暴露在過量輻射中的事故，2018 年10 月印尼獅航和2019 年3 月埃塞俄比亞航空公司的兩起波音737MAX飛機導致的空難都與軟件缺陷有關。運用今天的軟件工程技術能否生產出高質量的軟件，能否具有高可靠性？答案是肯定的！而且這種技術早在上世紀80 年代已經被開發出來，但由于對軟件開發人員技術門檻的要求過高，經濟方面投入較大，以及軟件產業界普遍的共識——軟件通過維護升級可以不斷完善，沒必要第一次就生產出完美無缺的軟件的理念等因素限制了這種技術的推廣普及。這種技術被稱為形式化方法，凈室軟件工程（Cleanroom Software Engineering）便是形式化方法的一種變種，其可操作性比純形式化方法更強。凈室技術通過在IBM、愛立信、美國國家航空航天局（NASA）、美國國防部（DoD）及大量其他機構的成功實踐證明了其自身的強大。1996 年DoD 軟件數據與分析中心在其所作的軟件方法比較分析中，報告凈室具有真實的價值和質量優勢[1]。

美國計算機科學家、數學家、IBM 院士米爾斯（Harlan D. Mills）博士在IBM 聯邦系統部工作期間創立了凈室軟件工程，一種基于數學理論的以經濟的方式生產高可靠性軟件的工程技術。這種技術從萌芽到成熟經歷了近20 年的時間，米爾斯在其形成的過程中做了大量的工作，從而被稱為凈室軟件工程創始人。本文將通過展示米爾斯在凈室軟件工程方面的具體工作，討論其貢獻，同時梳理凈室作為一種成熟方法的形成歷史過程。

1 米爾斯及凈室軟件工程

1.1 米爾斯學術生涯

米爾斯（1919-1996）是凈室軟件工程創始人，首席程序員團隊方法的創始人，軟件工程思想領袖。他是IBM Fellow（IBM 院士），IBM 聯邦系統部門的軟件工程和技術主管和IBM 公司技術委員會的成員。他是1975 年召開的第一屆軟件工程全國（美國）大會的主席。1975 年到1981 年，他擔任IEEE 軟件工程學報的編輯；從1980 年到1983 年，他擔任IEEE 計算機學會的主管；1981 年，他是IEEE Fall CompCon 的主席。1985 年，他獲得了DPMA 杰出信息科學獎，1987 年獲得了J. D. Warnier 獎。在米爾斯去世之后，為了紀念他，在1999 年，IEEE 計算機學會設立了Harlan D.Mills獎，主要獎勵在軟件工程理論與實踐領域做出貢獻的學者。

米爾斯于1952 年在愛荷華州立大學獲得數學博士學位。從1954 年到1957 年，他在通用電氣的管理咨詢服務公司工作，1958 年創立了公司Mathematica，后來由Martin Marietta 收購。1964 年至1987 年，米爾斯在IBM 公司聯邦系統部工作。于1996 年去世時，米爾斯博士是佛羅里達理工學院（Florida Institute of Technology）的計算機科學教授，也是軟件工程技術公司（Vero Beach，FL and Knoxville，TN）的創始人，圖1 為米爾斯博士。

圖1 米爾斯（Harlan D.Mills）

1.2 凈室軟件工程

凈室軟件工程是一種應用數學和統計學理論以經濟的方式生產高質量軟件的工程技術。“凈室”一詞來源于半導體工業的生產硬件的凈室[1]。半導體工業的凈室在生產產品的過程中，將預防缺陷產生作為最重要的事情，而不是之后排除故障。使用“凈室”命名，顯示了凈室軟件工程也將缺陷預防放在絕對重要的首位，其目標是開發零缺陷的軟件產品。凈室具有堅實的理論基礎，并由①統計質量控制下的增量開發技術；②基于函數的規格、設計和驗證技術（盒式結構方法）；③統計測試和軟件認證技術等三大關鍵技術有機整合而成。它以凈室小組作為工作基本單元采用多人共同工作的方式生產、測試軟件產品。所以，它的工作成果都歸集體（凈室小組），當然出現問題時，也由集體承擔責任。

米爾斯在凈室方面最重要的一篇文章是1987 年9份發表在《IEEE Software》上的“凈室軟件工程”。該文章中首次提出“凈室軟件工程”的概念，并介紹了采用凈室軟件工程方法開發的三個成功案例，統計式質量控制在管理方面的好處，軟件統計屬性從何而來，如何衡量一個軟件的質量，功能驗證的優點和代替排錯的原因、統計測試、增量開發、軟件認證等。該文中未提及盒式結構方法，但提到了精確的規格說明書，而盒式結構中的黑盒正是精確描述軟件需求規格的工具。從米爾斯在1990 年發表的文章“統計質量控制下的工程軟件”中可以探知盒式結構方法已被納入凈室[2]。

2 奠定凈室軟件工程理論基礎

2.1 凈室理論基礎的歷史背景

1968 年10 月，NATO（北大西洋公約組織）在當時的聯邦德國召開了“軟件工程”國際學術會議。會議正式提出了“軟件危機”和“軟件工程”，并說明通過“軟件工程”解決當時的“軟件危機”。會議的發起人慕尼黑工業大學的計算機科學家Fritz Bauer 教授認為，軟件工程是建立和使用一套合理的工程原則，以便經濟地獲得可靠的、可以在實際機器上高效運行的軟件[3]。其中，“工程原則”的意思包含了軟件工程除了要有方法、工具等技術措施以外，還應該有必要的組織管理措施。會議上還提出了要建立軟件開發和生產的數學基礎。之后在1969 年的軟件工程會議上，將軟件的正確性問題和概念作為主題之一進行了討論。這促使軟件的數學基礎和軟件正確性問題成為軟件工程基礎的重要組成部分[4]。這種背景也是凈室基于數學理論，重視組織管理，并且將正確性證明作為重要方法的主要原因。

2.2 凈室理論基礎的內容及米爾斯的工作

凈室軟件工程的理論基礎來自于數學，具體為其軟件開發方法基于數學的函數理論，其測試方法基于統計學。米爾斯意識到一個特定的程序像函數一樣有定義域到值域的映射，從而將程序看作是一個數學函數規則，致使函數理論和應用成為軟件開發和驗證的基礎[5]。也正是基于該理論，后續才有了基于函數理論的程序正確性驗證技術、增量開發技術和盒式結構方法。米爾斯的“大型系統中的自頂向下編程”（1970 年發表）、“結構化程序設計的數學基礎”（1972 年發表）、“計算機程序設計新數學”（1975 年發表）和“如何正確編寫和認識程序”（1975 年發表）等文章奠定了凈室方法的函數理論基礎。米爾斯與林格（R. C. Linger）、維特（B.I.Witt）三人合著的《結構化編程：理論與實踐》是上世紀70、80 年代最有影響力的結構化編程方面的著作之一，書中還提出了后來凈室方法中采用的一項重要技術——基于函數理論的程序正確性驗證技術（功能驗證）。

米爾斯的另一個觀點——軟件測試只是從無限的可能的軟件使用情況中抽取的樣本，奠定了凈室統計測試方法和質量認證的基礎。他于1970 年發表的論文“關于計算機程序的統計驗證”將統計推斷技術引入到程序正確性問題中[6]，從而將統計學應用于軟件認證。此外，他在1970 年提出了飽受爭議的“首席程序員團隊”技術，雖然飽受爭議，但首席程序員團隊技術為軟件團隊成員之間的溝通渠道問題提供了原創解決方案[7]，而且早在1971 年中期，由IBM 交付《紐約時報》使用的在線存儲和檢索系統項目中成功運用了該技術[8]。凈室小組工作法可以說是在某種程度上繼承了首席程序員團隊技術。

2.3 凈室理論基礎的影響

一種成熟的理論基礎對于工程方法（技術）極其重要，它起到的指引作用是其他任何事物無法代替的。米爾斯對軟件數學理論基礎的解釋——“程序是一個數學函數規則”對計算機科學產生了重要影響，使得大量數學函數的理論和應用成為軟件開發和驗證的基礎。也正是因為有了堅實的數學理論基礎，才會有后來的基于函數理論的程序正確性驗證技術、增量開發技術和盒式結構方法。由于凈室方法將統計學作為測試的理論基礎，其統計抽樣測試技術才得以穩固的發展。

3 開發三大關鍵技術

3.1 開發統計質量控制下的增量開發技術

增量開發的思想是先開發出一個能夠運行，只有基本架構的增量（軟件），這個增量也許只有界面，沒有實現其他任何功能。之后，逐步添加功能，生成第二個、第三個、……、第N 個增量，最終得到完整功能的軟件。統計質量控制之下的增量開發技術實際上是將制造業中的統計質量控制引入到軟件開發過程中，預防和控制軟件開發過程中的每一項任務的質量，從而生產出高質量的軟件。

該技術早在1970 年已經有了初步方案。米爾斯在其著名文章“大型系統中的自頂向下編程”中，通過“中間系統序列”和“骨架程序”等概念，首次展示了增量開發的思想。這種思想的產生有三個前提，即①米爾斯將程序看作是數學函數；②結構化編程；③程序正確性證明。將程序看作一個數學函數后，可以通過不斷將函數逐步推導擴展成多個更簡單的函數和連接詞，直至可以使用程序語句表示為止。在1968 年和1969 年，荷蘭計算機科學家迪杰斯特拉（E.W.Dijkstra）發表了多篇有影響力的結構化編程的文章，提倡去除程序里的GOTO 語句，使用順序、選擇和循環三種結構編寫程序。結構化編程的出現，讓自頂向下編程成為可能，改變了之前在紙上先做設計，然后自底向上的編程習慣。程序正確性證明技術也在1969 年前后發展了起來，它的發展為函數推導過程的正確性證明提供了理論依據和技術手段。也是1970 年，第一個軟件生命周期模型——瀑布模型出現，之后軟件產業界迅速接受了該模型。但由于意識到瀑布模型的線性開發的缺點，米爾斯繼續發展了增量開發技術（增量開發模型）。直至上世紀80 年代，米爾斯將統計質量控制技術引入軟件開發，與增量開發技術結合后形成了統計質量控制下的增量開發技術。

3.2 開發盒式結構方法

凈室的基于函數的規格、設計和驗證技術也被稱為盒式結構方法。盒式結構（box structures）方法用于描述軟件規格，并通過逐步求精的擴展方法實現軟件規格。盒式結構包括黑盒、狀態盒和明盒等三類盒子。黑盒描述用戶的外部行為，狀態盒是黑盒的擴展，明盒是狀態盒的擴展，明盒基本上是一段偽代碼算法或是程序。1986 年，米爾斯和林格、赫夫納（A. R.Hevner）合著的《信息系統分析與設計原理》（Principles of Information Systems Analysis and Design）提出了一種簡化分析和設計的數學方法——盒式結構方法。開發該方法的原因是由于當時系統分析使用的數據流圖工具在描繪復雜的商業業務時線條顯得紛亂復雜，不僅不利于分析，且容易使人犯錯。而盒式結構里的黑盒可以很好的解決該問題，簡化系統分析工作。系統設計工作是在不斷的將黑盒擴展為狀態盒，將狀態盒擴展為明盒的過程中實現的，且在每一步擴展過程中都會有嚴格的正確性驗證，確保最終軟件產品滿足用戶當初的所有需求。

3.3 開發統計測試和軟件認證技術

凈室的統計測試技術理論依據來自統計學的抽樣理論。凈室測試與傳統測試方法不同，在傳統測試方法中，測試人員一開始就假定軟件中肯定存在錯誤，在這種心理前提下盡可能找出設計和編碼的錯誤，且錯誤越多越好，而且如果找到并修復了足夠多的錯誤，則認為軟件質量會提高。凈室軟件測試（認證）是為了認證軟件的可靠性，而不是傳統意義上的測試軟件，即不是為了找出錯誤。在凈室測試中，測試人員和開發人員不是敵對的關系，這一點也與傳統測試不同。

早在1970 年，米爾斯就注意到了可以將統計學中的概念引入到軟件編程。1983 年，米爾斯與戴爾（M.Dyer）開發了凈室的統計測試與軟件認證技術。在當時，傳統的測試方法是程序員只使用有代表性的用戶操作軟件的手法和輸入測試軟件。這種測試方法只能保證軟件在測試用例上是正確的，但不能保證其他情況下也是正確的。米爾斯在其1987 年發表的論文“凈室軟件工程”中曾解釋軟件本身并沒有統計屬性，但是用戶使用（操作）軟件情況是可以被統計的，所以軟件的統計屬性來自于用戶對軟件的可能使用情況。根據用戶的使用情況分布概率，隨機生成測試用例，之后通過測試用例測試軟件的正確性。

3.4 三大關鍵技術的影響

凈室的三大關鍵技術可以合起來使用，也可以獨立分開使用。當合起來作為凈室技術使用時，其效果已經在多個大型項目中得以展示，并被包括NASA 和DoD 等對軟件要求極高的多家機構所認同。凈室的增量開發技術通過智力控制解決軟件復雜性問題方面給出了一種解決方案。這是因為可以讓開發者在某一時間段將精力集中在某一個增量上，而不用時刻考慮更多的問題。增量技術通過快速交付增量，得到用戶反饋，改進需求和生產過程，再交付增量，……的循環過程方式，為軟件生產方和用戶方的積極溝通提供了方案，避免了最終軟件產品并非用戶所需的嚴重問題。盒式結構方法為人們提供了一種簡化了的系統分析和設計的數學方法。這種方法不僅可以用于結構化分析和設計，還可以用于面向對象分析和設計。它解決了系統分析時使用數據流圖工具在描述復雜系統業務時的線條混亂的問題，為系統分析和設計提供了一種獨特的工具。統計測試和軟件認證技術在人員關系層面解決了開發人員和測試人員的敵對關系，將其關系從對立轉為合作。它在技術層面通過抽樣測試用例推進了測試技術的發展，將當時只用幾種典型用例測試軟件的方式往前推進了一大步。

4 結語

米爾斯博士是凈室軟件工程創始人。1970 年至1990 年的20 年間，他奠定了凈室的理論基礎與IBM同事一起開發并實踐了三大關鍵技術，讓凈室從一粒種子長成一棵參天大樹。米爾斯的成就除了其自身的天分和知識儲備以外，也與當時軟件工程的提出，各種軟件技術被開發應用的大環境有關，還與當時美國政府重視軟件工程的發展，米爾斯所在的IBM 聯邦系統部能夠承接美國政府和軍方的大型項目，從而有機會研究和實踐高可靠性軟件理論和技術有關。當然，也與米爾斯一同開發實踐凈室的團隊成員有很大關系。

由于經濟成本較高，對開發人員的技術門檻和用戶代表的信息素養要求較高，適合于開發大型高可靠性軟件項目等因素，凈室在我國并沒有得到足夠的重視和發展。但隨著不斷的有大型軟件項目的啟動，對軟件高可靠性的強烈要求，凈室軟件工程必定在我國會得到更多的關注。