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 real-time systems, in particular telecommunications 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 and 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.
- 社団法人電子情報通信学会の論文
- 2001-02-01
著者
-
Kim Byeong
School Of Computer And Software Eng. Kumoh National University Of Technology
-
Kim Hyeon
School Of Computer And Software Eng. Kumoh National University Of Technology
-
KIM Wooyoung
E-Speak Operation, Hewlett-Packard Company
-
Kim Wooyoung
E-speak Operation Hewlett-packard Company
関連論文
- Investigation of wafer warpage resulted from deep trench isolation in multi-layered SOI (Electron devices: 第15回先端半導体デバイスの基礎と応用に関するアジア・太平洋ワークショップ(AWAD2007))
- Investigation of wafer warpage resulted from deep trench isolation in multi-layered SOI (Silicon devices and materials: 第15回先端半導体デバイスの基礎と応用に関するアジア・太平洋ワークショップ(AWAD2007))
- A Small Size Dual-band MEMS Antenna using LC Resonators(Session 8B Emerging Devices and Technologies II,AWAD2006)
- A Small Size Dual-band MEMS Antenna using LC Resonators(Session 8B Emerging Devices and Technologies II)
- RF MEMS Technology
- A GA-Based Fuzzy Traffic Controller for an Intersection with Time-Varying Flow Rate(Artificial Intelligence, Cognitive Science)
- Fabricaton of Poly(dimethylsiloxane) Microlens for Laser-Induced Fluorescence Detection
- Potential of Thermo-Sensitive Hydrogel as an Actuator
- P107 Cytotoxicity of honey bee (Apis mellifera) venom in normal human lymphocytes and HL-60 cells
- A Morphology-independent Wafer Level Rivet Packaging with LEGO-like Assembly (先端デバイスの基礎と応用に関するアジアワークショップ(AWAD2005))
- A Morphology-independent Wafer Level Rivet Packaging with LEGO-like Assembly (先端デバイスの基礎と応用に関するアジアワークショップ(AWAD2005))
- Construction of Global State Transition Graph for Verifying Specifications Written in Message Sequence Charts for Telecommunications Software
- Potential of Thermo-Sensitive Hydrogel as an Actuator
- New DC Arc Discharge Synthesis Method for Carbon Nanotubes Using Xylene Ferrocene as Floating Catalyst