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

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

基于时间自动机的实时系统建模及验证

实时系统必须在一个事先定义好的时间限制内对来自外部或内部的事件进行响应,如何有效验证实时模型的正确性和安全性是一个难点。文章通过多个时间自动机来模拟实时系统中的各个对象,并用UPPAAL对模型进行验证,减少了模型验证的状态搜索空间,为实时嵌入式系统开发和验证提供了一种可行、安全的控制机制。实验结果显示了系统的有效性。