UML时间顺序图的可达性分析

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

Analysis of the Reachability of Timed UML Sequence Diagrams

For real-time systems,UML sequence diagrams describe interaction among objects,which shows the sce- narios of system behaviour. In this paper,we discuss about the reachability of the composition of UML sequence dia- grams,which can describe multi-scenarios. We can transform this problem to the corresponding timed automata,but the corresponding time automata has a large state space and the cost is large and not efficient. For these reasons,to solve part of the problem of reachability,we adapt a solution based on linear programming for its higher efficiency. The method of the solution is shown as follows: firstly,we traverse all simple path segments that can reach the given node to check the reachability; secondly,we traverse the path segments reaching the given node to check the reacha- bility,such path segments include all the loops at most once. In this paper,when we try to check the reachability of the given node,there may be three results: true,false and uncertain,for we haven't traversed all the path segments. Since some loops has nothing to do with the reachability,we try to distinguish those loops that have no relationship with the reachability in order to improve the algorithm.