形式化方法在軟件工程中的應用研究

苗德成，馮黎波

（1．韶關學院數學與信息科學學院，廣東韶關 512000；2．河北科技大學理學院，河北石家莊 050018）

形式化方法在軟件工程中的應用研究

苗德成1，馮黎波2

（1．韶關學院數學與信息科學學院，廣東韶關 512000；2．河北科技大學理學院，河北石家莊 050018）

探討了形式化方法的基本概念，重點研究了形式化方法的數學理論基礎和其在軟件工程各階段的應用情況，分析了形式化方法在理論研究和工程實踐上的優勢和局限性及其原因，并指出了形式化方法發展的幾個方向，最后對形式化方法在軟件工程中的應用做了評價。

形式化方法；軟件規約形式語言；軟件工程；形式系統；規約

基于軟件工程方法論，軟件工程是將客觀世界實際問題抽象成認識世界概念模型，再將認識世界概念模型轉換為程序世界可執行程序集合的活動，前者是認知領域符號推演與系統論證過程，而后者則是工程領域理論實踐與計算轉換過程。在軟件工程活動中成功運用形式化方法將實際問題認知模型轉換為軟件規約［1］（software specification）可縮短軟件開發周期并減少項目研制成本，軟件規約既是系統分析師、設計師、程序員與用戶之間的協議，也是系統模塊與程序部分的界面，只要保證軟件規約對實際問題描述的可靠性與協調性，就能確保軟件系統實現的完備性與一致性。

1 形式化方法

軟件工程活動中形式化方法雖然被廣泛使用，但形式語言、形式系統等相關基本概念并未有精確定義。形式語言（formal language）是按一定語法規則構成的公式或符號串的有限或無限集［2］。一階語言（firstorder language），Ada，Fortran，Java等都是形式語言［3］。形式系統是建立在形式語言基礎上的一個邏輯演繹系統以完成特定符號推演過程。從形式系統和實際問題復雜性分析，形式化方法是具有堅實數學基礎，使用形式語言構建形式系統全面描述和系統分析現實世界復雜問題的一種有效工具。形式化方法基本含義是用數學方法解決計算機科學理論研究和軟件工程實踐相關問題的工具，集合論、數理邏輯、代數理論、程序設計語言理論、構造類型論（constructive type theory）等數學理論構成了形式化方法堅實的理論基礎。

對于形式化方法在軟件工程中的具體應用，集合論（含可解決羅素悖論問題的直覺集合論）各種算子、序關系（如點態序［5］、基于Egli－Milner偏序與Smyth偏序的冪域理論等）適于描述軟件系統狀態轉換，而數理邏輯是形式化方法最重要的理論工具，軟件系統的業務邏輯可用形式理論［3］及相關演算完成，業務邏輯的服務用形式理論閉包（formal theory closures）描述，通過修正演算形成軟件版本的演變，而軟件版本序列的可交換性保證實際軟件功能具有較好的可擴展性。形式化方法堅實的理論基礎在于其內在的數學結構，從數學理論角度分析，任何復雜的數學結構均可建于集合、邏輯等基本數學概念上，因此，集合論和數理邏輯這2種數學工具構成了形式化方法最為重要的數學理論基礎，如圖1所示。

類別代數（sorted algebras）尤其是∑－代數等多類別代數是抽象數據類型（abstract data type）的理論基礎，基于∑－代數的等式理論（equation theories）與項重寫系統（term rewriting systems）拓展了自動定理證明領域，很好地解決程序終止性問題、完備性算法與統一性算法（unification algorithms）等問題［5］。范疇論在計算機科學中有廣泛應用，其許多技術成為形式化方法重要工具，雙笛卡爾閉范疇（bicartesian closed categories）等形式系統的范疇分析非常適合于描述客觀世界復雜問題，而范疇論與組合邏輯結合為函數型語言的編譯程序提供新方法，進程代數、共代數、界程演算等理論推進了形式化方法進一步發展。程序設計語言理論分析程序設計語言的語法性質、操作特性和語義形式，描述所開發軟件系統結構、組成、有窮自動機［4］（finite automata）及與軟件工程各階段對應的形式模型，其中，遞歸計算是程序設計語言理論有效處理程序循環結構的一項核心技術，而泛函分析的不動點理論（fixed point theory）是設計程序指稱語義時高效處理遞歸計算的重要工具。構造類型論為軟件系統設計與研發提供一個新框架［5］，數理邏輯與程序設計語言理論在這個新的框架內有機結合，在一個形式系統內同時描述軟件規約與程序設計，自動生成軟件并進行程序驗證。形式化方法以圖1的數學理論為基礎，形成了應用于軟件生命周期不同階段不同的軟件規約形式語言SSFL（software specification formal language）。

