网站首页  词典首页

请输入您要查询的论文：

　

标题 UML状态图到B形式化规范的转换实现
范文 滕飞+杨静



摘要摘要：统一建模语言UML在面向对象的建模技术中得到了广泛应用。但是UML模型缺乏形式化语义，难以使用数学方式对模型进行分析和验证。B方法作为一种建立在严格数学机理上的形式化方法，将可视化UML模型转换为B形式化规范，可以对模型进行形式化描述和分析，确保模型的可靠性。通过研究从UML状态图到B形式规范的转换规则，提出了一种基于XMI的状态图到B形式化规范的自动转换方法，并使用Java语言实现了自动转换工具UML2B。
关键词关键词：UML状态图；B方法；转换工具；UML2B
DOIDOI：10.11907/rjdk.162480
中图分类号：TP301文献标识码：A文章编号文章编号：16727800（2017）001000605
0引言
需求分析是软件定义时期的最后一个阶段，工作是深入描述软件功能和性能，确定软件设计的限制和软件同其它系统元素的接口细节[1]。统一建模语言（UML）是软件分析、设计与可视化建模的工业标准[2]，使用面向对象的概念进行建模，在软件开发中得到了广泛应用。UML状态图用来描述系统的动态行为，它是基于对象特征相对传统状态机的变体，主要用于捕捉来自外界对象或环境的服务请求的某对象内部行为的动态特征[3]。UML用自然语言描述的语义不够精确，没有提供一种对UML模型进行推理的合理机制，无法对模型的一致性、完整性、正确性进行形式化的分析和验证，因此有必要对UML模型进行形式化描述。B方法产生于20世纪80年代早期，由法国计算机科学家J-R Abrial在Z 语言的基础上提出，是更加面向软件开发过程的形式化方法。B方法作为一种形式化方法，可以对软件系统提供无二义的、更精确的描述，使系统具有较高的可信度和正确性。在B方法的应用和研究中，文献[4]提出了一套从UML状态机到B形式化规约的转换规则。文献[5]通过B方法和UML在问题对象域层次上的结合，给出了在软件设计中提高软件质量的方法。文献[6]做了UML状态图到形式化B语言转换的实例研究。目前的研究主要以提出UML模型到B方法的转换规则，并在案例中应用转换规则，验证转换规则的正确性，但没有实现转换工具。直接根据UML状态图和B方法的语法规则实现转换，过程较繁琐，需要人工干预，难以用程序实现自动转换。本文通过研究从UML状态图到B方法的转换规则，提出了一种基于XMI的自动转换方法，并在此基础上使用Java语言实现了模型转换的原型工具UML2B。
1UML与B方法
1.1UML简介
统一建模语言UML（Unified Modeling Language）是一种由OMG（Object Management Group）提出的标准对象建模语言，作为支持模型化和软件系统开发的图形化语言，可以使用面向对象概念进行建模。UML作为一种面向对象的标准建模语言，在信息管理系统建模领域得到了广泛应用[7]。通过相关的UML建模软件，建立系统模型，可以以一种可视化的方式向开发人员和客户呈现系统设计模型。
1.2形式化B方法简介
B方法是一种“面向模型”的数学方法，也称B语言。利用B方法建立的模型可以使用数学方式进行分析，从而避免需求设计中的不一致、不完整。该方法使用AMN（Abstract Machine Notation ）作为软件开发过程中的规约、设计及实现语言，使程序和程序规约说明处于一个统一的数学框架之下[8]。B抽象机中主要包括变量、不变式、操作，可以从静态行为和动态行为两个方面描述系统。使用B方法创建的形式化模型可以使用现有B方法支持工具，如B-Tookit、Pro B、Atelier-B等进行分析，以提高模型的可靠性。
2模型转换方法
2.1自动转换框架
本文提出的自动转换框架如图1所示。
自动转换过程包括4个步骤：①使用UML建模软件（如：StartUml、Rational Rose）设计UML状态图，并通过建模软件自带的插件生成对应的XMI文档，命名为UMLStart.xml，将其作为自动转换的输入端；②设计Java类，从UMLStart.xml中提取的信息保存到对应的Java类实例化对象中；③根据UML状态图和B抽象机之间的映射关系，编写UML状态图到B抽象机的转换規则，并使用Java语言实现转换程序；④读取保存在Java数据结构中的信息，按照转换规则生成对应的B形式化规范，转换结果可以在屏幕中显示。
2.2转换规则
UML模型与B形式化方法在语义和结构上存在对应关系，可以将UML状态图转换为B方法中的抽象机。下面给出从状态图到B形式化规范的转换规则。
规则一：状态转换，如表1和表2所示。状态表示对象在生命周期的某个条件或者状况，对象需要执行某些活动、满足某些条件等，当对象执行了一系列活动，或当某个事件发生后，对象的状态发生了变化。基本状态指不含子状态的状态，只有若干个转移和可能的入口、出口动作。组合状态指包含了若干个子状态的状态，嵌套于组合状态中的状态成为子状态[9]。本文使用抽象机中的SETS子句描述状态图中的状态，用一个枚举集合STATE代表基本状态，枚举集合SUBSTATE代表子状态。
END；表9UML状态图与XMI元素映射UML状态图XMI元素基本状态SimpleState组合状态CompositeState转移Transition监护条件Guard动作 EffectXMI文档通过元素的属性或其子元素描述UML模型。每个模型元素都有工具给了它一个唯一的标识号，表示在该元素的“xmi.id” 属性中。模型元素的命名表示在该元素的“name”属性中[12]。通过研究，可以使用元素标签名称对XMI文档进行检索，按照转换规则从被检索的标签中的属性，或其子元素中提取转换信息。在提取信息过程中，可以利用“xmi.id” 属性值在XMI文档中查找对应元素。
3UML2B原型工具实现
本文采用Java语言在MyEclise平台上实现转换工具，主要技术包括解析XML、J2SE、MVC架构。解析XML文件方面，有SAX、DOM等技术。SAX的全称是Simple APIs for XML，也即XML简单应用程序接口[13]。SAX接口的基本原理是由接口的使用者提供符合定义的处理器。XML分析时遇到特定的事件，就去调用处理器中特定事件的处理函数[14]。DOM是应用程序访问XML文档的编程API，该API包含了用于XML文档节点信息，修改文档数据信息和动态存取XML等一系列方法[15]。本文通过对比SAX和DOM的技术特点，采用DOM技术实现工具相关功能。DOM模式解析XML文件，可以将其整体读入内存，并转化为一个树型文档，从而可以多次遍历这颗树并获取节点信息。根据工具的业务特点，采用Java提供的XML解析器DOM API for Java处理XML文档。工具包图如图2所示。
工具分为6个包，分别是Intput、View、UMLToJava、UMLToB、Dom、XMLParse包。Intput包用于读取操作者输入的UML模型。View是UML2B工具的视图部分，包括StartPanel、ContextPanel、ValuePanel 3个类，StartPanel类显示起始界面，操作者可以输入所要转换的UML模型地址。ContextPanel类用于显示转换中提取的UML模型信息。ValuePanel类用于显示最后的转换结果。UMLToJava包通过相应的转换规则和算法，从状态图对应的XMI文档中提取信息，并保存到相应的Java对象中。Dom包中包括转换信息的Java实现类，如表10所示。从UML模型对应的XMI文档中提取信息保存到对应类的实例化对象中。
UMLToB包通过操作，保存转换信息的Java数据结构，按照转换规则生成对应的B形式化规范，完成状态图到B形式化规范的转换。UML2B工具的类图如图3所示。
4案例应用
下面使用UML2B工具对实例进行转换。这个实例是一个洗衣机的状态图。洗衣机的初始状态是停止状态（Stop），当用户在有电的情况下按下开关，洗衣机进入运行状态（Running），首先进入称重状态（Weigh），当重量小于等于7KG时，洗衣机开始正常工作，依次进入清洗状态（Washing）、漂洗状态（Rinseing）、甩干状态（Dry），洗涤过程结束进入等待用户操作状态（Waiting）。当重量大于7KG时，超过了洗衣机的运行负荷，进入警报状态（Reporting），警报结束后进入等待用户操作状态（Waiting）。当洗衣机在运行状态时，用户发出close操作，洗衣机进入停止状态。洗衣机状态如图4所示。
按照前述的转换框架，使用StarUML建模软件创建状态图模型并导出对应的XMI文档，命名为UMLStart.xml，作为UML2B工具的输入端。UMLStart.xml可以在工具界面中显示，如图5所示。
UML2B工具通过程序从UMLStart.xml文件提取转换信息，保存到Java数据结构中。根据转换规则，Stop是一个基本状态，Running是一个组合状态，按照规则一转换为抽象中对应的集合。Start是一个结束于组合状态边缘的转移，按照规则三转换为抽象机中对应的操作。close是一个开始于组合状态边缘的转移，按照规则四转换为抽象机中对应的操作。weighing是一个复合转移，按照规则七转换为抽象机中对应的操作。Rinse、spin、stopWash、stopReport是组合状态中子状态间的转移，按照规则六转换为抽象机中对应的操作。转换结果在屏幕中显示，如图6所示。
实验通过一个案例，使用UML2B工具实现了从UML状态图到B形式化规范的转换。实验结果验证了本文提出的转换方法可行，在此方法上开发的UML2B工具可以实现自动转换功能。转换后得到的B形式化模型可以使用现有的B方法工具进行分析。
5结语
本文研究了从UML状态图到B方法的转换规则，在此基础上，提出了一种自动转换方法。着重介绍了从UML状态图到B形式化规范的转换规则，以及转换工具的主要设计思路，使用Java语言实现了模型转换的原型工具UML2B。通过案例应用表明本文提出的转换方法可行，在此基础上实现的原型工具UML2B可以实现转换功能。
参考文献参考文献：
[1]塔维娜，何积丰.基于形式化方法的需求分析[J].计算机工程，2003，29（18）：107108.
[2]许卓明，顾华建，倪玉燕，等.UML类图向OWL本体转换工具的设计与与实现[J].河海大学学报，2007，（35）4：477482.
[3]姚淑珍，金茂忠.UML状态图的形式化建模及其分析[J].北京航空航天大学学报，2007，（33）4：472476.
[4]肖健宇，张德云，董皓，等.UML状态机到B形式化规约转换[J].微电子学与计算机，2005，22（8）：8084.
[5]何飞，谷建华.B方法和UML在软件设计中的结合应用[J].计算机工程与科学，2007，（29）1：134136.
[6]皱盛荣，孟静，阳雪平，等.UML状态图到形式化B语言转换的实例研究[J].科学技术与工程，2007，（7）24：63346338.
[7]方红萍，陈和平.信息系统UML建模研究[J].计算机工程与设计，2006，（27）19：36133615.
[8]胡启敏，薛锦云.形式化方法Designware、B的比较[J].计算机工程与应用，2007，43（31）：9699.
[9]吴帅.UML模型图到B方法形式规约转换研究与应用[D].南昌：江西师范大学，2007.
[10]TIMOTHY J GROSE，GARY C DONEY，STEPHEN A BRODSKY.精通XMI——使用XMI、XML和UML进行Java编程[M].徐强，金艳红，译.北京：电子工业出版社，2004.
[11]熊永刚，唐慧佳.基于XMI的UML模型到XML文檔转换实现[J].计算机应用与软件，2010，27（4）：6870.
[12]黎闯.UML交互图到Contract规格说明的转换及其程序实现[D].广州：暨南大学，2005.
[13]赵俊岚.XML编程中的DOM与SAX技术[J].计算机工程，2004（30）24：7072.
[14]张迪，朱敏，张凌立.基于SAX的XML解析与应用[J].计算机与数字工程，2008（36）7：103106.
[15]李发应.基于DOM与SAX的数据存取技术研究与实现[J].信息技术，2009（2）：5154.
责任编辑（责任编辑：杜能钢）
随便看

　

科学优质学术资源、百科知识分享平台，免费提供知识科普、生活经验分享、中外学术论文、各类范文、学术文献、教学资料、学术期刊、会议、报纸、杂志、工具书等各类资源检索、在线阅读和软件app下载服务。

　

Copyright © 2004-2023 puapp.net All Rights Reserved
更新时间：2024/12/23 6:05:44