基于Z语言的装备管理业务基础软件平台研究

打开文本图片集

摘要：为提高装备管理软件开发效能，本文将形式化方法与软件工程化思想有机结合，给出了基于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、Wiunner和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-），男，高级工程师，博士.主要研究领域：军事装

备、作战使用、信息系统与信息管理等.

推荐访问:装备 语言 业务 基础 研究