圖1 形式化方法的數學基礎Fig．1 Mathematical foundation of formal methods

2 軟件工程各階段的規約描述

按照軟件工程“自頂向下、逐步求精”的原則將軟件開發生命周期分為6個階段：可行性分析、需求分析、體系結構設計、詳細設計、編碼、測試發布，形式化方法貫穿軟件工程整個生命周期。SSFL是形式化方法重要外延，SSFL的衡量標準是抽象表達的準確性與清晰性、概念運用的標準性與無二義性、形式化處理能力的支持性與可解釋性等。SSFL類型較多，每種SSFL數學基礎不同，其應用側重點也不同。SSFL總體上分為3類：非形式化、半形式化和形式化［6］。非形式化SSFL描述框架性內容，以圖形或自然語言輔助說明主體信息；半形式化SSFL用BNF描述語法，不進行形式化語義定義而用偽碼設計接口和模塊；形式化SSFL基于參數化的類別代數等數學理論形式化表述語法和定義語義。

2．1 可行性分析

可行性分析是軟件生命周期的第1階段，運用大量數據資料對影響軟件系統開發各種因素全面、系統地論證待開發系統項目是否可行，提出綜合分析評價，指出項目可行性、風險預測和建議為項目決策提供依據。本階段將客觀世界實際問題從初始概念轉換為可行性研究報告，文檔準確分析市場需求，合理確定投資方案，規定具體采納的軟件標準或規范，定義專業術語并列出縮寫詞原文，說明待開發軟件系統輸入／輸出、基本數據流程和處理流程、軟硬運行環境、開發環境條件和限制及軟件投入使用的最遲時間等技術、功能或性能指標。

當前極少有專門定位于可行性分析的形式化方法，其主要原因在于難以將自然語言表達能力與形式化方法符號演算系統很好地結合起來，達到普通用戶既可理解形式系統的描述，同時又可保持形式化方法精確、可推演等優勢的終極目標目前看來還需要許多工作要做。Z語言基于模式演算［7］，是一種運算功能強大但不可執行的半形式化語言，Z語言的最大優點是采用非形式化的英語對軟件規約解釋，短小且易于閱讀。

2．2 需求分析

需求分析以可行性分析報告作為輸入，分信息預處理和信息處理2個子階段，前者要求SSFL可讀性好、易修改、可維護，后者要求SSFL精確無二義性并可進行完整性檢查和一致性證明。將可行性分析非形式化處理部分與本階段形式化處理部分聯系起來是需求分析難點，需求規格說明書是與用戶交流的主要物質基礎。

VDM（vienna development method）元語言是一種形式化語言［8］，基于謂詞演算和集合論的證明規則，采用“面向模型”方法給出抽象機狀態確定模型，生成文檔可讀性好，程序員易于掌握和實現原型。從形式化處理角度上分析，指稱語義的設計是需求分析階段主要工作之一，VDM寫指稱語義基本步驟是構建語法域與語義域，建立語義解釋函數并定義一些輔助函數，然后利用語義方程解釋語法單位的語義，其中域的構造是重點，VDM由原始域（數值域、字符域、真值域等）經并、積、冪、子等算子和投影（projection）、注入（injection）、檢查（inspection）等原子操作構造所需各種域。但是VDM在需求分析階段的使用存在明顯缺陷，第一，它缺乏模塊性；第二，VDM不能處理并發的情況，而RAISE（Rigorous approach to industrial software engineering）語言彌補了VDM的不足［9］。RAISE使用的代數法與VDM基于模型的方法存在明顯不同，即如何描述規約和對規約語言賦予語義，VDM沒有明確解決怎樣將這不同結合起來，而RAISE很好地做到了這一點。RAISE是一種光譜語言，既可以在需求分析階段書寫初級抽象規約，也可以在詳細設計階段描述自動轉換為編碼階段所需的程序設計語言的具體規約，RAISE提供一系列工具和轉換技術，形成處理需求分析階段全過程的嚴格方法。

