Timing analysis of MSC specifications with asynchronous concatenation

Message Sequence Chart (MSC) is a graphical and textual language for describing the interactions between system components, and MSC specifications (MSSs) are a combination of a set of basic MSCs (bMSCs) and a High-level MSC that describes potentially iterating and branching system behavior by specifying the compositions of basic MSCs, which offer an intuitive and visual way of specifying design requirements. With concurrent, timing, and asynchronous properties, MSSs are amenable to errors, and their analysis is important and difficult. This paper deals with timing analysis of MSC specifications with asynchronous concatenation. For an MSC specification, we require that for any loop, its first node be flexible in execution time and its any associated external timing constraint be enforced on the entire loop. Such an MSC specification is called a flexible loop-closed MSC specification (FLMSS). We show that for FLMSSs, the reachability analysis and bounded delay analysis problems can be solved efficiently by linear programming. The solutions have been implemented into our tool TASS and evaluated by experiments.