摘要：為提高裝備管理軟件開發(fā)效能，本文將形式化方法與軟件工程化思想有機(jī)結(jié)合，給出了基于Z語言的裝備管理業(yè)務(wù)基礎(chǔ)軟件平臺(tái)的體系結(jié)構(gòu)和設(shè)計(jì)，并基于Z-EMP平臺(tái)開發(fā)了AA-MIS原型系統(tǒng)，驗(yàn)證了Z-EMP平臺(tái)的研究方向和設(shè)計(jì)思想是正確可行的，為解決裝備管理信息系統(tǒng)軟件開發(fā)問題提供了一種思路和方法。

關(guān)鍵詞：形式化方法；Z語言；業(yè)務(wù)基礎(chǔ)軟件平臺(tái)；軟件工程；裝備管理

中圖分類號(hào)：TP301.2 文獻(xiàn)標(biāo)識(shí)碼：A

1 緒論

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

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

本文將形式化方法與軟件工程化思想有機(jī)結(jié)合，以工作流引擎和規(guī)則引擎技術(shù)為支撐，基于Z語言構(gòu)建了裝備管理業(yè)務(wù)基礎(chǔ)軟件平臺(tái)，通過形式化方法精確描述業(yè)務(wù)需求、業(yè)務(wù)基礎(chǔ)平臺(tái)加速軟件開發(fā)進(jìn)程、自動(dòng)化測試提升軟件質(zhì)量，探索解決裝備管理軟件開發(fā)問題的途徑。

2 研究現(xiàn)狀及存在問題

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

2.1軟件工程方法

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

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

為解決開發(fā)進(jìn)度問題，軟件設(shè)計(jì)方法方面的研究成果眾多，可分為重量級(jí)方法和輕量級(jí)方法。重量級(jí)方法產(chǎn)生大量的正式文檔，強(qiáng)調(diào)以開發(fā)過程為中心，主要包括ISO9000、CMM和統(tǒng)一軟體開發(fā)過程（RUP）等。輕量級(jí)方法沒有對大量正式文檔的要求，主要包括“極限編程”和“敏捷流程”等。面向方面的程序設(shè)計(jì)（AOP）被認(rèn)為是近年來另外一個(gè)重要發(fā)展方向。

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

2.2形式化方法

形式化方法（Formal Method）是建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上的軟件開發(fā)方法，以精確的語義描述軟件系統(tǒng)，在此基礎(chǔ)上進(jìn)行自動(dòng)生成、轉(zhuǎn)化及驗(yàn)證。20世紀(jì)60年代“軟件危機(jī)”以來，在推動(dòng)軟件工程化以外，形式化方法的研究及應(yīng)用也取得了長足發(fā)展。

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

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

2.3業(yè)務(wù)基礎(chǔ)軟件平臺(tái)

信息管理系統(tǒng)復(fù)雜、業(yè)務(wù)需求變化頻繁、工程量大。傳統(tǒng)開發(fā)模式是在底層技術(shù)平臺(tái)上直接構(gòu)建系統(tǒng)，特點(diǎn)是編碼式開發(fā)和一次性開發(fā)持續(xù)運(yùn)行，因此導(dǎo)致軟件僵化，業(yè)務(wù)組件無法重構(gòu)，效率低下?，F(xiàn)代開發(fā)模式要求按需求定制；組件化設(shè)計(jì)，實(shí)現(xiàn)軟件復(fù)用；易調(diào)整，可配置，實(shí)現(xiàn)柔性設(shè)計(jì)；開放性架構(gòu)與標(biāo)準(zhǔn)化接口，實(shí)現(xiàn)持續(xù)集成等。各類應(yīng)用系統(tǒng)開發(fā)實(shí)踐逐漸形成了基于平臺(tái)的快速開發(fā)方法。業(yè)務(wù)基礎(chǔ)軟件平臺(tái)[8]主要指以業(yè)務(wù)導(dǎo)向和驅(qū)動(dòng)、可快速構(gòu)建應(yīng)用軟件的開發(fā)平臺(tái)，是業(yè)務(wù)管理類應(yīng)用軟件的通用基礎(chǔ)平臺(tái)，主要產(chǎn)品有：用友UAP、普元EOS、金蝶BOS、東軟金算盤UP和E6，以及SAP NetWeaver等。

