计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2011年
35期
77-80,142
,共5页
曾一%孙政%周吉%胡小威
曾一%孫政%週吉%鬍小威
증일%손정%주길%호소위
形式化方法%元模型%UML状态图%B方法%模型转换
形式化方法%元模型%UML狀態圖%B方法%模型轉換
형식화방법%원모형%UML상태도%B방법%모형전환
状态图是UML动态视图之一,主要描述对象的动态行为,但缺乏形式化的动态语义,不利于软件从需求到代码的自动化转换.B语言支持形式化规格说明,在MDA转换过程中,把UML状态图转换为B规格说明,可以使MDA中的需求表达得更为精确.基于此,提出了一种基于EMF的状态图到B规格说明的转换方法,设计了状态图和B抽象机的元模型,定义了元模型之间的转换规则,给出了该规则的ATL描述,最后在Eclipse平台实现了状态图到B规格说明的自动转化.该方法为MDA过程中获取形式化需求提供了一种新的途径.
狀態圖是UML動態視圖之一,主要描述對象的動態行為,但缺乏形式化的動態語義,不利于軟件從需求到代碼的自動化轉換.B語言支持形式化規格說明,在MDA轉換過程中,把UML狀態圖轉換為B規格說明,可以使MDA中的需求錶達得更為精確.基于此,提齣瞭一種基于EMF的狀態圖到B規格說明的轉換方法,設計瞭狀態圖和B抽象機的元模型,定義瞭元模型之間的轉換規則,給齣瞭該規則的ATL描述,最後在Eclipse平檯實現瞭狀態圖到B規格說明的自動轉化.該方法為MDA過程中穫取形式化需求提供瞭一種新的途徑.
상태도시UML동태시도지일,주요묘술대상적동태행위,단결핍형식화적동태어의,불리우연건종수구도대마적자동화전환.B어언지지형식화규격설명,재MDA전환과정중,파UML상태도전환위B규격설명,가이사MDA중적수구표체득경위정학.기우차,제출료일충기우EMF적상태도도B규격설명적전환방법,설계료상태도화B추상궤적원모형,정의료원모형지간적전환규칙,급출료해규칙적ATL묘술,최후재Eclipse평태실현료상태도도B규격설명적자동전화.해방법위MDA과정중획취형식화수구제공료일충신적도경.
