UML实时活动图的形式化分析  

Formal Analysis on UML Real-Time Activity Diagram

作　　者：崔萌[1,2] 李宣东[1,2] 郑国梁[1,2] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室,南京210093 [2]南京大学计算机科学与技术系,南京210093

出　　处：《计算机学报》2004年第3期339-346,共8页Chinese Journal of Computers

基　　金：国家自然科学基金 ( 6 0 2 0 70 3 6 ;6 0 2 3 3 0 2 0 );国家"八六三"高技术研究发展计划基金 ( 2 0 0 1AA1 1 3 2 0 3 ;2 0 0 2AA1 1 6 0 90 );江苏省自然科学基金 (BK2 0 0 1 0 3 3 )资助

摘　　要：统一建模语言 (UML)自从成为OMG规范后 ,应用越来越广泛 .但UML没有精确的、形式化的语义阻碍了它的进一步发展 .该文基于Petri网 ,给出带时间约束的UML活动图的形式化描述 .与Petri网不同的是 ,Petri网的时间约束是在跃迁 (transition)上 ,而作者将UML活动图的时间约束放在活动状态上 .在此基础上 ,用整型时间的验证技术对实时活动图的时间性质加以分析 ,为实时系统的建模打下了基础 .Unified Modeling Language (UML) has been widely used since it became a standard of OMG. However, its lack of rigor and formal semantics prevents it further development. This paper extends UML activity diagrams with timing constraints for modeling real-time systems, and gives a formal description of UML activity diagrams based on Petri Net. Authors' work can be a basis of checking UML activity diagram models. Authors develop the algorithms for analyzing the real-time properties of activity diagram using integer time verification technology. UML activity diagrams are similar to Petri nets, However, in view of describing timed program behavior, authors put the constraints on activity states instead of on transitions in Petri Net.

关 键 词：UML 统一建模语言 OMG规范 面向对象 活动图 形式化分析 

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