2.4Z語言

Z語言[9]是基于一階謂詞邏輯和集合論的形式規(guī)約說明語言，適合用于編寫計(jì)算機(jī)系統(tǒng)規(guī)格說明，主要特點(diǎn)是：可推理和證明、是結(jié)構(gòu)化的、可使用自然語言、和模型可求精實(shí)現(xiàn)，不足是缺乏關(guān)于計(jì)時(shí)或并發(fā)行為的描述能力。

Z語言形式規(guī)約是一個(gè)強(qiáng)類型系統(tǒng)。Z形式規(guī)約的數(shù)據(jù)類型可分為基本類型和復(fù)合類型。Z形式規(guī)約的構(gòu)型主要包括抽象狀態(tài)構(gòu)型、操作構(gòu)型、聲明使用構(gòu)型、謂詞使用構(gòu)型、重命名構(gòu)型和類屬構(gòu)型等，其中最主要的是說明軟件系統(tǒng)的狀態(tài)構(gòu)型和說明狀態(tài)轉(zhuǎn)化的操作構(gòu)型。

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

2.5存在的主要問題

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

（1）形式化方法在軟件開發(fā)過程中的應(yīng)用還不普及，對需求表述研究應(yīng)用的多，對軟件需求到軟件代碼自動(dòng)化轉(zhuǎn)換研究的少，進(jìn)展不明顯。

（2）業(yè)務(wù)基礎(chǔ)平臺(tái)的發(fā)展取得了很大進(jìn)步，尤其以工作流技術(shù)為核心的平臺(tái)實(shí)現(xiàn)了面向功能到面向業(yè)務(wù)過程的變化，針對業(yè)務(wù)規(guī)則的配置修改變得靈活了，但業(yè)務(wù)規(guī)則的提取依然復(fù)雜，軟件開發(fā)過程依然很繁瑣，自動(dòng)化程度很低。

（3）形式化方法與業(yè)務(wù)基礎(chǔ)平臺(tái)的結(jié)合研究尚未開展，仍然沒有兩者良好結(jié)合的應(yīng)用實(shí)例。

3 平臺(tái)體系結(jié)構(gòu)與設(shè)計(jì)

（1）Z語言的引入

業(yè)務(wù)基礎(chǔ)軟件平臺(tái)將非功能性需求通過系統(tǒng)基礎(chǔ)功能模塊的形式實(shí)現(xiàn)，在統(tǒng)一的需求分析、設(shè)計(jì)開發(fā)和高強(qiáng)度產(chǎn)品級(jí)測試的基礎(chǔ)上，對質(zhì)量提供有力保證，并通過持續(xù)的更新升級(jí)以進(jìn)一步提升質(zhì)量。功能性需求受到裝備發(fā)展、管理理念和思想的進(jìn)步等因素影響，處于不斷的變化發(fā)展之中?；跇I(yè)務(wù)流程和業(yè)務(wù)規(guī)則的業(yè)務(wù)基礎(chǔ)軟件平臺(tái)，將流程和規(guī)則與軟件分離，具備流程自定義和規(guī)則自維護(hù)能力，提高了應(yīng)對軟件變化的能力?；诹鞒虉D和自然語言的業(yè)務(wù)需求描述不精確的問題依然存在，伴隨需求的變化更新，錯(cuò)誤的累積效應(yīng)將放大顯現(xiàn)。引入Z語言的形式化方法精確描述業(yè)務(wù)需求，形成與業(yè)務(wù)流程和業(yè)務(wù)規(guī)則的轉(zhuǎn)換機(jī)制，將為解決軟件開發(fā)問題提供一種新的方法途徑。

（2）Z-EMP平臺(tái)體系結(jié)構(gòu)

