摘要：為提高裝備管理軟件開發效能，本文將形式化方法與軟件工程化思想有機結合，給出了基于Z語言的裝備管理業務基礎軟件平臺的體系結構和設計，并基于Z-EMP平臺開發了AA-MIS原型系統，驗證了Z-EMP平臺的研究方向和設計思想是正確可行的，為解決裝備管理信息系統軟件開發問題提供了一種思路和方法。

關鍵詞：形式化方法；Z語言；業務基礎軟件平臺；軟件工程；裝備管理

中圖分類號：TP301.2 文獻標識碼：A

1 緒論

伴隨武器裝備建設的快速發展，裝備管理流程化、規范化的迫切需要，裝備管理信息系統在現代裝備保障中的作用日益突出。為適應裝備管理模式持續改革、裝備管理業務不斷升級的需要，裝備管理信息系統軟件必須持續升級快速更新。但由于軟件規模增大、復雜度增加，開發進度嚴重滯后、經費失控、質量糟糕等問題十分突出，傳統的開發方法已不能適應業務需求加速變化的形勢需要。

解決和處理軟件開發問題有兩大方法。軟件工程方法建立了多種軟件開發過程模型，從不同角度解決軟件開發問題，試圖控制進度、成本，提高軟件質量。但由于需求描述不清、理解有誤而導致的改正成本成指數增加，開發問題積重難返。形式化方法[1]為準確描述需求提供了一種全新而有效的技術途徑，但該方面的研究限于理論研究層面多，在實際工業項目的應用相對較少。

本文將形式化方法與軟件工程化思想有機結合，以工作流引擎和規則引擎技術為支撐，基于Z語言構建了裝備管理業務基礎軟件平臺，通過形式化方法精確描述業務需求、業務基礎平臺加速軟件開發進程、自動化測試提升軟件質量，探索解決裝備管理軟件開發問題的途徑。

2 研究現狀及存在問題

軟件開發問題主要分為理論方法和技術方法兩大基本研究方向。技術方法以軟件工程化研究為主，按照“軟件工廠”模式提高軟件生產效率，實用性很強，得到了產業界的廣泛支持。隨著軟件的規模越來越大，復雜度越來越高，很難保證軟件的可靠性和軟件的開發效率。理論方法以形式化方法研究為主，目標是使系統具有較高的可信度和正確性，但實用性較差，難以投入實際應用。

2.1軟件工程方法

1968年NATO提出“運用系統的、規范的和可定量的方法來開發、運行和維護軟件”的工程化思想，主要包括方法、工具和過程三大要素。四十多年來，軟件工程雖然取得豐碩成果，但進度安排和成本估算不準，需求不清、變動大，質量低、難維護等問題依然日益嚴重，軟件需求、開發進度管理和軟件質量已成為軟件工程化面臨的三個主要難題。

上世紀八十年代中期軟件需求工程[2]被提出，Herb Krasner給出了需求工程五階段生命周期的定義，Matthias Jarke和Klaus Pohl給出了需求工程包括獲取、表示和驗證三階段的生命周期定義。需求工程逐漸成為研究熱點問題之一。“基于知識的需求工程”[3]把AI （Artificial Intelligence，人工智能）技術應用到需求工程領域，具有一個知識庫和推理機制，在此基礎上進行需求分析，檢測其活動。美國南加州大學開發的一個基于知識的需求檢測工具QARCC。“形式化需求分析方法”[4]是使用一種形式化語言進行語言公式的形式推理，用于檢查語法的良構性并證明某些屬性，其主要優勢在于可以減少二義性、提高準確性、為驗證打好基礎、允許對需求進行推理等。

為解決開發進度問題，軟件設計方法方面的研究成果眾多，可分為重量級方法和輕量級方法。重量級方法產生大量的正式文檔，強調以開發過程為中心，主要包括ISO9000、CMM和統一軟體開發過程（RUP）等。輕量級方法沒有對大量正式文檔的要求，主要包括“極限編程”和“敏捷流程”等。面向方面的程序設計（AOP）被認為是近年來另外一個重要發展方向。