SXL（state transition language）語言是可執行的SSFL，在需求分析階段從可行性分析報告描述的實際問題中導出E－R框架，根據E－R框架給出SXL語言的對象和事實，SXL語言的執行有助于開發團隊交流和理解［10］。VDM元語言、RAISE語言和SXL語言都是軟件工程需求分析階段普遍應用的形式化方法。

2．3 體系結構設計

體系結構設計是軟件設計第1階段，該階段根本目的是將需求規格說明書轉換為計算機可以實現的目標系統，對上階段各種備選方案綜合分析比較，選出最佳方案與用戶達成共識后為軟件確定數據結構并設計數據庫，提交體系結構設計說明書參加評審。體系結構設計側重描述軟件系統的接口、功能和結構，使用過程代數等形式化工具利用輸入、輸出間關系描述系統行為，將軟件規約模塊化而減少設計自由度。

TLG（two level grammar）語言適合軟件工程體系結構設計階段僅需說明做什么而不強調如何做的特點而在本階段得到普遍應用，TLG在表示形式上與Prolog相似，針對軟件系統形式化規約說明將自然語言嵌入嚴格的數學函數和邏輯程序設計范型中，書寫簡單，易于論證用戶需求的一致性［11］。

基于圖形用戶界面和可用形式化方法描述圖形界面程序設計環境的考慮，GLIDE也是本階段可用的一種半形式化的SSFL，其主體部分為圖形程序設計環境數據結構的產品集、簡單查詢、描述轉換和轉換不變式（transform invariant）的謂詞集［12］。GLIDE優點是抽象級別高，應用范圍廣，使用局限在于相應的軟件規約必須予以適當修改和擴充。

2．4 詳細設計

詳細設計是軟件設計第2階段，本階段基本要求是與上階段軟件系統形式化描述保持一致。在體系結構設計基礎上，為軟件系統各模塊確定相應算法及內部數據結構，獲得目標系統具體實現的精確描述，文檔詳細設計說明書為下階段編碼工作做好準備。

Larch語言基于一階謂詞邏輯用于說明程序序列功能，接口部分描述數據操作效果，核心部分描述獨立于計算模型固有特性，對Larch適當擴充可增強詳細設計階段軟件系統描述及處理能力［13］。形式化的Trace語言也是軟件工程詳細設計階段一種廣泛應用的形式化工具，用跡斷言（trace assertion）方法說明每個模塊接口需求，將模塊實現的抽象數據對象作為有窮自動機，其外部所有可見行為都是由對象的跡完全決定［14］。Trace語言不同于其他SSFL的突出特點是其定義抽象對象的方程式集作為一個等式系統可用項重寫模擬，將跡斷言規則視為跡重寫規則（trace rewriting rule）可形式化地得到跡重寫系統（trace rewriting system），從而在同一形式系統內同時進行程序的自動生成與驗證。

在軟件工程詳細設計階段，半形式化的Larch語言也可由項重寫實現，進一步增強規約描述的可讀性。詳細設計階段傳統的SSFL主要用于順序系統，但也有許多形式化技術支持并發系統，如Modula，Gypsy，Mesa等［15］。

2．5 編 碼

本階段將詳細設計階段成果用計算機程序設計語言描述出來，得到可在計算機上執行的程序。編碼階段程序設計語言的選擇、編碼風格的把握和編程技巧的運用直接影響程序可靠性、可讀性、可測試性和可維護性。

本階段有較多的SSFL進行形式處理工作，LOTOS（language of temporal ordering specification）語言是一種精確定義且可執行、可證明的形式化語言［15］，LOTOS由2部分構成，基于CCS（calculus of communication systems）和CSP（communicating sequential processes）的進程代數和基于代數語言ACT One／Two的抽象代數［16］，前者用于表示系統的時序行為，后者根據數據類型、操作函數等描述編碼階段的具體數據，LOTOS已成為OSI形式描述技術的事實標準且適用于分布式系統。

ADTS（algebraic data type specification）語言基于嚴格的多類別代數對軟件規約進行形式化推理［17］，支持可構造性、模塊化、參數化和異常處理，在ADTS可執行原型環境中以類似項重寫的方式可轉換為Pascal程序設計語言，在軟件工程編碼階段單元模塊設計中非常有用。