Z-EMP平臺(tái)設(shè)計(jì)理念是：針對功能性業(yè)務(wù)需求發(fā)展變化大、規(guī)則復(fù)雜，引入形式化方法消除需求的不確定性，通過求精轉(zhuǎn)換技術(shù)，結(jié)合工作流引擎和規(guī)則引擎，形成可運(yùn)行的系統(tǒng)業(yè)務(wù)功能；針對非功能性業(yè)務(wù)需求變化小、實(shí)現(xiàn)負(fù)雜，基于基礎(chǔ)軟件平臺(tái)的系統(tǒng)公共功能，通過功能模塊組合，形成可運(yùn)行的系統(tǒng)公共功能。

Z-EMP平臺(tái)綜合運(yùn)用工作流管理系統(tǒng)、商用智能和規(guī)則引擎等技術(shù)，通過形式化方法準(zhǔn)確描述業(yè)務(wù)需求，求精轉(zhuǎn)化為業(yè)務(wù)流程和業(yè)務(wù)規(guī)則，基于規(guī)則引擎和工作流引擎等運(yùn)行平臺(tái)運(yùn)行，形成裝備管理軟件系統(tǒng)。

業(yè)務(wù)基礎(chǔ)軟件平臺(tái)的體系結(jié)構(gòu)如圖1所示，分為用戶接口層、引擎層、業(yè)務(wù)邏輯層和持久化層。用戶接口層是一個(gè)軟件平臺(tái)最重要的組成之一，是用戶和軟件平臺(tái)交流的媒介。引擎層是業(yè)務(wù)基礎(chǔ)軟件平臺(tái)的核心，綜合運(yùn)用工作流引擎JBPM和規(guī)則引擎Droofs，協(xié)調(diào)調(diào)度業(yè)務(wù)流程和業(yè)務(wù)邏輯API接口。業(yè)務(wù)邏輯層是業(yè)務(wù)基礎(chǔ)軟件平臺(tái)的業(yè)務(wù)支撐層，逐步固化和組合業(yè)務(wù)邏輯API接口供引擎層調(diào)度。持久化層通過對象關(guān)系映像技術(shù)ORM（Object/Realtional Mapper）來進(jìn)行數(shù)據(jù)持久化。

（3）Z-EMP平臺(tái)設(shè)計(jì)

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

平臺(tái)的技術(shù)方案總體考慮如下：

（l）平臺(tái)總體采用J2EE架構(gòu)。J2EE具有跨平臺(tái)、可伸縮、靈活、易維護(hù)等特點(diǎn)，作為平臺(tái)的開發(fā)體系具有獨(dú)特的優(yōu)勢。

（2）通用環(huán)境支持常用開源及商用數(shù)據(jù)庫和服務(wù)器。通用環(huán)境支持是保證基于平臺(tái)的應(yīng)用快速完成開發(fā)、部署的重要基礎(chǔ)，應(yīng)該盡可能多的提供對這些服務(wù)器和數(shù)據(jù)庫的支持，供用戶按需配置。

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

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

3.4.1需求分析平臺(tái)設(shè)計(jì)

需求分析平臺(tái)通過對預(yù)置的形式化需求規(guī)范的擴(kuò)展分析，以流程描述為基礎(chǔ)，以基于Z語言的形式化需求描述為核心，提供完整的需求分析報(bào)告。圖2給出了需求分析平臺(tái)模塊整體設(shè)計(jì)結(jié)構(gòu)圖。

需求分析平臺(tái)用于設(shè)計(jì)開發(fā)人員與業(yè)務(wù)人員溝通交流業(yè)務(wù)需求并形成需求規(guī)范的一套工具組件，其基本工作流程是：

（1）獲取分析業(yè)務(wù)對象，構(gòu)建對象集。

（2）狀態(tài)構(gòu)型描述。

（3）獲取分析業(yè)務(wù)操作，構(gòu)建操作集。

（4）操作流程分析，操作構(gòu)型描述。

（5）構(gòu)建聲明集，聲明構(gòu)型描述。

（6）構(gòu)建謂詞集，謂詞構(gòu)型描述。