為解決軟件質量問題，以軟件測試為主要研究方向取得飛速發展。統計表明：在典型的軟件開發項目中，測試工作量往往占軟件開發總工作量的40%以上[5]。軟件測試階段在整個軟件開發周期中所占的比重日益增大。軟件測試環境復雜、分析工作量大，手工測試效率低，自動化測試逐漸取代手工方式成為主流測試方法。自動化測試具有效率高、成本低、效果好、可以復用等優點。自動化測試工具主要有Robot、Winrunner和QACenter等。此外，采用形式化方法描述并證明軟件需求形式化規格說明，通過程序正確性證明、形式化推理分析、模型檢驗等方法證明軟件正確并提高軟件的質量，但這些方法處于研究階段較多，存在一定的局限性，還沒有達到工程化應用要求，軟件測試仍將是提高軟件質量的重要方法。

2.2形式化方法

形式化方法（Formal Method）是建立在嚴格數學基礎上的軟件開發方法，以精確的語義描述軟件系統，在此基礎上進行自動生成、轉化及驗證。20世紀60年代“軟件危機”以來，在推動軟件工程化以外，形式化方法的研究及應用也取得了長足發展。

形式化方法通常可分為五類[6]：（1）基于模型的方法，如：Z、Object-Z、VDM、B等。（2） 代數方法，如：OBJ、Larch規約語言、CLEAR等。（3）過程代數方法，如：通信順序過程CSP、通信系統演算CCS、通信過程代數（ACP）、計時CSP（TCSP）、時序排序規約語言（LOTOS）等。（4）基于邏輯的方法，如：時序邏輯、Hoare邏輯等。（5）基于網絡的方法，如：Petri網、狀態圖等。

形式化方法的應用可分為三個層次[7]：形式規格說明、用形式化開發和形式化校驗產生程序和完全使用機器校驗的定理證明。形式化方法在開發大型軟件系統和解決特殊問題等方面存在局限性，且缺乏工具支持，但形式化方法對于改進軟件質量是十分重要的，一定會成為解決軟件開發問題的有效途徑之一。

2.3業務基礎軟件平臺

信息管理系統復雜、業務需求變化頻繁、工程量大。傳統開發模式是在底層技術平臺上直接構建系統，特點是編碼式開發和一次性開發持續運行，因此導致軟件僵化，業務組件無法重構，效率低下。現代開發模式要求按需求定制；組件化設計，實現軟件復用；易調整，可配置，實現柔性設計；開放性架構與標準化接口，實現持續集成等。各類應用系統開發實踐逐漸形成了基于平臺的快速開發方法。業務基礎軟件平臺[8]主要指以業務導向和驅動、可快速構建應用軟件的開發平臺，是業務管理類應用軟件的通用基礎平臺，主要產品有：用友UAP、普元EOS、金蝶BOS、東軟金算盤UP和E6，以及SAP NetWeaver等。

2.4Z語言

Z語言[9]是基于一階謂詞邏輯和集合論的形式規約說明語言，適合用于編寫計算機系統規格說明，主要特點是：可推理和證明、是結構化的、可使用自然語言、和模型可求精實現，不足是缺乏關于計時或并發行為的描述能力。

Z語言形式規約是一個強類型系統。Z形式規約的數據類型可分為基本類型和復合類型。Z形式規約的構型主要包括抽象狀態構型、操作構型、聲明使用構型、謂詞使用構型、重命名構型和類屬構型等，其中最主要的是說明軟件系統的狀態構型和說明狀態轉化的操作構型。

構型由聲明和謂詞兩部分組成，有水平和垂直兩種表示形式。水平形式：[聲明|謂詞]；垂直形式可理解性和可讀性更強：

2.5存在的主要問題

可以看出，軟件開發過程存在的主要問題包括：

（1）形式化方法在軟件開發過程中的應用還不普及，對需求表述研究應用的多，對軟件需求到軟件代碼自動化轉換研究的少，進展不明顯。

（2）業務基礎平臺的發展取得了很大進步，尤其以工作流技術為核心的平臺實現了面向功能到面向業務過程的變化，針對業務規則的配置修改變得靈活了，但業務規則的提取依然復雜，軟件開發過程依然很繁瑣，自動化程度很低。

（3）形式化方法與業務基礎平臺的結合研究尚未開展，仍然沒有兩者良好結合的應用實例。

3 平臺體系結構與設計

（1）Z語言的引入

業務基礎軟件平臺將非功能性需求通過系統基礎功能模塊的形式實現，在統一的需求分析、設計開發和高強度產品級測試的基礎上，對質量提供有力保證，并通過持續的更新升級以進一步提升質量。功能性需求受到裝備發展、管理理念和思想的進步等因素影響，處于不斷的變化發展之中。基于業務流程和業務規則的業務基礎軟件平臺，將流程和規則與軟件分離，具備流程自定義和規則自維護能力，提高了應對軟件變化的能力。基于流程圖和自然語言的業務需求描述不精確的問題依然存在，伴隨需求的變化更新，錯誤的累積效應將放大顯現。引入Z語言的形式化方法精確描述業務需求，形成與業務流程和業務規則的轉換機制，將為解決軟件開發問題提供一種新的方法途徑。

