Construction of Global State Transition Graph for Verifying Specifications Written in Message Sequence Charts for Telecommunications Software
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E84-D No.2 pp.249-261
- Publication Date
- 2001/02/01
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- PAPER
- Category
- Software Engineering
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Byeong Man KIM, Hyeon Soo KIM, Wooyoung KIM, "Construction of Global State Transition Graph for Verifying Specifications Written in Message Sequence Charts for Telecommunications Software" in IEICE TRANSACTIONS on Information,
vol. E84-D, no. 2, pp. 249-261, February 2001, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e84-d_2_249/_p
Copy
@ARTICLE{e84-d_2_249,
author={Byeong Man KIM, Hyeon Soo KIM, Wooyoung KIM, },
journal={IEICE TRANSACTIONS on Information},
title={Construction of Global State Transition Graph for Verifying Specifications Written in Message Sequence Charts for Telecommunications Software},
year={2001},
volume={E84-D},
number={2},
pages={249-261},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={February},}
Copy
TY - JOUR
TI - Construction of Global State Transition Graph for Verifying Specifications Written in Message Sequence Charts for Telecommunications Software
T2 - IEICE TRANSACTIONS on Information
SP - 249
EP - 261
AU - Byeong Man KIM
AU - Hyeon Soo KIM
AU - Wooyoung KIM
PY - 2001
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E84-D
IS - 2
JA - IEICE TRANSACTIONS on Information
Y1 - February 2001
AB - 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.
ER -
English