（7）組合構(gòu)型和框架構(gòu)型描述。

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

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

平臺(tái)需求的形式化分析與設(shè)計(jì)主要將平臺(tái)化裝備管理需求通過形式化分析與設(shè)計(jì)形成形式化需求模板，將裝備管理信息系統(tǒng)的功能需求抽象形成裝備管理基礎(chǔ)業(yè)務(wù)軟件平臺(tái)的通用需求，使用Z語言進(jìn)行形式化描述，構(gòu)成形式化需求模板的基礎(chǔ)文件。形式化需求模板是Z-EMP需求分析平臺(tái)的組成部分，由平臺(tái)一同管理維護(hù)。用戶使用平臺(tái)進(jìn)行信息系統(tǒng)的需求分析時(shí)，只在模板基礎(chǔ)上，進(jìn)一步分析描述特殊需求。

形式化需求模板引用的方法和主要內(nèi)容。引用形式化需求模板時(shí)，用戶只需選擇引用形式化需求模板，即可將平臺(tái)內(nèi)建的形式化需求描述全部繼承，并在此基礎(chǔ)上，進(jìn)一步進(jìn)行需求分析和描述，并形成Z語言描述的形式化需求文檔。Z語言編輯器采用Z/EVES2.1工具，遵循該編輯的符號(hào)規(guī)范。

3.4.2快速開發(fā)平臺(tái)設(shè)計(jì)

快速開發(fā)平臺(tái)包括布局定義、流程定義和規(guī)則抽取三大模塊。布局定義模塊通過布局定義設(shè)計(jì)應(yīng)用系統(tǒng)的用戶界面，并與后端處理的業(yè)務(wù)邏輯組件接口關(guān)聯(lián)，形成基本的操作應(yīng)用。流程定義模塊通過業(yè)務(wù)流程的圖形化定義，將孤立、單一的業(yè)務(wù)處理活動(dòng)按照業(yè)務(wù)需求構(gòu)造成業(yè)務(wù)活動(dòng)流程，基于工作流引擎驅(qū)動(dòng)流程的運(yùn)行。規(guī)則抽取模塊以形式化需求描述為基礎(chǔ)，通過規(guī)則抽取與轉(zhuǎn)換等一系列操作步驟，將業(yè)務(wù)規(guī)則固化形成規(guī)則庫，基于規(guī)則引擎驅(qū)動(dòng)業(yè)務(wù)規(guī)則的注入與運(yùn)行。對一些特殊的業(yè)務(wù)規(guī)則和業(yè)務(wù)邏輯，開發(fā)用戶應(yīng)繼續(xù)擴(kuò)展編寫有關(guān)代碼，實(shí)現(xiàn)業(yè)務(wù)功能。規(guī)則抽取與應(yīng)用依賴于規(guī)則引擎系統(tǒng)，采用開源Drools規(guī)則引擎系統(tǒng)實(shí)現(xiàn)規(guī)則注入、解析與應(yīng)用等，是快速開發(fā)平臺(tái)實(shí)現(xiàn)的關(guān)鍵技術(shù)問題。

快速開發(fā)分為引擎驅(qū)動(dòng)和生成源代碼兩種基本模式。引擎模式是指通過開發(fā)平臺(tái)設(shè)計(jì)出應(yīng)用模板并發(fā)布到平臺(tái)引擎，運(yùn)行時(shí)，平臺(tái)引擎驅(qū)動(dòng)應(yīng)用模板設(shè)計(jì)的相關(guān)業(yè)務(wù)操作，完成業(yè)務(wù)處理過程。生成源代碼模式主要通過一個(gè)開發(fā)平臺(tái)的設(shè)計(jì)器定義業(yè)務(wù)模塊，輔助生成源代碼框架，用戶基于源代碼框架繼續(xù)編寫、修改源代碼實(shí)現(xiàn)業(yè)務(wù)邏輯。