（2）Z-EMP平臺體系結構

Z-EMP平臺設計理念是：針對功能性業務需求發展變化大、規則復雜，引入形式化方法消除需求的不確定性，通過求精轉換技術，結合工作流引擎和規則引擎，形成可運行的系統業務功能；針對非功能性業務需求變化小、實現負雜，基于基礎軟件平臺的系統公共功能，通過功能模塊組合，形成可運行的系統公共功能。

Z-EMP平臺綜合運用工作流管理系統、商用智能和規則引擎等技術，通過形式化方法準確描述業務需求，求精轉化為業務流程和業務規則，基于規則引擎和工作流引擎等運行平臺運行，形成裝備管理軟件系統。

業務基礎軟件平臺的體系結構如圖1所示，分為用戶接口層、引擎層、業務邏輯層和持久化層。用戶接口層是一個軟件平臺最重要的組成之一，是用戶和軟件平臺交流的媒介。引擎層是業務基礎軟件平臺的核心，綜合運用工作流引擎JBPM和規則引擎Droofs，協調調度業務流程和業務邏輯API接口。業務邏輯層是業務基礎軟件平臺的業務支撐層，逐步固化和組合業務邏輯API接口供引擎層調度。持久化層通過對象關系映像技術ORM（Object/Realtional Mapper）來進行數據持久化。

（3）Z-EMP平臺設計

Z-EMP平臺包括四個部分：需求分析平臺、快速開發平臺、運行支撐平臺和測試平臺，從軟件生命周期來看，涵蓋了需求分析、設計、編碼、測試、部署運營等多個階段。 軟件開發人員從輸入形式化需求規格到完成測試整個軟件開發過程的大部分工作均可提供支持。該平臺的實現在滿足快速開發和靈活定制需求的前提下，還應當注重實用性、經濟性、可行性，因此應利用一些開源軟件，在此基礎上進一步擴展提升，為平臺的開發提供支持。

平臺的技術方案總體考慮如下：

（l）平臺總體采用J2EE架構。J2EE具有跨平臺、可伸縮、靈活、易維護等特點，作為平臺的開發體系具有獨特的優勢。

（2）通用環境支持常用開源及商用數據庫和服務器。通用環境支持是保證基于平臺的應用快速完成開發、部署的重要基礎，應該盡可能多的提供對這些服務器和數據庫的支持，供用戶按需配置。

（3）平臺通用語言采用JAVA，接口和配置文件采用XML語言。

（4）平臺開發工具以Eclipse為主，結合其他專用工具。基于Java、開源的Eclipse可擴展開發平臺是主流的Java開發工具之一。Eclipse開發工具提供了主框架和一組服務，用于組件化構建開發環境，通過加入組件用戶可無約束的擴展功能，這正好也符合了業務基礎軟件平臺運行環境多變和功能特別復雜的需要。其他專用工具有Ant和FreeMaker擴展引擎開發工具和JDK、Tomcat和Mysql等基本運行環境專用軟件。

3.4.1需求分析平臺設計

需求分析平臺通過對預置的形式化需求規范的擴展分析，以流程描述為基礎，以基于Z語言的形式化需求描述為核心，提供完整的需求分析報告。圖2給出了需求分析平臺模塊整體設計結構圖。

需求分析平臺用于設計開發人員與業務人員溝通交流業務需求并形成需求規范的一套工具組件，其基本工作流程是：

（1）獲取分析業務對象，構建對象集。

（2）狀態構型描述。

（3）獲取分析業務操作，構建操作集。

（4）操作流程分析，操作構型描述。

（5）構建聲明集，聲明構型描述。

（6）構建謂詞集，謂詞構型描述。

（7）組合構型和框架構型描述。

（8）引用模板生成形式化需求文檔。

（9）Z類型檢查，形式化分析推理，修正形式化需求。

