Synthesis of Message Sequence Charts from Communicating Finite-State Machines

• US 20090235226A1
• Filed: 03/14/2008
• Published: 09/17/2009
• Est. Priority Date: 03/14/2008
• Status: Active Grant

• Current Assignee: Fujitsu Limited
• Original Assignee: Fujitsu Limited
• Inventors: Liu, Cong, MURTHY, Praveen K.
• Granted Patent: US 8,577,665 B2
• Time in Patent Office: Days
• US Class Current: 717/104
• CPC Class Codes: G06F 8/10 Requirements analysis; Specification techniques

Abstract

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.

Claims

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.

2. The method according to claim 1, further comprising harmonizing communication semantics of the CFSM with the MSC by specifying a plurality of First-In-First-Out (FIFO) message channels among a plurality of CFSMs according to a message type.

3. The method according to claim 1, wherein the transforming of the CFSM to the Petri net model comprises:

mapping each state of the CFSM states to a place of the Petri net;

marking each place corresponding to initial states from among the CFSM states;

modeling the message channels as places of the Petri net; and

modeling alternative state transitions as non-deterministic choices by inserting a silent transition,

wherein the generating the labeled finite digraph comprises searching states of the Petri net according to a firing of a transition in a free choice set of transitions, as a linearization of the Petri net states.

4. The method according to claim 1, wherein the generating of the labeled finite digraph comprises searching states of the Petri net according to a firing of a transition in a free choice set of transitions, as a linearization of the Petri net states.

5. The method according to claim 4, wherein the searching comprises repeatedly selecting a single transition in the free choice set of transitions as a single linearization from among alternative linearizations according to the minimum linearization time specified by a minimal T-invariant.

6. The method according to claim 5, wherein all possible transitions in the selected free choice set are searched.

7. The method according to claim 1, wherein the minimum linearization time is according to a T-invariant of the Petri net.

8. The method according to claim 1, wherein communication channels of the CFSMs have unbounded capacity.

9. An apparatus synthesizing a message sequence chart (MSC) from a communicating finite-state machine (CFSM), comprising:

a controller

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.

10. The apparatus according to claim 9, wherein the controller further harmonizes communication semantics of the CFSM with the MSC by specifying a plurality of First-In-First-Out (FIFO) message channels among a plurality of CFSMs according to a message type.

11. The apparatus according to claim 9, wherein the transforming of the CFSM to the Petri net model comprises:

mapping each state of the CFSM states to a place of the Petri net;

marking each place corresponding to initial states from among the CFSM states;

modeling the message channels as places of the Petri net; and

modeling alternative state transitions as non-deterministic choices by inserting a silent transition,

wherein the generating the labeled finite digraph comprises searching states of the Petri net according to a firing of a transition in a free choice set of transitions, as a linearization of the Petri net states.

12. The apparatus according claim 9, wherein the generating of the labeled finite digraph comprises searching states of the Petri net according to a firing of a transition in a free choice set of transitions, as a linearization of the Petri net states.

13. The apparatus according to claim 12, wherein the searching comprises repeatedly selecting a single transition in the free choice set of transitions as a single linearization from among alternative linearizations according to the minimum linearization time specified by a minimal T-invariant.

14. The apparatus according to claim 13, wherein all possible transitions in the selected free choice set are searched.

15. The apparatus according to claim 9, wherein the minimum linearization time is according to a T-invariant of the Petri net.

16. The apparatus according to claim 9, wherein communication channels of the CFSMs have unbounded capacity.