本平臺(tái)快速開發(fā)模式綜合了兩種基本模式的優(yōu)點(diǎn)，以引擎模式實(shí)現(xiàn)裝備管理業(yè)務(wù)流程、通用業(yè)務(wù)邏輯和業(yè)務(wù)規(guī)則的快速開發(fā)，以生成組件代碼模式提供進(jìn)一步修改業(yè)務(wù)邏輯組件的擴(kuò)展接口，實(shí)現(xiàn)特殊業(yè)務(wù)邏輯的快速開發(fā)，大大提高了開發(fā)效率。

快速開發(fā)流程如圖3所示。

3.4.3運(yùn)行支撐平臺(tái)設(shè)計(jì)

運(yùn)行支撐平臺(tái)也稱為運(yùn)行時(shí)框架，是應(yīng)用系統(tǒng)運(yùn)行的支撐環(huán)境，包括應(yīng)用系統(tǒng)支持環(huán)境和數(shù)據(jù)支撐環(huán)境，主要包括：用戶接口（界面層）組件、工作流引擎組件、規(guī)則引擎組件、業(yè)務(wù)邏輯組件、業(yè)務(wù)規(guī)則組件、持久化組件等，共同協(xié)作為應(yīng)用系統(tǒng)的運(yùn)行提供基礎(chǔ)支持。

應(yīng)用系統(tǒng)運(yùn)行支撐環(huán)境基于Tomact6.0構(gòu)建。為提高Z-EMP平臺(tái)應(yīng)用系統(tǒng)環(huán)境的適應(yīng)性，應(yīng)用系統(tǒng)設(shè)計(jì)時(shí)，一是自動(dòng)繼承服務(wù)器基礎(chǔ)應(yīng)用環(huán)境，二是要提供環(huán)境自定義接口，自主選擇運(yùn)行環(huán)境配置參數(shù)。

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

3.4.4測試平臺(tái)設(shè)計(jì)

一個(gè)完善的自動(dòng)化測試系統(tǒng)一般會(huì)包括：生成測試用例、測試用例接口、驅(qū)動(dòng)被測軟件程序、主控程序、記錄出錯(cuò)步驟、bug庫等，其中，生成測試用例模塊是自動(dòng)化測試系統(tǒng)的主要難點(diǎn)[10]。測試用例對達(dá)成測試目的來說是至關(guān)重要的。好的測試用例可以提高測試的質(zhì)量和工作效率?？梢哉f，生成完備的、恰當(dāng)?shù)臏y試用例是整個(gè)測試平臺(tái)設(shè)計(jì)的重要內(nèi)容。

測試平臺(tái)設(shè)計(jì)依據(jù)形式化需求規(guī)格說明生成測試用例遵循狀態(tài)覆蓋準(zhǔn)則和狀態(tài)變遷覆蓋準(zhǔn)則。狀態(tài)覆蓋準(zhǔn)則依據(jù)形式化需求規(guī)格說明，設(shè)計(jì)足夠多的測試用例使的狀態(tài)構(gòu)型中的所有狀態(tài)在測試用例套中至少出現(xiàn)一次。狀態(tài)變遷覆蓋準(zhǔn)則依據(jù)形式化需求規(guī)格說明，設(shè)計(jì)足夠多的測試用例保證抽象狀態(tài)構(gòu)型中的狀態(tài)轉(zhuǎn)換全部覆蓋，或者說最少確保有一個(gè)測試用例能夠覆蓋測試狀態(tài)轉(zhuǎn)換過程一次。

測試平臺(tái)測試基于形式化需求Z語言規(guī)格說明自動(dòng)生成測試用例，主要分三步：

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

（2）以線性謂詞為基礎(chǔ)轉(zhuǎn)換為線性不等式組，求解線性不等式組以得到對應(yīng)取值范圍的邊界極點(diǎn)。

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

4 平臺(tái)應(yīng)用實(shí)現(xiàn)與驗(yàn)證