平臺需求的形式化分析與設計主要將平臺化裝備管理需求通過形式化分析與設計形成形式化需求模板，將裝備管理信息系統的功能需求抽象形成裝備管理基礎業務軟件平臺的通用需求，使用Z語言進行形式化描述，構成形式化需求模板的基礎文件。形式化需求模板是Z-EMP需求分析平臺的組成部分，由平臺一同管理維護。用戶使用平臺進行信息系統的需求分析時，只在模板基礎上，進一步分析描述特殊需求。

形式化需求模板引用的方法和主要內容。引用形式化需求模板時，用戶只需選擇引用形式化需求模板，即可將平臺內建的形式化需求描述全部繼承，并在此基礎上，進一步進行需求分析和描述，并形成Z語言描述的形式化需求文檔。Z語言編輯器采用Z/EVES2.1工具，遵循該編輯的符號規范。

3.4.2快速開發平臺設計

快速開發平臺包括布局定義、流程定義和規則抽取三大模塊。布局定義模塊通過布局定義設計應用系統的用戶界面，并與后端處理的業務邏輯組件接口關聯，形成基本的操作應用。流程定義模塊通過業務流程的圖形化定義，將孤立、單一的業務處理活動按照業務需求構造成業務活動流程，基于工作流引擎驅動流程的運行。規則抽取模塊以形式化需求描述為基礎，通過規則抽取與轉換等一系列操作步驟，將業務規則固化形成規則庫，基于規則引擎驅動業務規則的注入與運行。對一些特殊的業務規則和業務邏輯，開發用戶應繼續擴展編寫有關代碼，實現業務功能。規則抽取與應用依賴于規則引擎系統，采用開源Drools規則引擎系統實現規則注入、解析與應用等，是快速開發平臺實現的關鍵技術問題。

快速開發分為引擎驅動和生成源代碼兩種基本模式。引擎模式是指通過開發平臺設計出應用模板并發布到平臺引擎，運行時，平臺引擎驅動應用模板設計的相關業務操作，完成業務處理過程。生成源代碼模式主要通過一個開發平臺的設計器定義業務模塊，輔助生成源代碼框架，用戶基于源代碼框架繼續編寫、修改源代碼實現業務邏輯。

本平臺快速開發模式綜合了兩種基本模式的優點，以引擎模式實現裝備管理業務流程、通用業務邏輯和業務規則的快速開發，以生成組件代碼模式提供進一步修改業務邏輯組件的擴展接口，實現特殊業務邏輯的快速開發，大大提高了開發效率。

快速開發流程如圖3所示。

3.4.3運行支撐平臺設計

運行支撐平臺也稱為運行時框架，是應用系統運行的支撐環境，包括應用系統支持環境和數據支撐環境，主要包括：用戶接口（界面層）組件、工作流引擎組件、規則引擎組件、業務邏輯組件、業務規則組件、持久化組件等，共同協作為應用系統的運行提供基礎支持。

應用系統運行支撐環境基于Tomact6.0構建。為提高Z-EMP平臺應用系統環境的適應性，應用系統設計時，一是自動繼承服務器基礎應用環境，二是要提供環境自定義接口，自主選擇運行環境配置參數。

用戶類型不同，對數據庫的使用需求也將不同。數據支撐環境應支持不同的數據庫系統，如Oracle、MS SQL server、DB2、Postgresql和Mysql等。此外，還應具有在不同類型的數據庫系統之間實現遷移的能力。Z-EMP平臺提供的數據庫支持環境能夠隱藏不同類型數據庫系統之間的差別，對于平臺來說數據庫系統是透明的。

3.4.4測試平臺設計

一個完善的自動化測試系統一般會包括：生成測試用例、測試用例接口、驅動被測軟件程序、主控程序、記錄出錯步驟、bug庫等，其中，生成測試用例模塊是自動化測試系統的主要難點[10]。測試用例對達成測試目的來說是至關重要的。好的測試用例可以提高測試的質量和工作效率。可以說，生成完備的、恰當的測試用例是整個測試平臺設計的重要內容。

測試平臺設計依據形式化需求規格說明生成測試用例遵循狀態覆蓋準則和狀態變遷覆蓋準則。狀態覆蓋準則依據形式化需求規格說明，設計足夠多的測試用例使的狀態構型中的所有狀態在測試用例套中至少出現一次。狀態變遷覆蓋準則依據形式化需求規格說明，設計足夠多的測試用例保證抽象狀態構型中的狀態轉換全部覆蓋，或者說最少確保有一個測試用例能夠覆蓋測試狀態轉換過程一次。

測試平臺測試基于形式化需求Z語言規格說明自動生成測試用例，主要分三步：

