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

Research and implementation on state chart transformation in B

作　　者：曾一[1] 孙政[1] 周吉[1] 胡小威[1] 

机构地区：[1]重庆大学计算机学院,重庆400030

出　　处：《计算机工程与应用》2011年第35期77-80,142,共5页Computer Engineering and Applications

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]