基于形式化规格说明的UML状态图提取

为了辅助软件开发者理解形式化规格说明，提出一种从B方法规格说明中提取UML状态图的方法。通过分析状态信息在规格说明中的表现形式，定义一系列精确的简单状态、状态迁移、复合迁移、分层状态和状态图通信等提取规则。借助状态变量表和状态迁移表，最终实现状态元素和状态关系的提取，并以此构造完整的UML状态图。实验结果验证了方法的正确性及有效性。

UML state-chart extraction based on formal specification

To assist software developers understand formal specification, this paper proposed a method of UML state-chart extraction based on B method specifications. By analyzing the representation of state information in specifications, a serious of extraction rules were defined, including simple state, state transition, compound transition, hierarchical state, state-chart communication and so on. With the help of state variable table and state transition table, state elements and state relations were extracted. Complete UML state-chart was built. The correctness and effectiveness of this method was proved by an experiment.