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

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

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