The search functionality is under construction.
The search functionality is under construction.

Author Search Result

[Author] Wooyoung KIM(1hit)

1-1hit
  • Construction of Global State Transition Graph for Verifying Specifications Written in Message Sequence Charts for Telecommunications Software

    Byeong Man KIM  Hyeon Soo KIM  Wooyoung KIM  

     
    PAPER-Software Engineering

      Vol:
    E84-D No:2
      Page(s):
    249-261

    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.