UML模型形式化B方法转换的实现

摘要

UML是软件开发的标准语言,已经广泛运用于各种领域的软件设计建模之中.但是UML的半形式化表达方式缺乏准确的语义,使其无法在软件设计过程中针对需求的一致性进行分析,因此需要使用一种形式化方法对UML模型进行描述.以高速列车控制系统为例,基于B方法对用例图模型与顺序图模型进行形式化转换,对两种模型中各组成部分从语义角度分别进行了描述,从而完整地刻画了UML模型所描述的系统需求.%As a standard language for software development, UML is widely used in designing and modelling software in various fields. However, UML is a semi-formal language lack of accurate semantics, which makes it impossible to analyse the consistency of the requirements in the software design process. Therefore, it is necessary to use a formal method to describe UML models. This paper takes High Speed Train Control System as an example and carries out a formalisation conversion of use case diagram models and sequence diagram models by B method. This formalisation conversion method will describe each component of the two kinds of models from the point of view of semantic and depict the requirements described by UML models completely.