Message Sequence Chart (MSC) standardized by International Telecommunication Union is a graphical and textual language for specification of concurrent systems. It has been used formally as well as informally to specify behavior of real-time systems, in particular telecommunication switching systems. Formal verification of a system specification is crucial to ensure that implementation of the system works correctly. In particular, verification methods based on finite states have been widely used in telecommunication systems design. The methods determine global system states and transitions between them (i. e. , build a global state transition graph (GSTG)), and verify the system's desired properties, such as safety and liveness, on the GSTG. In this paper, we focus on construction of GSTGs from MSC specifications. We propose action dependency graph as an intuitive description of semantics of MSC specifications and present an algorithm to translate MSC specifications to action dependency graphs as well as an algorithm to construct a global state transition graph from an action dependency graph.

A protocol completion method is proposed to transform protocols synthesized from service specifications into error-free protocols. Communication service specifications described by message sequence charts can be synthesized into protocols. The synthesized protocols may include latent exceptional behaviors that are beyond the given service specifications. Therefore, even if the service specifications themselves are verified, these exceptional behaviors may produce protocol errors such as deadlock states or unspecified reception. Error-free protocols can be obtained from error-free service specifications by synthesizing and then completing the synthesized protocols. By taking account of each service specification through protocol completion, every exceptional behavior can be detected in the protocol entities including erroneous exceptional behaviors. This function can also be applied to resolution of feature interactions. The proposed method is applied to the synthesis of the X.227 protocol from its partial service specifications.

This paper discusses how to derive message sequence charts (MSCs) from a set of state transition descriptions. Recently, MSC notation has received much attention in the communications software field because it graphically shows system global behavior, So MSC handling techniques are being widely studied. These studies have recommended the design a system by a set of formal MSCs in the early stages of development and then to convert them into state transition descriptions. However, it is difficult to apply those results to existing communications software products. This is because these systems are designed based on state transition descriptions and there are no formal MSCs for them. In this paper, we propose a method of deriving MSCs based on optimized reachability analysis. This method generates MCSs that avoid state explosion. A case study using Q.931 protocol shows the feasibility of this method.