（1）預處理用Z語言描述的形式化規格說明，識別出輸入變量和輸出變量的約束條件，以及變量之間的約束關系，并簡化轉換成線性謂詞。

（2）以線性謂詞為基礎轉換為線性不等式組，求解線性不等式組以得到對應取值范圍的邊界極點。

（3）找出取值范圍的邊界附近的點，進行輸出變量到輸入變量的逆變換以最終得到測試用例。

4 平臺應用實現與驗證

Z-EMP平臺是采用形式化方法和快速開發平臺兩種技術路線綜合解決軟件開發問題的研究型平臺，將形式化方法和軟件工程化方法有機結合，將形式化方法拓展延伸到了設計開發階段，這一基本思路實現了快速開發平臺的敏捷性與形式化方法的準確性統一。基于Z-EMP平臺的軟件開發是一種全新的軟件開發新思維，開發流程如圖4所示。

AA-MIS系統是裝備全壽命管理信息系統，從裝備籌措、儲存、保管、維修、訓練、使用到報廢全業務過程，使用對象為機關和部隊相關工作人員。該系統設計裝備型號多、涉及保障單位分布廣，業務復雜、專業性強等諸多特點，而且當前武器裝備建設出于轉型發展階段，新裝備新型號陸續裝備部隊。裝備管理需求處于不斷變化發展之中，基于傳統開發模式開發的信息系統已經不適應當前使用需求，必須形成軟件持續優化和快速服務能力以保證軟件服務質量，有效完成裝備效能化管理使命。

基于Z-EMP平臺開發的AA-MIS系統主要完成了業務流程的圖形化快速定義，適應業務流程的變化發展；業務規則復雜的質量控制模塊的形式化描述，開發了質量控制整套邏輯接口組件，具備了基于平臺快速實現形式化需求的能力；基于形式化需求輔助生成了部分測試用例，實際應用到系統的測試過程，尤其在邏輯覆蓋測試上發揮了一定作用。AA-MIS系統的開發應用較好了驗證了Z-EMP平臺研究方向的正確性和平臺實現的可能性。

5 總結

本文首先分析了軟件工程和形式化方法的優勢和不足，介紹了業務基礎軟件平臺的思想，首次提出將形式化方法和Z語言引入到快速開發平臺綜合解決軟件需求與開發的問題，給出了Z-EMP平臺體系結構和總體設計，最后結合AA-MIS系統開發，驗證了Z-EMP平臺的研究方向和設計思想，Z-EMP平臺適合作為裝備管理業務基礎軟件平臺持續開展研究，以解決裝備管理信息系統軟件開發問題。

由于客觀原因，基于Z語言的業務基礎平臺的研究僅僅是一個初步的探索與嘗試，許多認識與思考還很粗淺。在形式規范重用和Z語言工具等方面，需要進一步加強研究。

參考文獻：

[1] 李瑩，吳江琴.軟件工程形式化方法與語言[M].杭州：浙江大學出版社，2010，3-4.

[2] 吳軍華.軟件工程—理論、方法與實踐[M].西安：西安電子科技大學出版社，2010，1-17，58-73.

[3] Karl E. Wiegers.陸麗娜，等，譯.軟件需求（Software Requirements）[M].北京：機械工業出版社，2000，42-65.

[4] 夏建勛，唐紅武.需求分析的Z語言形式化方法[J].科學技術與工程，2008，8（8）：2245-2248.

[5] PATTON R.軟件測試[M].北京：機械工業出版社，2002，1-96.

[6] Barroca L.M，Mcdermid J.A，Formal methods： Use and Relevance for The Development of Safety Critical Systems[J].The Computer Journal，1992，35：579-599.

[7] 蔡立志.基于形式化的軟件測試復用若干關鍵技術的研究[D].上海大學，2009.

[8] 閆中玉.基于業務基礎軟件平臺的企業建模方法的研究與應用[D].江蘇大學，2007.

[9] 王宏生.Z形式規約的自動求精研究[M].北京：國防工業出版社，2009，15-16.

[10] 鄒北驥，等.基于形式規約的軟件測試用例自動生成技術研究[J].湖南大學學報（自然科學版），2004，31（3）：81-85.

作者簡介：

孫桂領（1980-），男，工程師，碩士.主要研究領域：形式化建模

與應用、軟件工程、裝備管理、信息系統與信息管理等.

沈堅平（1963-），男，高級工程師，博士.主要研究領域：軍事裝

備、作戰使用、信息系統與信息管理等.