一种状态图到B规格说明的自动转换方法研究实现

计算机工程与应用 ›› 2011, Vol. 47 ›› Issue (35): 77-80.

一种状态图到B规格说明的自动转换方法研究实现

曾一，孙政，周吉，胡小威

重庆大学计算机学院，重庆 400030

收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2011-12-11 发布日期:2011-12-11

Research and implementation on state chart transformation in B

ZENG Yi，SUN Zheng，ZHOU Ji，HU Xiaowei

College of Computer Science，Chongqing University，Chongqing 400030，China

Received:1900-01-01 Revised:1900-01-01 Online:2011-12-11 Published:2011-12-11

摘要/Abstract

摘要： 状态图是UML动态视图之一，主要描述对象的动态行为，但缺乏形式化的动态语义，不利于软件从需求到代码的自动化转换。B语言支持形式化规格说明，在MDA转换过程中，把UML状态图转换为B规格说明，可以使MDA中的需求表达得更为精确。基于此，提出了一种基于EMF的状态图到B规格说明的转换方法，设计了状态图和B抽象机的元模型，定义了元模型之间的转换规则，给出了该规则的ATL描述，最后在Eclipse平台实现了状态图到B规格说明的自动转化。该方法为MDA过程中获取形式化需求提供了一种新的途径。

关键词: 形式化方法, 元模型, UML状态图, B方法, 模型转换

Abstract: State chart，one of the UML dynamic views，mainly describes the dynamic behavior of the objects while the lackage of the formalized dynamic semantics go against the automational conversion of the software from the demand to the code.B language supports formal specifications，in the MDA conversion process，transforming UML state chart into B specification makes the expression of the requirement of MDA in a more accurate way.Based on this，this paper puts forward a conversion approach based on EMF state chart to B specification，designs the metamodel of state chart and B abstract machine，then provides the definition of the conversion rule among metamodels and the ATL description of it as well，at last achieves the automational conversion from state chart to B specification on the Eclipse platform.This method provides a novel way to obtain formal demand in the process of MDA.

Key words: formal method, metamodel, UML state chart, B-method, model transformation

曾一，孙政，周吉，胡小威. 一种状态图到B规格说明的自动转换方法研究实现[J]. 计算机工程与应用, 2011, 47(35): 77-80.

ZENG Yi，SUN Zheng，ZHOU Ji，HU Xiaowei. Research and implementation on state chart transformation in B[J]. Computer Engineering and Applications, 2011, 47(35): 77-80.

[1]	张俊，廖雪花，余旭玲，雷蒙. 关系型数据库内存化存储模型研究[J]. 计算机工程与应用, 2021, 57(19): 123-128.
[2]	刘友林，郑巍，谭莉娟，樊鑫，杨丰玉. 面向适航标准的机载软件测试验证工具综述[J]. 计算机工程与应用, 2021, 57(11): 1-10.
[3]	王诗宇，刘洪星，范家佳. 移动用户界面概念模型到代码的转换方法研究[J]. 计算机工程与应用, 2020, 56(10): 240-245.
[4]	祝义1，2，黄志球1，周航1，刘林源1，3. 函数式程序模板元编程的元建模实现方法[J]. 计算机工程与应用, 2018, 54(7): 1-10.
[5]	李云祥，宋元斌，范晨昊. 复杂项目调度中的逻辑关系表述及模型转换[J]. 计算机工程与应用, 2018, 54(13): 216-223.
[6]	陈博文，蒋磊，刘潇文，张群. 基于混沌量子粒子群的FHN神经元UWB信号检测[J]. 计算机工程与应用, 2017, 53(6): 135-140.
[7]	郑继明1，2，崔玉岩1，耿金玲2，陈龙1. 运用DWT和ORB的图像篡改检测方法[J]. 计算机工程与应用, 2017, 53(11): 187-191.
[8]	胡晓辉1，韩佳芮2. 车站联锁进路控制逻辑的形式化方法[J]. 计算机工程与应用, 2016, 52(17): 229-234.
[9]	唐伟. 一种有效的模糊关联规则挖掘的形式化方法[J]. 计算机工程与应用, 2015, 51(18): 114-119.
[10]	曹真，曹旻. 面向测试的构件系统模型及测试用例生成方法[J]. 计算机工程与应用, 2014, 50(22): 59-64.
[11]	王广彦. 元模型输入参数筛选方法研究[J]. 计算机工程与应用, 2013, 49(8): 51-57.
[12]	李鸿1，2，马小平1. 粒计算的四元模型研究[J]. 计算机工程与应用, 2013, 49(4): 9-13.
[13]	游伟，雷定猷. 铁路超限超重货物装载加固可拓实例推理方法[J]. 计算机工程与应用, 2013, 49(18): 24-28.
[14]	刘松. 事件和参数双因素驱动的智能模型集成机制[J]. 计算机工程与应用, 2012, 48(8): 28-31.
[15]	尼加提·纳吉米1，2，买合木提·买买提3，吐尔根·依布拉音4. 基于N元模型的维吾尔语词性标注实验研究[J]. 计算机工程与应用, 2012, 48(25): 137-140.