1. A method of synthesizing a message sequence chart (MSC) from a communicating finite-state machine (CFSM), comprising: transforming the CFSM to a Petri net model; generating a labeled finite digraph with each path representing a linearization of an occurrence net segment of the Petri net; decomposing the diagraph into segments; mapping each segment to a compositional MSC; and outputting the compositional MSC.