Analysing Message Sequence Graph Specifications
Joy Chakraborty, Deepak D'Souza, K. Narayan Kumar

IISc-CSA-TR-2009-1
(March 2009)

Available formats: [pdf]

Filed on March 17, 2009
Updated on May 14, 2009


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.
The transition system we give can also be used for a bounded analysis
of general (not necessarily com-connected) MSG specifications.


Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2009/1/.

Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]