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

摘要

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 ral-time systems, in particular telecommunication switching sys- tems. 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.