Language and Tool Support for Class and State Machine Refinement in UML-B
Language and Tool Support for Class and State Machine Refinement in UML-B
复制标题
UML-B 中类和状态机细化的语言和工具支持
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
C. Snook
中科院分区：
文献类型：
--
作者：
M. Said;M. Butler;C. Snook
UML-B 是Event-B 的“类UML”图形前端，为面向对象的建模概念提供支持。特别是，UML-B 支持类图和状态机，以及普通 Event-B 中未明确支持的概念。在Event-B中，细化用于关联不同抽象级别的系统模型。相同的抽象细化概念也可以应用在 UML-B 中。本文介绍了细化类和细化状态机的概念，以实现 UML-B 中类和状态机的细化。与这些概念一起，还介绍了一种在类之间移动事件以促进抽象的技术。我们的工作明确了 UML-B 中的类结构和状态机细化。 UML-B 绘图工具和 Event-B 转换器经过扩展以支持新的细化概念。通过自动柜员机 (ATM) 的案例研究来演示细化类和细化状态机的应用和有效性。
UML-B is a `UML-like' graphical front end for Event-B that provides support for object-oriented modelling concepts. In particular, UML-B supports class diagrams and state machines, concepts that are not explicitly supported in plain Event-B. In Event-B, refinement is used to relate system models at different abstraction levels. The same abstraction-refinement concepts can also be applied in UML-B. This paper introduces the notions of refined classes and refined state machines to enable refinement of classes and state machines in UML-B. Together with these notions, a technique for moving an event between classes to facilitate abstraction is also introduced. Our work makes explicit the structures of class and state machine refinement in UML-B. The UML-B drawing tool and Event-B translator are extended to support the new refinement concepts. A case study of an auto teller machine (ATM) is presented to demonstrate application and effectiveness of refined classes and refined state machines.