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

摘要

统一建模语言(UML)自从成为OMG规范后,应用越来越广泛.但UML没有精确的、形式化的语义阻碍了它的进一步发展.该文基于Petri网,给出带时间约束的UML活动图的形式化描述.与Petri网不同的是,Petri网的时间约束是在跃迁(transition)上,而作者将UML活动图的时间约束放在活动状态上.在此基础上,用整型时间的验证技术对实时活动图的时间性质加以分析,为实时系统的建模打下了基础.