UML顺序图中消息的形式化描述与相关特性分析

摘要

为了实现基于UML顺序图的自动化测试,研究了顺序图中消息的形式化描述方法.形式化地定义了消息的发送和接收,并对二者的一致性关系进行了分析.提出了活动点的概念,讨论了其所具有的性质.建立了活动点集合上的二元关系描述方法,形式化地讨论了单个对象活动点集合与顺序图中全部活动点集合中该二元关系的具体表现.定义了消息集合上的二元关系,分析了其所具有的性质.最后,对顺序图中的时间约束特性和消息约束特性进行了形式化的分析.