UML时间顺序图的自动验证技术  

The automated verification technology of UML time sequence diagram

作　　者：陈江[1,2] 陈建国[1] 陆慧娟[1] 唐文彬[1] 

机构地区：[1]中国计量学院信息工程学院,浙江杭州310018 [2]浙江网新恒天软件技术有限公司,浙江杭州310030

出　　处：《中国计量学院学报》2010年第2期124-129,共6页Journal of China Jiliang University

基　　金：浙江省科技厅重大科技专项(No.2007C13091)

摘　　要：UML顺序图反映对象之间的消息交互顺序,在系统建模中应用十分广泛.对顺序图进行时间扩展得到UML时间顺序图,使其具备对实时系统建模的能力.在此基础上研究了UML建模工具和模型验证工具UPPAAL的接口信息,将UML时间顺序图模型转化为时间自动机模型,并对该系统模型进行形式化验证.设计和实现了基于XML的UML时间顺序图自动验证工具.The UML sequence diagram was widely used in the system modeling reflects the sequence of message interaction in objects.To extend a sequence diagram by the time feature,the UML time sequence diagram was the capacity for real-time system modeling.On the basis of the interface information between the UML modeling tool and the model verification tool UPPAAL,the UML time sequence diagram transferd into timed automata model and performs the formal verification to the system model.Based on the XML,automatic verif...

关 键 词：UML时间顺序图 自动验证 系统建模 

分 类 号：TP302.7[自动化与计算机技术—计算机系统结构]