摘要 |
Synthesizing a message sequence chart (MSC) from a communicating finite-state machine (CFSM), by 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, and mapping where each segment to a compositional MSC.
|