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

UML顺序图反映对象之间的消息交互顺序,在系统建模中应用十分广泛.对顺序图进行时间扩展得到UML时间顺序图,使其具备对实时系统建模的能力.在此基础上研究了UML建模工具和模型验证工具UPPAAL的接口信息,将UML时间顺序图模型转化为时间自动机模型,并对该系统模型进行形式化验证.设计和实现了基于XML的UML时间顺序图自动验证工具.