Show simple item record

dc.contributor.advisorD'Souza, Deepak
dc.contributor.authorChakraborty, Joy
dc.date.accessioned2011-03-29T05:03:32Z
dc.date.accessioned2018-07-31T04:40:16Z
dc.date.available2011-03-29T05:03:32Z
dc.date.available2018-07-31T04:40:16Z
dc.date.issued2011-03-29
dc.date.submitted2009
dc.identifier.urihttp://etd.iisc.ac.in/handle/2005/1102
dc.description.abstractMessage 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.en_US
dc.language.isoen_USen_US
dc.relation.ispartofseriesG23081en_US
dc.subjectData Transmission Modesen_US
dc.subjectMessage Communicationen_US
dc.subjectMessage Sequence Chartsen_US
dc.subjectMessage Sequence Graphs (MSG)en_US
dc.subjectMesssage Sequence Graphs - Transition Systemen_US
dc.subject.classificationComputer Scienceen_US
dc.titleAnalysing Message Sequence Graph Specificationsen_US
dc.typeThesisen_US
dc.degree.nameMSc Enggen_US
dc.degree.levelMastersen_US
dc.degree.disciplineFaculty of Engineeringen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record