摘要： 研究了UML 模型到B 形式化规约的转换。提出了一套从OCL 数据类型及定义在这些数据类型上的操作到B AMN 的转换规则。OCL 的Boolean 类型和Integer 类型分别对应于B 中的BOOL 类型和Z 类型；OCL 中的String 类型需用B 抽象机器重新定义新的数据类型Char_TYPE 和String_TYPE 来进行规约；OCL 中的REAL 类型采用B 中的记录表达式进行近似模拟；OCL 中的Collection 类型(包括Set，Orderedset，Bag，Sequence)用B 语言中的set，sequence，tree 等进行近似模拟。

关键词: 统一建模语言；对象约束语言；形式化方法；B 方法

Abstract: Transformation from UML model to B method’s specification is studied. A suit of rules of transformation from OCL data types to B abstract machine notations is proposed. The Boolean type and Integer type of OCL are separately translated to B’s BOOL and Z type; OCL String type is specified by new defined Char_TYPE and String_TYPE; OCL real type is simulated by B’s record expression; OCL collection type which includes Set, Orderedset, Bag and Sequence is simulated by B’s set, sequence and tree types

Key words: Unified modeling language(UML); Object constraint language(OCL); Formal method; B-method