近年來一些程序構造的形式系統被引入軟件工程活動中，基于Martin－l?f構造類型論的SSFL技術在軟件工程編碼階段得到了廣泛的應用。許多Martin－l?f構造類型論的形式化方法將程序與軟件規約形式說明對應起來，這些形式化方法不再使用Tarski真值語義，而是利用命題和集合之間Curry－Howard同態的Brouwer－Heyting－Kolmogorov直覺語義解釋Ξ，Π等邏輯常數，把集合轉換為解決實際問題的軟件規約，用集合內元素構造滿足該軟件規約的程序，當前已經開發出許多以構造類型論為基礎的形式系統（如LCF，ALF，Coq等）可完成程序開發、驗證及形式化證明。

2．6 測試發布

測試發布是軟件工程活動最后階段，本階段在軟件投入運行前對軟件生命周期各階段文檔和程序源代碼進行查錯和糾錯，從用戶角度精心設計一批測試用例運行程序，暴露軟件中潛在錯誤、缺陷及風險，驗證軟件是否滿足用戶要求。

長期理論研究和工程實踐積累了豐富的形式化測試和發布技術，分布式網絡系統的并發度、不確定性、分布控制和安全性及可靠性等問題是當前軟件工程測試發布階段SSFL研究的重點，其中，形式驗證和測試集成方法是新興的研究熱點［18］。形式化測試序列和測試覆蓋標準基于控制流或數據流，從EFA（extended finite automata）或Petri網可達圖中產生測試序列。OBJ語言是一種形式化的寬域語言，以獨立于實現的方式描述數據結構，其可執行性使得可按源代碼測試方式驗證軟件規約［19］。OBJEX是一個形式化測試工具，基于重寫規則執行軟件規約形式說明完成語法和類型檢查。

3 形式化方法的簡要評價

形式化方法在軟件工程各階段的廣泛應用有效地改進軟件質量［20］，提高開發效率，減少開發費用，形式化方法作為一種有效的交流形式易于在軟件規約上取得一致，軟件工程各階段的文檔既是開發團隊與用戶交流的重要依據，又是軟件開發的起點。形式化方法在軟件開發中的優勢主要在于問題抽象、語法定義準確、語義清晰可操縱、表達無二義性、描述簡潔規范，形式化方法獨特優勢還體現在軟件系統非功能特性的證明上，保密性、安全性和結構性要求等非功能特性難以用傳統的測試技術核查，形式化方法利用數學工具求解確定的近似解可進行有效地核查。

形式化方法在軟件工程各階段取得很大成功，但在理論研究和工程實踐上仍存在一些局限性，尤其是由于缺乏有效工具而在實際工業項目中應用相對較少，形式化方法的工業標準更是少見，例如在形式系統中受當前程序驗證工具能力影響，有些問題（如程序停機的不可判定性）即便是簡單卻也無法證明。形式化方法局限性源于其龐大的數學基礎體系，首先是軟件規約選用的數學工具未必絕對有效，其次是形式化規約在數學意義上的解決不具備唯一性，甚至有些理論在當前工程實踐活動中還找不到正確的數學解釋，再次不同工程領域、不同應用背景下軟件規約存在十分突出的相容性問題。

由于缺少定理證明機制支持，程序功能正確性難以證明，因此，將不同的形式化分析方法組合起來，形成一種混合方法，把形式化證明與實用的測試、容錯和運行時檢查等技術相結合是形式化方法未來發展的一個研究方向。形式化方法雖然在軟件工程活動中有許多優勢，但對數學基礎要求較高，軟件開發團隊特別是程序員難以理解，將形式化的表達方式簡化，盡最大努力自然語言化，增強軟件規約的可讀性則會得到更大的發展空間，這也是形式化方法應該努力的一個方向。

4 結 語

形式化方法在軟件工程中的應用褒貶不一，支持者認為形式化方法極大地推進了軟件開發的進程［21］，而反對者幾乎持完全反對的態度［22］，形式化方法40多年的研究與應用取得大量成果說明其并非一無是處，但也應清醒地認識到形式化方法理論研究特別是工業應用中的困難和缺陷。

［1］ 陳火旺，羅朝暉，馬慶鳴．程序設計方法學基礎［M］．長沙：湖南科學技術出版社，1987．

［2］ 陸汝鈐．計算機語言的形式語義［M］．北京：科學出版社，1992．

［3］ 李 未．數理邏輯基本原理與形式推演［M］．北京：科學出版社，2007．

［4］ 陳意云．程序設計語言理論［M］．北京：高等教育出版社，2004．

