Abstract: It is presented that a formalization for UML statechart diagrams in the RAISE specification language RSL. By such a formalization, a general framework is proposed for integration of graphical UML statechart diagrams and formal RSL specifications, which forms the continuation of the previous work on formalization of UML class diagrams in RSL. This allows the definition of UML semantic interpretations that are precise and unambiguous, and also enhancing the readability, conciseness and abstraction of the resulting RSL specification. A case study illustrates how the framework can be used to create formal specification for UML models and analyze the properties of the models.

Key words: UML, statechart, RAISE, formalization

摘要： 使用RAISE规范语言RSL给出了UML状态机视图的形式描述。通过这一形式化提出了一种对图形化的UML状态机视图模型的形式化和RSL规范进行集成的框架，这一工作是对UML类图在RSL中形式化的继续，使得人们可以对UML的非形式化模型给出一种精确、无二义性的语义解释，同时也提高了RSL规范的抽象层次，增强了其可读性、简明性。最后通过一个应用实例，说明这一框架如何用于从UML模型创建对应的形式化规范，并对模型的性质进行了分析。

关键词: UML, 状态机, RAISE, 形式化