UML状态机视图的RSL形式描述(英文)  

The Formalization for UML Statechart Diagrams 1)

作　　者：孙猛[1] 张乃孝[1] Bernhard K Aichernig 

机构地区：[1]北京大学数学科学学院,北京100871 [2]澳门联合国大学国际软件技术研究所

出　　处：《北京大学学报（自然科学版）》2005年第3期344-357,共14页Acta Scientiarum Naturalium Universitatis Pekinensis

基　　金：国家自然科学基金资助项目 (6 0 2 730 0 1和 6 0 4 730 5 6 )

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

关 键 词：UML 状态机 RAISE 形式化 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]