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

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