Analysis of the Reachability of Timed UML Sequence Diagrams
UML时间顺序图的可达性分析

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.