基于Event-B形式化分析UML模型一致性

Formally analyzing the inconsistency of UML models with Event-B

软件工程实践中广泛采用UML作为建模语言,UML模型在演进过程中会引入UML模型一致性问题.采用Event-B形式化技术可以协助分析UML模型的一致性,提出UML模型向Event-B模型转换的方法和规范性要求,设计具体的转换算法,证明这些算法的规范性以及采用这些算法转换得到的Event-B模型和原UML模型的等价性.文中提出了基于EventB形式化分析UML模型一致性的方法,并通过具体的案例说明了方法的具体执行过程.结果证明:基于Event-B形式化分析UML模型一致性的方法是有效的,可帮助改进UML模型质量.

Unified modeling language （UML） pervades the practices of software engineering. The evolution of UML models would introduce the inconsistency problems. Exploiting formal methods is a way to analyze the in-consistency problems of UML models. This paper provides a process to define the rules for transforming a UML model to an Event-B model and the transforming algorithms, and defines a conformance standard to be followed by this transforming. A set of concrete transforming algorithms are provided in this paper, whose conformance to that conformance standard is proved as well. The equivalence of a UML model and an Event-B model, which is generated by those transforming algorithms from the prior UML model, is proved on the consistency of semantics of two models. Upon these preparations, a method of formally analyzing the inconsistency of UML models is pres-ented. Then, an example shows the details of the process of formally analyzing the inconsistency of UML models, whose outcomes specify the effectiveness of thisprocess. This formal analysis process is valid and effective for im-proving the quality of models in software engineering.