UML状态机模型元素的RSL形式化定义

Formalization for Model Element of UML Statechart in RSL

UML状态机作为UML动态描述机制的重要组成部分,在描述系统及模型的动态行为时扮演着重要的角色,但已有的UML动态语义缺乏准确的形式化描述。首先将UML状态机抽象成图;再将图通过传统的有穷自动机进行语义扩展,同时增加状态分层,形成一个基于UML状态机的有穷自动机;然后用RAISE规约语言RSL对扩展后的自动机进行形式化定义,使UML状态机中的模型元素的语义更加清晰、精确,为后期的UML状态机的操作语义形式化研究打下基础。

UML statechart plays an important role in describing the dynamic behavior of system and model as an impor- tant part of UML dynamic description mechanism. Existing dynamic semantics of UML are lack of accurate formal de- scription. UML Statechart was defined as the abstract syntax graphs, which were expanded into a new finite automaton based on UML statechart through the traditional finite automaton and increased state hierarchy. Then, this paper for- realized the model elements of UML statechart through RAISE specification language（RSL）. The formal semantic of the model elements of UML statechart is more clear and accurate, which is the base of the later operation semantic study of UML statechart.