UML状态机视图的RSL形式描述

北京大学学报（自然科学版）

UML状态机视图的RSL形式描述

孙猛¹,张乃孝¹,Bernhard K Aichernig²

收稿日期:2004-03-04 出版日期:2005-05-20 发布日期:2005-05-20

The Formalization for UML Statechart Diagrams

SUN Meng¹, ZHANG Naixiao¹, Bernhard K Aichernig²

Received:2004-03-04 Online:2005-05-20 Published:2005-05-20

摘要/Abstract

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

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

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

中图分类号:

TP311.5

孙猛,张乃孝,Bernhard K Aichernig. UML状态机视图的RSL形式描述[J]. 北京大学学报（自然科学版）.

SUN Meng,ZHANG Naixiao,Bernhard K Aichernig. The Formalization for UML Statechart Diagrams[J]. Acta Scientiarum Naturalium Universitatis Pekinensis.

导出引用管理器 EndNote|Ris|BibTeX

链接本文: https://xbna.pku.edu.cn/CN/

https://xbna.pku.edu.cn/CN/Y2005/V41/I3/344

[1]	单锦辉, 张路, 王金波, 张涛. 实时嵌入式软件时间抽象状态机的扩展[J]. 北京大学学报自然科学版, 2019, 55(2): 197-208.
[2]	陈钢, 于林宇, 裘宗燕, 王颖. 基于逻辑的形式化验证方法: 进展及应用[J]. 北京大学学报（自然科学版）, 2016, 52(2): 363-373.
[3]	饶俊峰, 张显峰, 潘一凡. 气溶胶光学厚度及Ångström指数遥感反演的不确定性对紫外线指数计算的影响[J]. 北京大学学报（自然科学版）, 2016, 52(2): 210-218.
[4]	孙钊,王勇. 芯片功能验证流的高效生成方法[J]. 北京大学学报（自然科学版）, 2007, 43(1): 92-95.
[5]	孙猛, 杨红丽, 张乃孝, 裘宗燕. 基于UML的软件结构规范与精化[J]. 北京大学学报（自然科学版）, 2007, 43(1): 1-10.
[6]	刘瑜, 林报嘉, 唐大仕. UML-G: 针对地理信息应用的面向对象建模语言[J]. 北京大学学报（自然科学版）, 2004, 40(2): 271-278.
[7]	孙踊, 杨宏戟. 基于通信顺序进程的计算机网络通信协议形式化描述[J]. 北京大学学报（自然科学版）, 1997, 33(1): 110-122.
[8]	莫小欢. CPⁿ中具有特殊常Kähler角的调和曲面之特性[J]. 北京大学学报（自然科学版）, 1995, 31(3): 277-281.