摘要： 对于实时系统来说，UML顺序图描述了对象之间的交互。对象之间的交互展现了系统行为的场景。本文中，我们针对描述多场景的UML顺序图组合中的可达性问题进行研完。尽管这个问题可以转换为相应的时间自动机，然后进行处理，但其转化为之后，状态空间巨大，解决的开销比较大，效率不高。针对部分可达性问题，本文采用更为高效的基于线性规划的解决方案，其思想如下：首先遍历所有到达给定节点的简单路径片断来验证可达性，随后遍历到达给定节点的并且包含所有循环至多一次的路径片断来验证可达性。由于我们并没有遍历所有路径片断，因此用本文的方

关键词: 顺序图 UML 可达性分析 时间自动机 实时系统 系统行为 状态空间 解决方案 线性规划 行处理 片断 路径 节点 遍历 循环 不确定 交互 对象 场景 验证 算法