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

计算机科学 ›› 2013, Vol. 40 ›› Issue (5): 177-183.

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

郭艳燕,刘惊雷

烟台大学计算机学院烟台264005;烟台大学计算机学院烟台264005

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家自然科学基金(61170224),山东省自然科学基金(ZR2011FL018),山东高等学校科研计划项目(J10LG27)资助

Formalization for Model Element of UML Statechart in RSL

GUO Yan-yan and LIU Jing-lei

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

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

关键词: 统一建模语言(UML),状态机,形式化方法,有穷自动机,RAISE规约语言(RSL)

Abstract: UML statechart plays an important role in describing the dynamic behavior of system and model as an important part of UML dynamic description mechanism．Existing dynamic semantics of UML are lack of accurate formal description．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 formalized 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．

Key words: Unified modeling language(UML),Statechart,Formal method,Finite automata,RAISE specification language(RSL)

郭艳燕,刘惊雷. UML状态机模型元素的RSL形式化定义[J]. 计算机科学, 2013, 40(5): 177-183. https://doi.org/

GUO Yan-yan and LIU Jing-lei. Formalization for Model Element of UML Statechart in RSL[J]. Computer Science, 2013, 40(5): 177-183. https://doi.org/

参考文献

[1] OMG.UML2.0 Infrastructure Specification．http://www.omg.org/cgi-bin/doc?formal/2005-07-05.pdf,2005
[2] OMG.Object Constraint Language．Version 2.3.1．http://www.omg.org/cgi-bin/doc?formal/2009-02-02.pdf,2009
[3] 蒋慧,林东,谢希仁.UML状态机的形式语义[J].软件学报,2002,3(12):2244-2250
[4] Egyed A．Automatically Detecting and Tracking Inconsistencies in Software Design Models[J]．IEEE Transactions on Software Engineering,2011,37(2):188-204
[5] Bjorner D.软件工程卷1:抽象与建模[M]．刘伯超,向剑文,译．北京:清华大学出版社,2010:18-21
[6] Woodcock J．Formal Methods:Practice and Experience[J]．ACM Computing Surveys,2009,1(4):19:1-19:36
[7] 郭峰,姚淑珍.基于Petri网的UML状态图的形式化模型[J]．北京航空航天大学学报,2007,3(2):248-252
[8] 董威,王戟,齐志昌．UML Statecharts的模型检验方法[J].软件学报,2003,4(4):750-756
[9] 朱雪阳,唐稚松.Statecharts 的组合语义与求精[J].软件学报,2006,7(4):670-681
[10] Jin Yan,Esser R．A method for describing the syntax and semantics of UML statecharts[J]．Software System Model,2004,3(2):150-163
[11] 单黎君,朱鸿．UML的形式化描述语义[J]．计算机工程与科学,2010,32(3):96-103
[12] 郭亮,缪淮扣,王皙,等.UML模型到FSM模型的转换[J].计算机科学,2009,6(7):113-116
[13] Sun Meng,Zhang Nai-xiao．The Formalization for UML statechart Diagrams[J]．Acta Scientiarum Naturalium Universitatis Pekinensis,2005,1(3): 344-356
[14] 李明,杨海波,张其文,等．基于时序描述逻辑的UML状态图语义[J]．计算机工程,2010,36(23):76-78
[15] 李留英,王戟,齐治昌.UML Statechart图的操作语义[J].软件学报,2001,2(12):1865-1868
[16] 曾一．基于形式化规格说明的UML状态图提取[J]．计算机应用研究,2011,8(5):1767-1769
[17] Bendraou R．A Comparison of Six UML-Based Language forSoftware Process Modeling[J].IEEE Transactions on Software Engineering,2010,6(5):662-675
[18] Whittle J．Synthesizing Hierarchical State Machines from Ex-pressive Scenario Descriptions[J]．ACM Transactions on Software Engineering,2010,9(3):8:1-8:40
[19] Bjorner D．软件工程卷2:系统与语言规约[M]．刘伯超,向剑文,译.北京:清华大学出版社,2010:406-413
[20] Ershov A P,Itkin V E．Correctness of mixed computation in Algol-like programs[J]．Mathematical Foundations of Computer Science,1977,53:59-77

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed