软件设计开发本栏目责任编辑：谢媛媛Computer Knowledge and Technology 电脑知识与技术第5卷第19期(2009年7月)形式化与UML 结合的建模方法及其应用舒良春，肖美华（南昌大学计算中心，江西南昌330031）摘要：首先阐述了形式化方法与可视化方法的优缺点，并在此基础上提出软件体系结构形式化与可视化UML 互补的建模方法，主要探讨UML 和Z 结合的建模过程，并用一个系统开发实例进行展示。
关键词：UML ；Z ；形式化方法；软件体系结构建模中图分类号：TP311文献标识码：A 文章编号：1009-3044(2009)19-5167-03Combination of Formalization and UML Modeling Method and its ApplicationSHU Liang-chun,XIAO Mei-hua(Computing Center,Nanchang University,Nanchang 330031,China)Abstract:First of all,express the advantages and disadvantages of the formalization and visualization methods,then based on this,bring for -word the software architecture method ,focused on the modeling process of the combination of UML and Z ,and finally use an example to display.Key words:UML;Z;formalization methods;software architecture modeling在目前通用的软件开发方法中，其描述通常还是非形式化的方法和工具。
然而这种非形式化的方法并不能很好地描述不同组成系统之间的一些特性，已经难以适应软件体系结构研究的进一步发展。
因此，在软件体系结构的研究过程中必须要有能显示描述、有独立性的形式化研究工具。
形式化方法作为一种严格以数学为基础的方法，能够清晰、精确、抽象、简明地规范和验证软件系统及其性质，帮助发现其它方法不容易发现的系统描述的不一致，不明确或不完整，有助于增加软件开发人员对系统的理解，因而形式化方法能够极大地提高软件的安全性和可靠性。
UML 作为一种通用的对象建模语言，经过了十几年的不断使用、修改、发展和完善，现在逐渐趋于成熟，已成为在软件工业中占支配地位的建模语言，并在许多领域的软件开发中得到应用。
但UML 对软件体系结构建模时，缺少分析体系结构所需的准确语义，多视角建模视图之间也存在不一致性，这使得对模型难以进行一致性检查和正确性分析，进而限制了它的有效性。
并且。
这些非形式化特征使开发者无法从中看出设计的优劣，不利于对系统优劣的度量，不能帮助开发人员评估和改进。
因此，UML 结合形式化的建模方法是解决UML 非形式化缺陷的重要途径之一，并将对软件系统的开发具有重大的研究价值。
本文将在对前人关于软件体系结构的形式化方法分析研究的基础上，结合可视化的UML 技术，构造一种新的软件体系结构建模方法。
1软件体系结构建模方法概述形式化描述和可视化描述是目前主要的两类软件体系结构描述方法。
其中，形式化描述以体系结构描述语言ADL 为代表，可视化描述以统一建模语言UML 为代表。
[1]1）形式化描述软件体系结构软件工程中的形式化方法就是依靠数学模型和计算来描述和验证一个目标软件系统的行为和特性，包括需求规格、设计和实现等，其最根本的一点就是建立在严格的数学基础上。
使用形式化方法可以帮助开发者获得对其所描述的系统的深刻而正确的理解，发现并及时更正设计中的错误和缺陷。
软件开发中的形式化方法主要是形式化规范说明语言，目前广泛应用的一些形式语言，如Z 、VDM ，B 、CSP 、Temporal Logic 、ITL 、Petri 图等，这些形式化方法在功能上各有侧重，可以互补。
z 语言是由英国Oxford 大学程序研究组PRG 的Jean Raymond Abrial 、Bernard Sufrin 等人设计的一种基于一阶谓词逻辑和集合论的形式规格说明语言，它采用了严格的数学理论，可以产生简明、精确、无歧义且可证明的规格说明[2]。
z 语言是一种功能很强的形式规格说明语言，可以保证其书写的规格说明文档的正确性，同时还能保证有很好的可读性和可理解性。
Z 语言是迄今为止应用最为广泛的形式化语言之一，软件企业在软件开发，特别是大型软件的开发中经常采用z 语言进行需求分析，以产生形式化、精确的需求规格说明。
本论文实例分析中的××省电力公司EHR 人力资源系统是一个大型的人力资源管理系统，因而将采用Z 语言这样一个最为适宜的形式化方法。
2）可视化描述软件体系结构UML 是一种将软件开发过程中出现的各种模型用可视化图形来描述的语言，它融合了多种面向对象开发方法的优点，采用统一的图形和符号从多个视角描述软件系统的各种抽象模型，获得了国际标准化组织的认可，并被国际软件界广泛接纳。
但是随着软件规模和复杂性不断增大，UML 的不足就逐渐暴露出来了。
这是由于复杂系统的建模往往需要严格的语义分析，而UML 却缺乏准确的语义，这使得对软件体系结构的可构造性建模能力较弱，缺乏形式化语义，对体系结构的描述只能到达非形式化的层次，不利于系统的求精和验证。
收稿日期：2009-04-09基金项目：2008年江西省研究生创新专项资金省教育厅资助项目-网络协议安全性分析及支撑工具研究（YC08A032）ISSN 1009-3044Computer Knowledge and Technology电脑知识与技术Vol.5,No.19,July 2009,pp.5167-5169E-mail:xsjl@ Tel:+86-551-569096356909645167Computer Knowledge and Technology电脑知识与技术第5卷第19期(2009年7月)3）形式化与可视化语言结合的软件体系结构建模方法形式化z方法能产生精确、无二义性的形式规约，为软件开发提供了严格的数学基础，但不够直观。
UML是一种可视化的图形建模语言，采用直观的图形表示法为系统进行建模，但缺乏精确的语义。
形式化Z方法和UML存在很大的互补性，二者的结合研究对提高软件的可靠性有着非常重要的意义[2]。
本文在最后部分将用一个实例演示UML和Z方法结合的应用。
2基于UML和Z的软件体系结构建模过程由于形式化方法的加入，UML和Z结合的建模的目标与开发模式与传统的建模过程有着明显的不同，主要体现在UML和Z结合建模的需求分析和设计阶段，需要投入比传统开发模式大得多的工作量，UML和Z结合的建模方法既保证了软件体系结构设计的一致性和可靠性，也使得后期的编码和测试工作相对简单。
图1为UML与形式化模型检测相结合的软件体系结构建模过程[3]。
3应用实例下面将采用笔者主持开发的××省电力公司人力资源系统(EHR)作为实例来介绍UML和Z结合的软件体系结构开发过程，这个过程中所使用的工具见图2。
3.1系统需求××省电力公司人力资源系统（EHR）是集人才招聘、合同管理、工资社保管理、人事变动、档案管理等功能为一体的人事系统。
该系统主要用于人事部对人才的管理和财务部对员工工资发放的管理。
具体需求如下：1）员工通过登陆系统进行注册，人事部管理人员通过系统来审核员工的注册信息，这样就建立了企业与员工之间的合同关系；2）人事部管理人员根据员工的日常工作表现、职称、工种及学历等情况提出员工的基本工资、奖金、职位升迁、人事调动等方案，方案由公司领导确认后执行。
3）财务部根据公司确定的工资、奖金方案，对员工工资进行管理，包括员工薪金的升降、员工账户的修改、员工账户的删除、生成财务各类报表、提出薪金改革方案等。
3.2UML用例图和类图根据系统功能说明可知，本系统的角色主要有：员工、财务部、人事部、公司领导；主要的业务有：人事管理、财务管理等。
图3和4分别为此人力资源系统的Use Case图和类图。
3.3形式化说明、验证Use Case模式中的类、关系、函数都可以通过Z语言进行形式化的描述，如：利用Z语言，可以将Use Case形式化为如图5所示格式：图5基于Z的Use Case图的形式化其中Declarations是角色、Use Case和系统的说明，Predicates部分用于表示角色和Use Case之间的关系，也就是说用来表示某个角色与Use Case之间有关系，即使用了Use Case的功能[4]。
根据以上对形式化方法的说明，下面我们将给出本人力资源系统的部分求精过程：//每个员工（Worker）都有自己的ID和个人信息，ID和个人信息之间是一个全双射关系；员工之间的ID不能重复；员工的ID和登录密码之间也不能相同并且密码必须小于8个字节。
图1UML与Z相结合的软件体系结构建模过程图2系统开发工具图3人力资源系统的Use Case图5168本栏目责任编辑：谢媛媛软件设计开发软件设计开发本栏目责任编辑：谢媛媛Computer Knowledge and Technology 电脑知识与技术第5卷第19期(2009年7月)（上接第5158页）2)组件模型建立编辑default.vm 主界面页面放到Layout 模块中，而default.vm 主要又由defaultTop.vm 、menu.vm 、defaultBottom.vm 三个页面组成，放到模块Navigation 中。
负责物料数据视图展示的displayItem.vm 文件放到Screen 模块中。
所有业务逻辑都在\tdk\webapps\ims\WEB-INF\classes\org\mycompany\ims\modules 类文件中处理，负责处理物料添加、修改、删除操作的类文件ItemSQLclass 放到Action 模块中，而负责读取物料记录的类文件displayItem.class 放到Screen 模块中。
3)组件的协同用户登录后先进入default.vm ，发出请求进入物料管理页面displayItem.vm,其调用displayItem.class 类负责与数据层Torque 中的物料数据对象打交道，从数据库中读取出所有的物料数据记录。
用户请求添加新物料信息，调用addItem.vm 页面，在添加提交后返回到displayItem.vm ，但在返回之前定义了Action 事件,则调用ItemSQL.class 插入新记录后再执行displayItem.class ，把新的数据返回到dis -playItem.vm 视图文件。