Record Details

Analysing Message Sequence Graph Specifications

Electronic Theses of Indian Institute of Science

View Archive Info
 
 
Field Value
 
Title Analysing Message Sequence Graph Specifications
 
Creator Chakraborty, Joy
 
Subject Data Transmission Modes
Message Communication
Message Sequence Charts
Message Sequence Graphs (MSG)
Messsage Sequence Graphs - Transition System
Computer Science
 
Description Message Sequence Charts are a visual representation of the system specification which shows how all the participating processes are interacting with each other. Message Sequence Graphs provide modularity by easily allowing combination of more than one Message Sequence Charts to show more complicated system behavior. Requirements modeled as Message Sequence Graphs give a global view of the system as interaction across all the participating processes can be viewed. Thus systems modeled as Message Sequence Graphs are like sequential composition of parallel process. This makes it very attractive during the requirements gathering and review phases as it needs inter-working between different stakeholders with varied domain knowledge and expertise – requirements engineers, system designers, end customers, test professionals etc.
In this thesis we give a detailed construction of a finite-state transition system for a com-connected Message Sequence Graph. Though this result is fairly well-known in the literature there has been no precise description of such a transition system. Several analysis and verification problems concerning MSG specifications can be solved using this transition system. The transition system can be used to construct correct tools for problems like model-checking and detecting implied scenarios in MSG specifications.
There are several contributions of this thesis. Firstly, we have provided a detailed construction of a transition system exactly implementing the message sequence graph. We have provided the detailed correctness arguments for this construction. Secondly, this construction works for general Message Sequence Graphs and not limited to com-connected graphs alone, although, we show that a finite model can be ensured only if the original graph is com-connected. Also, we show that the construction works for both synchronous and asynchronous messaging systems. Thirdly, we show how to find implied scenarios using the transition model we have generated. We also discuss some of the flaws in the existing approaches. Fourthly we provide a proof of undecidability argument for non com-connected MSG with synchronous messaging.
 
Contributor D'Souza, Deepak
 
Date 2011-03-29T05:03:32Z
2011-03-29T05:03:32Z
2011-03-29
2009-04
 
Type Thesis
 
Identifier http://etd.iisc.ernet.in/handle/2005/1102
 
Language en_US
 
Relation G23081