Z-EMP平臺(tái)是采用形式化方法和快速開發(fā)平臺(tái)兩種技術(shù)路線綜合解決軟件開發(fā)問題的研究型平臺(tái)，將形式化方法和軟件工程化方法有機(jī)結(jié)合，將形式化方法拓展延伸到了設(shè)計(jì)開發(fā)階段，這一基本思路實(shí)現(xiàn)了快速開發(fā)平臺(tái)的敏捷性與形式化方法的準(zhǔn)確性統(tǒng)一?；赯-EMP平臺(tái)的軟件開發(fā)是一種全新的軟件開發(fā)新思維，開發(fā)流程如圖4所示。

AA-MIS系統(tǒng)是裝備全壽命管理信息系統(tǒng)，從裝備籌措、儲(chǔ)存、保管、維修、訓(xùn)練、使用到報(bào)廢全業(yè)務(wù)過程，使用對象為機(jī)關(guān)和部隊(duì)相關(guān)工作人員。該系統(tǒng)設(shè)計(jì)裝備型號(hào)多、涉及保障單位分布廣，業(yè)務(wù)復(fù)雜、專業(yè)性強(qiáng)等諸多特點(diǎn)，而且當(dāng)前武器裝備建設(shè)出于轉(zhuǎn)型發(fā)展階段，新裝備新型號(hào)陸續(xù)裝備部隊(duì)。裝備管理需求處于不斷變化發(fā)展之中，基于傳統(tǒng)開發(fā)模式開發(fā)的信息系統(tǒng)已經(jīng)不適應(yīng)當(dāng)前使用需求，必須形成軟件持續(xù)優(yōu)化和快速服務(wù)能力以保證軟件服務(wù)質(zhì)量，有效完成裝備效能化管理使命。

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

5 總結(jié)

本文首先分析了軟件工程和形式化方法的優(yōu)勢和不足，介紹了業(yè)務(wù)基礎(chǔ)軟件平臺(tái)的思想，首次提出將形式化方法和Z語言引入到快速開發(fā)平臺(tái)綜合解決軟件需求與開發(fā)的問題，給出了Z-EMP平臺(tái)體系結(jié)構(gòu)和總體設(shè)計(jì)，最后結(jié)合AA-MIS系統(tǒng)開發(fā)，驗(yàn)證了Z-EMP平臺(tái)的研究方向和設(shè)計(jì)思想，Z-EMP平臺(tái)適合作為裝備管理業(yè)務(wù)基礎(chǔ)軟件平臺(tái)持續(xù)開展研究，以解決裝備管理信息系統(tǒng)軟件開發(fā)問題。

由于客觀原因，基于Z語言的業(yè)務(wù)基礎(chǔ)平臺(tái)的研究僅僅是一個(gè)初步的探索與嘗試，許多認(rèn)識(shí)與思考還很粗淺。在形式規(guī)范重用和Z語言工具等方面，需要進(jìn)一步加強(qiáng)研究。

參考文獻(xiàn)：

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

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

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

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

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

[6] Barroca L.M，Mcdermid J.A，F(xiàn)ormal methods： Use and Relevance for The Development of Safety Critical Systems[J].The Computer Journal，1992，35：579-599.

[7] 蔡立志.基于形式化的軟件測試復(fù)用若干關(guān)鍵技術(shù)的研究[D].上海大學(xué)，2009.

[8] 閆中玉.基于業(yè)務(wù)基礎(chǔ)軟件平臺(tái)的企業(yè)建模方法的研究與應(yīng)用[D].江蘇大學(xué)，2007.

[9] 王宏生.Z形式規(guī)約的自動(dòng)求精研究[M].北京：國防工業(yè)出版社，2009，15-16.

[10] 鄒北驥，等.基于形式規(guī)約的軟件測試用例自動(dòng)生成技術(shù)研究[J].湖南大學(xué)學(xué)報(bào)（自然科學(xué)版），2004，31（3）：81-85.

作者簡介：

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

與應(yīng)用、軟件工程、裝備管理、信息系統(tǒng)與信息管理等.

沈堅(jiān)平（1963-），男，高級(jí)工程師，博士.主要研究領(lǐng)域：軍事裝

備、作戰(zhàn)使用、信息系統(tǒng)與信息管理等.