［5］ 屈延文．形式語義學基礎與形式說明［M］．北京：科學出版社，2010．

［6］ HARTMUT E，FERNANDO O，BENJAMIN B，et．al．A component framework for system modeling based on high－level replacement systems［J］．Software and Systems Modeling，2004，3（2）：114－135．

［7］ NICOLAS W，ANDREW S．Towards formally template relational database representations in Z［J］．Abstract State Machines，2010，5 977：363－376．

［8］ FITZGERALD J，LARSEN P G，SAHARA S，et al．VDMTools：Advances in support for formal modeling in VDM［J］．Newsletter of ACM SIGPLAN Notices，2008，43（2）：3－11．

［9］ NARAYAN D，OSCAR T，GERMAN M，et al．Rigorous definition／specification in RAISE specification language of a framework for web services about geographic information systems［A］．IEEE Seventh International Conference on Information Technology［C］．Los Alamitos：IEEE Computer Society，2010．76－81．

［10］ LEE S，SLUIZER S．An executable language for modeling simple behavior［J］．IEEE Trans on SE，1991，17（6）：527－543．

［11］ SEUK B L，WU Xiao－qing，CAO Fei，et al．T－Clipse：An integrated development environment for two－level grammar［A］．ACM Proceedings of the 2003 OOPSLA Workshop on Eclipse Technology eXchange［C］．New York：［s．n．］，2003．89－93．

［12］ KLEYN M K，BROWNE J C．A high level language for specifying graph based languages and their programming environments［J］．IEEE Proc of 15th Intl Conf on SE，1993，20（5）：324－335．

［13］ JOHN V G，JAMES J H，JEANNETTE M W．The larch family of specification language［J］．IEEE Software，1985（1）：24－36．

［14］ MARKUS L．Confluence problems for trace rewriting systems［J］．Information and Computation，2001，170（1）：1－25．

［15］ GWEN S，ANDREA F，ANTONELLA C．Negotiation among web services using LOTOS／CADP［J］．Web Services，Lecture Notes in Computer Science，2004，3 250：198－212．

［16］ AMMAR A．An environment based on rewriting logic for parallel systems formal specification and prototyping［J］．Journal of Systems Architecture，1997，44（2）：79－105．

［17］ LUC J，LUC D，WILLY V P．An algebraic data type specification language and its rapid prototyping environment［A］．ACM Proceedings of the 11th International Conference on Software Engineering［C］．New York：［s．n．］，1989．74－84．

［18］ CONSTANT C，JERON T，MARCHAND H，et al．Integrating formal verification and conformance，testing for reactive systems［J］．IEEE Trans on SE，2007，33（8）：558－574．

［19］ 鄭紅軍，張乃孝．軟件開發中的形式化方法［J］．計算機科學（Journal of Computer Science ＆Technology），1997，24（6）：90－96．

［20］ 朱 冰，梅 宏，楊芙清．軟件開發過程中的形式化方法［J］．計算機科學（Journal of Computer Science ＆Technology），1995，22（1）：31－36．

［21］ JIM W，PETER G L，JUAN B，et al．Formal methods：Practice and experience［J］．Journal of ACM Computing Surveys，2009，41（4）：1－40．

［22］ BOWEN J P，HINCHEY M G．Ten commandments of formal methods…ten years later［J］．IEEE Journals of Computer，2006，39（1）：40－48．

Application of formal methods to software engineering

MIAO De－cheng1，FENG Li－bo2
（1．College of Mathematics and Information Science，Shaoguan University，Shaoguan Guangdong 512000，China；2．College of Sciences，Hebei University of Science and Technology，Shijiazhuang Hebei 050018，China）

This paper discusses briefly some basic concepts of formal method，and studies mainly its mathematical theory foundation and its application in each stage of software engineering．The paper also analyzes advantages，limitations of formal method as well as their respective reasons in theoretical research and engineering practice，then points out some future developing directions of formal method，and finally makes a brief evaluation of applying formal method to software engineering．

formal method；software specification formal language；software engineering；formal system；specification

TP301

A

1008－1542（2011）06－0575－05

2011－08－29；責任編輯：張 軍

廣東省科技計劃資助項目（2009B050700008）；韶關學院科研資助項目（2010－207－04）

苗德成（1979－），男，黑龍江伊春人，講師，博士，主要從事軟件系統形式化理論、形式語義學方面的研究。