Analysing Message Sequence Graph Specifications

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. Technical Report IISc-CSA-2009-1, Department of Computer Science and Automation, Indian Institute of Science, Bangalore. 1 

• Type: Journal
• Year: 2010
• Where: ISOLA
• Authors: Joy Chakraborty, Deepak D'Souza, K. Narayan Kumar
• Keywords: Formal Methods, ISOLA 2010, Message Sequence Graph, MSG Specifications, Transition System