=Paper=
{{Paper
|id=None
|storemode=property
|title=A Petri Net Approach to Synthesize Intelligible State Machine Models from Choreography
|pdfUrl=https://ceur-ws.org/Vol-851/paper17.pdf
|volume=Vol-851
|dblpUrl=https://dblp.org/rec/conf/apn/MiyamotoH12
}}
==A Petri Net Approach to Synthesize Intelligible State Machine Models from Choreography==
https://ceur-ws.org/Vol-851/paper17.pdf
A Petri Net Approach to Synthesize Intelligible
State Machine Models from Choreography?
Toshiyuki Miyamoto1 and Yasuwo Hasegawa1
Graduate School of Engineering, Osaka University,
Suita, Osaka 565-0871, Japan
miyamoto@eei.eng.osaka-u.ac.jp
Abstract. Application of service-oriented architecture, which builds the
entire system by a combination of independent software components, to
a wide variety of computer systems is expected. The problem to synthe-
size state machine models of the services from a communication diagram
representing the overall specifications of service interaction is known as
the choreography realization problem. It should be minded on automatic
synthesis that software models should be simple to be understood easily
by software engineers. In this paper, we propose a method to synthesize
hierarchical state machine models for the choreography realization prob-
lem. The proposed method is evaluated using a metric for intelligibility.
1 Introduction
In recent years, the internationalization of activities and information technology
in the enterprise has intensified competition between companies. Companies are
under pressure to respond quickly to business needs, and the period for making
changes to existing business and launching new businesses has been shortened.
For this reason, the need to change or build quickly information systems has
been increasing.
Under such circumstances, service-oriented architecture (SOA)[12] has been
attracting attention as the architecture of information systems in the enterprise.
In SOA, an information system is built by composing independent software units
called services.
In this paper, we consider the problem of synthesizing a concrete model from
an abstract specification. It is not easy for the designers to design a concrete
model directly from requirements since there exists huge gaps. But, defining an
abstract specification is relatively simple. Therefore, if we can automatically syn-
thesize a concrete model from abstract high-quality specification, it is expected
that designer’s workload is greatly reduced and product quality is improved.
In the field of software engineering, there exist several investigations that syn-
thesize the concrete model from the abstract specification. Harel et al. proposes
a methodology for synthesizing statechart models from scenario-based require-
ments[5]. Whittle et al. proposes a methodology for synthesizing hierarchical
?
This work was supported by KAKENHI (23500045).
T. Miyamoto, Y. Hasegawa: Synthesize Intelligible State Machine Models 223
state machine models from expressive scenario descriptions[13]. Liang et al. de-
fines a set of comparison criteria, and surveys 21 different synthesis approaches
presented in literature based on the criteria[7]. In addition, the theory of regions
has been attracting attention as a method to synthesize nets[3].
In SOA, the problem to synthesize the concrete model from an abstract
specification is known as the choreography realization problem[11]. In which
the abstract specification, called choreography, is defined as a set of interactions
among services, which are given in a dependency relation of messages sent and
received; the concrete model is called the service implementation which defines
the behavior of the service. This paper utilizes the communication diagram and
the state machine of UML 2.x[10] to describe the choreography and the service
implementation, respectively.
Bultan and Fu formally introduced the choreography realization problem in
[2]. They used collaboration diagrams of UML1.x and showed some conditions
for a given choreography to be realizable. In addition, they showed a method
to represent the service implementation as the state space in which a state was
defined as a set of unsent messages, and they also showed a method to map to
a set of finite state machines. However, it is not intelligible because the number
of states increases exponentially as the number of messages increases. Further-
more, they have adopted the semantics that message send and receive events for
a synchronous call occur simultaneously. Under this semantics, the UML speci-
fication that “the execution of the call operation action waits until the execution
of the invoked behavior completes and a reply transmission is returned to the
caller”[10] can not be represented.
Miyamoto et al. have proposed a method to synthesize hierarchical state
machines from the choreography given in communication diagrams[8]. In the
method, dependency constraints between message send and receive events are
represented by Petri nets[9]; the state machine is synthesized from its reach-
ability space. A method to extract the hierarchical structure by analyzing the
reachability space is given, but the technique can only be applied to simple cases.
This paper proposes a method of converting a Petri net into the state machine
directly. It is shown that there is a relation between the possibility of direct
conversion and structural properties of Petri nets. At first the proposed method
converts the Petri net so as to satisfy the structural properties, then it converts
Petri nets into hierarchical state machines without generating their state spaces.
This paper is organized as follows. Section 2 introduces an UML subset,
called subset of UML for formally describing choreography and behavioral feature
(cbUML), to discuss the choreography realization problem, and an extended
Petri net, called message mark graph (MMG). The proposed method, called
Construct State-machine Cutting Bridges (CSCB) method, is evaluated in terms
of the intelligibility in Sect. 3. However, in this paper it is assumed that the
choreography is given in a single communication diagram as the first stage of
the study. Section 4 is the conclusion.
224 PNSE’12 – Petri Nets and Software Engineering
2 Preliminaries
2.1 cbUML
Let us introduce a subset of UML, called cbUML, for the discussion in this paper.
Definition 1 (cbUML). cbUML is a tuple (C, M, A, CD, SM), where C is the
set of classes, M is the set of messages, A is the set of attributes, CD is the
set of communication diagrams, and SM is the set of state machines. Each of
messages and attributes is owned by a class, and behavior of a class is defined
by a state machine.
Messages The set M of messages are partitioned with respect to the sort of
messages: M = Msop ∪ Maop ∪ Mrep , where Msop is the set of synchronous
messages generated by synchronous calls, Maop is the set of asynchronous mes-
sages generated by asynchronous calls, and Mrep is the set of reply messages
to synchronous messages. Let Ms = Msop and Ma = Maop ∪ Mrep . Corre-
spondence between the synchronous call and its response is given by the func-
tion ref er : M 7→ M ∪ {nil}, such that ∀m ∈ Msop : ref er(m) ∈ Mrep ,
∀m ∈ Mrep : ref er(m) ∈ Msop , and ∀m ∈ Maop : ref er(m) = nil. Note that
∀m ∈ Msop ∪ Mrep : ref er(ref er(m)) = m.
There is a difference in behavior during interactions due to differences in the
sort of message as follows: In a synchronous call, caller’s execution is stopped
until it receives a reply from the callee. On the other hand, in the asynchronous
call, the caller is possible to continue to operate, regardless of the behavior of
the callee side.
In UML, each message has two events: a send event and a receive event. For a
synchronous message, it is considered that they occur simultaneously. However,
for the later discussion we need two events that occur separately. Therefore
we define that each synchronous message has two events: a preparation event
for message sending and a send-receive event, where the preparation event is a
caller’s event and the send-receive event is a callee’s event. A preparation event
and a send-receive event for a synchronous message m ∈ Ms are denoted by $m
and !m, respectively. For an asynchronous message m ∈ Ma , its send event and
receive event are denoted by !m and ?m, respectively. Hereafter a send event is a
send-receive event for a synchronous message or a send event for an asynchronous
message. The set Σ of message events and the set ∆ of send events are defined
as follows:
Σ = {$m, !m | m ∈ Ms } ∪ {!m, ?m | m ∈ Ma }, and
∆ = {!m | m ∈ M}.
Communication Diagrams Communication diagrams show interactions where
the arcs between the communicating lifelines are decorated with description of
the passed messages and their sequencing.
T. Miyamoto, Y. Hasegawa: Synthesize Intelligible State Machine Models 225
Check1
Service1 Service3 Service6
Ack1
Check4
Req1
Answer
Check2 Check5
Service2 Service4
ReplyCheck2
Info1
Check3
Service5
Fig. 1. A communication diagram
!Req1_rep
!Check2 !Check5
!Req1
!Check1
!Check4 !Check5_rep
!ReplyCheck2 !Answer
!Ack1
!Check3
!Info1
Fig. 2. Dcd
Definition 2 (Communication Diagram). A communication diagram cd ∈
CD is a tuple cd = (Ccd , Mcd , Conncd , linecd , Dcd ), where Ccd ⊆ C is the set of
instances of classes (called lifelines or objects) in cd, Mcd ⊆ M is the set of
messages in cd, Conncd ⊆ Ccd × Ccd is the set of connectors, which is given as a
symmetric relation on Ccd , linecd : Mcd 7→ Conncd assigns a connector for each
message, and Dcd ⊆ ∆cd × ∆cd is a dependency relation among send events.
Note that the reflexive and transitive closure of Dcd is a partial order.
A conversation is the sequence of messages exchanged among the objects.
The set of conversations defined by a communication diagram cd is denoted by
∗
C(cd) ⊆ 2M , where M∗ is the set of all sequences of messages.
Definition 3. A conversation σ = m1 m2 · · · mn is in C(cd) if and only if σ ∈
M∗ and the corresponding sequence γ =!m1 !m2 · · ·!mn of send events satisfies
∀i, j ∈ [1..n] : (!mi , !mj ) ∈ Dcd ⇒ i < j.
Figure 1 shows a communication diagram. In this example, messages Req1
and Check5 are synchronous messages, and dashed lines with open arrow head
are their reply messages. Suppose that the dependency relation among send
events is given as shown in Fig. 2, where rhombuses, rectangles, and ellipses
indicate synchronous calls, their reply, and asynchronous calls, respectively. The
following sequence is a conversation of the example.
σ = Req1 Check1 Req1_rep Check2 Check3
226 PNSE’12 – Petri Nets and Software Engineering
State Machines The behavior of each object is described by a state machine.
Definition 4 (State Machine). A state machine is a tuple sm = (Vsm , Rsm ,
topsm , contsm , T Rsm , Esm , Constsm , Behsm ), where Vsm = SSsm ∪CSsm ∪F Ssm ∪
ISsm is the set of vertices1 , Rsm is the set of regions, top ∈ Rsm is the top re-
gion, contsm : (Vsm ∪ Rsm ) \ {topsm } 7→ (CSsm ∪ Rsm ) is an ownership relation
between vertices and regions, T Rsm is the set of transition relations, Esm is
the set of events, Constsm is the set of constraints, and Behsm is the set of
behaviors.
In UML state machines, although there are various kinds of states and
pseudo-states, only simple states, composite states, final states, and initial pseudo-
states are used in this paper. A composite state is able to own one or more
regions, and a region is able to own vertices. The function contsm represents
the ownership of vertices and regions, and contsm (x1 ) = x2 means that x1 is
owned by x2 . For a x ∈ Vsm ∪ Rsm , let des(x) = {x0 | ∃i > 0 : contism (x0 ) = x}
be the set of descendants of x, where cont1sm (·) = contsm (·) and contism (·) =
sm (·)) (i > 1).
contsm (conti−1
Definition 5 (Orthogonal State). If there exist vertices v1 , v2 ∈ Vsm and
different regions r1 , r2 ∈ Rsm , r1 6= r2 such that contsm (r1 ) = contsm (r2 ),
v1 ∈ des(r1 ), and v2 ∈ des(r2 ), two vertices v1 , v2 are called orthogonal, and
denoted by v1 ⊥ v2 .
Definition 6. A set V̂sm ⊂ Vsm of vertices is called consistent if and only if for
each pair v1 , v2 ∈ V̂sm of vertices v1 ⊥ v2 , v1 ∈ des(v2 ), or v2 ∈ des(v1 ).
The set Esm of events is given as Esm = Σsm ∪ {τ }, where Σsm is the set of
message events in the state machine and τ is the completion event that occurs
when a transition with no trigger event fires.
A transition relation etr ∈ T Rsm is a tuple etr = (src, trig, grd, ef f, tgt),
where src ∈ Vsm is the originating vertex of the transition, a trigger trig ∈
Esm is the event that makes the transition fire, a guard grd ∈ Constsm is
a constraint, an effect ef f ∈ Behsm is an optional behavior to be performed
when the transition fires, and tgt ∈ Vsm is the target vertex. Note that {src, tgt}
must not be consistent. According to the UML specification[10], triggers, guards,
and effects are denoted like “trig[grd]/ef f ” in diagrams. It is supposed that
Σsm ⊆ Behsm , and a caller’s event of message sending becomes an effect and a
callee’s event becomes a trigger.
Due to space limitations, the details of operational semantics of state ma-
chines are omitted, and the steps of doing synchronous calls and asynchronous
calls are explained by examples.
Figure 3 shows the execution of the asynchronous call. Gray states are active.
When state machine sm1 transitions from state s11 to state s12 by the occurrence
of the completion event, an asynchronous call is executed. At this time the send
1
SSsm is the set of simple states, CSsm is the set of composite states, F Ssm is the set
of final states, and ISsm is the set of initial pseudo states.
T. Miyamoto, Y. Hasegawa: Synthesize Intelligible State Machine Models 227
s11 s21 s11 s21 s11 s21
m
/!m ?m /!m ?m /!m ?m
s12 s22 s12 s22 s12 s22
sm1 sm2 sm1 sm2 sm1 sm2
Fig. 3. Steps for an asynchronous call
m rm
s21 s21 s21 s21 s21
s11 s11 s11 s11 s11
!m !m !m !m !m
/$m s22 /$m s22 /$m s22 /$m s22 /$m s22
s12 !rm s12 !rm s12 !rm s12 !rm s12 !rm
s23 s23 s23 s23 s23
sm1 sm2 sm1 sm2 sm1 sm2 sm1 sm2 sm1 sm2
Fig. 4. Steps for a synchronous call
event !m occurs, and the message m will be appended at the end of the queue of
sm2. The state machine sm2 transitions from state s21 to state s22 consuming
the message m by the occurrence of the receive event ?m.
Figure 4 shows the execution of the synchronous call. A synchronous call is
executed in sm1. At this time, the preparation event $m occurs in sm1, and the
region that contains the transition is suspended. In addition, the message m is
appended at the end of the queue of sm2. The state machine sm2 transitions
from state s21 to s22 consuming the message m by the occurrence of the send-
receive event !m. The sm2 sends a reply message rm to sm1 on transitioning
from s22 to s23. At this time the send event !rm occurs, and the message rm
is appended at the end of the queue of sm1. The sm1 releases the suspended
region, and transitions from state s11 to state s12 consuming the reply message
rm by the occurrence of the receive event ?rm. Note that the receive event ?rm
does not appear in the state machine, because we are using the region suspend
mechanism.
The set of all conversations obtained by the execution of a set SM of state
machines is denoted by C(SM).
2.2 Petri nets
The proposed method represents the dependency relation between message send
an receive events by using Petri nets[9]. Since this paper assumes that the chore-
ography is given by a communication diagram, Petri nets that appear in this
paper are marked graphs.
A Petri net N = (P, T, F, W ) is called ordinary when ∀(x, y) ∈ F : W (x, y) =
1. Then the weight function W is omitted. For x ∈ P ∪ T , the set {y ∈ P ∪ T |
(y, x) ∈ F } is called the preset of x, and denoted by •x. In the same way, the
set {y | (x, y) ∈ F } is called the postset of x, and denoted by x•.
228 PNSE’12 – Petri Nets and Software Engineering
A place p ∈ P is called a source place and a sink place when •p = ∅ and
p• = ∅, respectively. In the same way a transition t ∈ T is called a source
transition and a sink transition when •t = ∅ and t• = ∅, respectively. A transition
t is called a fork transition and a join transition when |t • | ≥ 1 and | • t| ≥ 1,
respectively. The sets of join transitions and fork transitions are denoted by Tjoin
and Tf ork , respectively. Under the standard definition, if ∀p ∈ P : | • p| = 1 and
|p • | = 1, then the Petri net is called a marked graph. In this paper, we relax the
condition as ∀p ∈ P : | • p| ≤ 1 and |p • | ≤ 1.
Definition 7 (Message Marked Graph). A message marked graph (MMG)
is a tuple N = (P, T, F, W, G, A), where the underlying Petri net (P, T, F, W )
satisfies the following conditions:
1. N is an ordinary and acyclic,
2. there exist only one source place ps and only one sink place pe ,
3. no source transitions and sink transitions exist, and
4. |ps • | = 1, | • pe | = 1, and ∀p ∈ P \{ps , pe } : [| • p| = 1, |p • | = 1].
G : T 7→ 2T is a firing constraint, and the partial function A : T 7→ Σ assigns
an event for the transition.
A state of MMG is expressed by a pair (M, X), where M : P 7→ Z+ is a
marking and X : T 7→ B is a firing configuration, where Z+ is the set of non-
negative integers and B = {true, false}. The initial state (M0 , X0 ) of MMG is
given as follows:
(
1 if p = ps
M0 (p) =
0 otherwise, and
X0 (t) = false (∀t ∈ T ).
A transition t ∈ T is enabled if and only if ∀p ∈ •t : M (p) ≥ W (p, t) and
∀t0 ∈ G(t) : X(t0 ) = true. A new state (M 0 , X 0 ) obtained by the firing of
transition t is given as follows:
M 0 (p) = M (p) − W (p, t) + W (t, p), and
(
0 0 true if t0 = t
X (t ) =
X(t ) otherwise.
0
Handles and Bridges Let N = (P, T, F ), and N1 = (P1 , T1 , F1 ) be a subnet
of N . An elementary path H = (n1 , . . . , nr ), r ≥ 2 of N is a handle of N1 if and
only if H ∩ (P1 ∪ T1 ) = {n1 , nr }.
Let N = (P, T, F ), and N1 = (P1 , T1 , F1 ) and N2 = (P2 , T2 , F2 ) be subnets
of N . An elementary path B = (n1 , . . . , nr ), r ≥ 2 is a bridge from N1 to N2 if
and only if B ∩ (P1 ∪ T1 ) = {n1 } and B ∩ (P2 ∪ T2 ) = {nr }.
For a transition t ∈ T , F J(t) ⊆ T is a set of terminal vertices of handles
starting from t. Similarly, JF (t) ⊆ T is a set of starting vertices of handles
terminating at t. Please refer to [4] for more detail about handles and bridges.
T. Miyamoto, Y. Hasegawa: Synthesize Intelligible State Machine Models 229
Convertible MMG Intuitively, if two states in a state machine are consistent,
both states may be active concurrently. The UML specification prohibits draw-
ing a transition between consistent states. An MMG is a representation of the
relationship between the order of the messages in the marked graph; in general
cases a state machine which satisfies the specification can not be directly, namely
without generating its state space, derived from the MMG.
Let us introduce a subclass of MMG called the convertible MMG (CMMG),
from which we can get a state machine satisfying the specification directly by
using Algorithm 1 shown later.
Definition 8. A MMG is called a CMMG if the following conditions hold:
1. |Tf ork | = |Tjoin |
2. Tf ork ∩ Tjoin = ∅
3. For any pair of handles H, H 0 in the MMG, only one of following conditions
holds: (a) H and H 0 share the same starting vertex and the same termi-
nal vertex, and (b) the starting vertices of H and H 0 are different and the
terminal vertices of H and H 0 are different.
4. If A(t) = $m, then t • • = {t0 }, A(t0 ) =?ref er(m).
From the definition of CMMG, for all t ∈ Tf ork (resp. t ∈ Tjoin ) |F J(t)| = 1
(resp. |JF (t)| = 1). Moreover the following lemma holds.
Lemma 1. Let N be a MMG, N1 be a subnet of N , and H be a handle of N1 .
If N is a CMMG, then there is no bridge from H to N1 .
Algorithm 1 shows how a CMMG is converted to a state machine. In the
algorithm, if A(t) ∈ {!m | m ∈ Ms } ∪ {?m | m ∈ Ma } then Event(t) = A(t), and
Constraint(t) = ∧a∈G(t) f ireda . The mapping Behavior(t) is given as follows:
own(m).m(· · · ) if A(t) ∈ {$m | m ∈ Msop }
Behavior(t) = send m(· · · ) to own(m) if A(t) ∈ {!m | m ∈ Maop }
reply to m(· · · ) if A(t) ∈ {!m | m ∈ Mrep }
where, own(m) is the owner object of message m, and in cbUML these ex-
pressions show a synchronous call, an asynchronous call, and a reply for a syn-
chronous call. In addition, if f iredt ∈ A, then add an expression ‘f iredt = true’
to Behavior(t). The ‘new’ expression shows a new element is generated.
Lemma 2. A CMMG is directly convertible to a state machine.
Figure 5 shows an example of CMMG, and Fig. 6 is the synthesized state
machine by Algorithm 1. In Fig. 5, places on each edge, ps and pe are omitted.
3 Choreography Realization Problem
3.1 Choreography Realization Problem
By a single communication diagram, one scenario that is an interaction of objects
in the system are described. All behavior of the system is given by a set of
communication diagram; this is referred to as choreography.
230 PNSE’12 – Petri Nets and Software Engineering
Algorithm 1: Converting CMMG to a state machine
Input: CMMG (P, T, F, G, A)
Output: State machine (V, R, top, cont, T R, E, Const, Beh), Attribute A
1 begin
S
2 A ← {f iredt | t ∈ t0 ∈T G(t0 )};
3 E ← {Event(t) | t ∈ T };
4 Const ← {Constraint(t) | t ∈ T };
5 Beh ← {Behavior(t) | t ∈ T };
6 V ← ∅;
7 R ← ∅;
8 tinit ← ps •;
9 tend ← •pe ;
10 top ← new Region();
11 RNG(tinit , top, tend );
12 RNG(t, r, te )
13 ip ← new InitialPseudoState(); cont(ip) ← r;
14 if Event(t) = Constraint(t) = ε then
15 s ← ip
16 else
17 s ← new SimpleState(); cont(s) ← r;
18 new Transition (ip, ε, ε, ε, s);
19 while t 6= te do
20 ev ← Event(t); const ← Constraint(t); beh ← Behavior(t);
21 if ev = const = beh = ε ∧ |t • | = 1 then
22 t ← t • •; continue;
23 if A(t) ∈ {$m | m ∈ Ms } then t ← t • •;
24 if |t • | ≥ 2 then
25 s0 ← new CompositeState(); cont(s0 ) ← r;
26 forall the p0 ∈ t• do
27 r0 ← new Region(); cont(r0 ) ← s;
28 RN G(p0 •, r0 , F J(t));
29 t ← F J(t) ;
30 else
31 s0 ← new SimpleState(); cont(s0 ) ← r;
32 t ← t • •;
33 new Transition (s, ev, const, beh, s0 );
34 s ← s0 ;
35 f s ← new FinalState();
36 new Transition (s, ε, ε, ε, f s);
Intuitively, the choreography realization problem is the problem to determine
whether it is possible to synthesize a set of state machines which realize the
choreography. In addition, it is desired to synthesize the state machines. The
choreography realization problem is formally defined as follows.
T. Miyamoto, Y. Hasegawa: Synthesize Intelligible State Machine Models 231
Service6-init
!Check5 ?Check4
Check5 / Check4 /
!Check5_rep
/ reply to Check5;
Service6-end
Fig. 5. CMMG Fig. 6. Generated state machine
Problem 1. For a given set CD of communication diagrams, is it possible to
synthesize the set SM of state machines which satisfy C(CD) = C(SM)? If
possible, obtain the set of state machines.
In the case of un-realizable choreography, is is desired to synthesize state
machines which behave as close to the choreography as possible. It is called
weakly realizable if there exist state machines which satisfy C(CD) ⊇ C(SM).
For a weakly realizable choreography, obtain the set of state machines whose
C(SM) is maximal.
In [2], sufficient realizability conditions for a class of collaboration diagrams
have been shown. We suppose that given CD is (weak) realizable hereafter and
the set CD contains only one communication diagram.
3.2 CSCB Method
The proposed CSCB method synthesizes state machines from a communication
diagram as below. Due to space limitations the details of the algorithm are
omitted.
1. Construct a dependency relation ⇒cd on the set of events.
For each object c, perform the following steps.
2. Derive a dependency relation ⇒ccd from ⇒cd .
3. Construct an MMG from ⇒ccd .
4. Cut T-T bridges from the MMG.
5. Separate fork and join transitions in the MMG.
6. Find one-to-one correspondence between Tf ork and Tjoin in the MMG.
7. Perform Algorithm 1.
232 PNSE’12 – Petri Nets and Software Engineering
?Req1_rep
!Req1_rep $Check5 !Check5
?Check2
!Check2
!Check4 ?Check4 !Check5_rep
$Req1 !Req1 !Check1 ?Check5_rep
?Check1
!Ack1 !ReplyCheck2 ?ReplyCheck2 !Answer ?Answer
?Ack1
!Check3 ?Info1
?Check3 !Info1
Fig. 7. ⇒cd
Service1-init Service2-init Service3-init Service4-init Service5-init Service6-init
$Req1 !Req1 ?Check1 ?Check2 ?Check3 !Check5 ?Check4
?Req1_rep !Check1 !Ack1 !Check4 $Check5 ?Info1 !Info1 !Check5_rep
?Answer !Check2 !Check3 Service3-end ?Check5_rep Service5-end Service6-end
Service1-end !Req1_rep ?ReplyCheck2 !ReplyCheck2
?Ack1 !Answer Service4-end
Service2-end
Fig. 8. ⇒ccd and MMGs for Service1, Service2, ... are shown from left to right.
Construction of dependency relation ⇒cd The dependency relation ⇒cd ⊆
Σcd × Σcd on the set of events is given by the following expression:
⇒cd =Dcd ∪ {($m, !m) | m ∈ Mcd cd
s } ∪ {(!m, ?m) | m ∈ Ma }
∪ {(?m1 , !m2 ) | m1 ∈ Mcd cd
a , m2 ∈ Ma , (!m1 , !m2 ) ∈ Dcd }
∪ {(?m1 , $m2 ) | m1 ∈ Mcd cd
a , m2 ∈ Ms , (!m1 , !m2 ) ∈ Dcd }
∪ {(!m1 , $m2 ) | m1 ∈ Mcd cd
s , m2 ∈ Ms , (!m1 , !m2 ) ∈ Dcd }
Figure 7 shows the dependency relation ⇒cd for the communication diagram
shown in Fig. 1.
Deriving ⇒ccd and Construction of MMG At first, ⇒cd is transitively
reduced, then the dependency relation ⇒ccd for each object c is derived. At this
time, in order to satisfy the condition 4 of CMMG, for all synchronous message
m ∈ Ma , if there exists an event e 6=?ref er(m) such that ($m, e) ∈⇒ccd , then a
relation (?ref er(m), e) is added in ⇒ccd .
The dependency relations ⇒ccd , which are derived from the dependency re-
lation ⇒cd shown in Fig. 7, are shown in Fig. 8. Here, since ($Req1, ?Req1r ep),
T. Miyamoto, Y. Hasegawa: Synthesize Intelligible State Machine Models 233
A A
(D)
C
C
B B
Fig. 9. Separating fork and join
transition Fig. 10. Finding one-to-one correspondence
($Req1, ?Answer) ∈⇒ccd for Service1, a relation (?Req1r ep, ?Answer) is added
in ⇒Service1
cd .
MMGs are constructed by converting vertices into transitions, adding a place
for each edge, and adding source and sink places in Fig. 8.
Cutting T-T bridges As shown in Lemma 1, since bridges are unnecessary in
CMMGs, they are cut. In the example in Fig. 8, (!Check1 !Check2 ?ReplyCheck2)
of Service2 is a bridge. After removing edges (!Check1, !Check2) and (!Check2,
?ReplyCheck2), edge (Service2-init, !Check2) and (!Check2, Service2-end) are
added. At that time, in order to avoid changing the behavior, the following
firing conditions are added.
(
!Check1 if A(t) = !Check2
G(t) =
!Check2 if A(t) = ?ReplyCheck2
Cutting all bridges is not always necessary. Let U be a set of bridges and
f : U 7→ 2U be a function such that f (u) is a set of bridges which will not
be bridges by cutting bridge u. Then, the problem to finding the set of bridges
results in the set cover problem[6].
Separating fork and join transitions If there exists fork and join transition,
it is split into a fork transition and a join transition as shown in Fig. 9.
Finding one-to-one correspondence As shown in Fig. 10, dummy transition
D is added in order to find one-to-one correspondence between fork and join
transitions..
Lemma 3. The MMG obtained by applying steps 1∼6 of CSCB method is a
CMMG.
Figure 11 shows CMMGs obtained from MMG in Fig 8.
Conversion into state machines By performing Algorithm 1, state machines
shown in Fig.s 12, 14, 13, 15, 16, and 6 are obtained.
234 PNSE’12 – Petri Nets and Software Engineering
Service1-init Service2-init Service3-init Service4-init Service5-init Service6-init
$Req1 !Req1 ?Check1 ?Check2 ?Check3 !Check5 ?Check4
?Req1_rep !Check1 !Check3 !Ack1 !Check4 $Check5 ?Info1 !Info1 !Check5_rep
?Answer !Req1_rep [!Check2]?ReplyCheck2 Service3-end ?Check5_rep Service5-end Service6-end
Service1-end ?Ack1 !Answer [!Check1]!Check2 !ReplyCheck2
Service4-end
Service2-end
Fig. 11. CMMG of the example
/ Service2.Req1();
Check1 / /send Ack1 to /send Check4 to
Answer / Service2; Service6;
Fig. 12. State machine of Service1 Fig. 13. State machine of Service3
3.3 Intelligibility Evaluation
Antonio et al. have experimentally evaluated the relationship between metrics
and intelligibility of the state machines by measuring time to understand state
machines[1]. According to the result, state machines are intelligible the smaller
the following metrics: the number of simple states (NSS), the number of transi-
tions (NT), and the number of guards (NG). In this section, the CSCB method
Req1 /
/reply to Req1; /send Check1 to Service3; /send Check3 to Service5;
fired_Check1=true; [fired_Check1] /
ReplyCheck2 [fired_Check2] / send Check2 to Service4;
fired_Check2=true;
Ack1 /
/send Answer to Service1;
Fig. 14. State machine of Service2
T. Miyamoto, Y. Hasegawa: Synthesize Intelligible State Machine Models 235
Check2 / Check3 /
Info1 /
/Service6.Check5();
/send Info1 to Service4;
/ send ReplyCheck2 to Service2;
Fig. 16. State machine of Service5
Fig. 15. State machine of Service4
Table 1. Evaluation result
Method in [2] Method in [8] CSCB
NSS NT NG NSS NT NG NSS NT NG
Service1 5 7 0 5 9 0 2 3 0
Service2 31 59 0 31 59 0 9 17 2
Service3 5 7 0 5 9 0 5 9 0
Service4 8 11 0 7 11 0 6 10 0
Service5 3 4 0 3 4 0 3 4 0
Service6 5 7 0 5 9 0 5 9 0
is evaluated by comparing with Bultan’s method[2], the state space generation
method[8] by using the above metric.
The Bultan’s method[2] synthesize flat state machines from the dependency
relation. Suppose the number of events relating to object c to be |Σ c |, then the
c
number of states of the state machine becomes 2|Σ | . This method, however,
generates plenty of unreachable state from the initial state. In this paper, state
machines after removing these unreachable states are used.
The state space generation method[8] generates a state space for each MMG
at first, and then converts the state spaces into state machines. The method, how-
ever, tries to find “independent sequences” in the state space, and tries to reduce
the number of states by using composite states. Therefore, when no independent
sequence is found, the same result with the Bultan’s method is obtained.
Table 1 shows values of the metrics of state machines which are obtained
from the communication diagram in Fig. 1. Note that in the Bultan’s method
and the state space generation method, the reply message to a synchronous
call is considered as an asynchronous message which is independent with the
synchronous call. On the other hand, in the proposed method, the state transition
relating to a synchronous call terminates only when it receives the reply message.
The proposed method adds relation at step2 so as each preparation event for
message sending has only the receive event of the reply message as an immediate
successor. Therefore, in the dependency relation for Service1, events ?Req1_rep
236 PNSE’12 – Petri Nets and Software Engineering
and ?Answer are in concurrent for the Bultan’s method and the state space
generation method, but they are in sequential for the CSCB method.
As for Service2, since the state space generation method failed to find inde-
pendent sequences, the state space are converted into a state machine as is. In
contrast, the proposed method succeeds to significantly reduce the number of
states by cutting bridges.
4 Conclusion
In this paper, we considered the approach to the choreography realization prob-
lem considering intelligibility of synthesized state machines. We proposed a
method to synthesize state machines without generating state spaces from the
choreography defined by single communication diagram. We evaluated the pro-
posed method by using metrics about intelligibility of the generate state ma-
chines.
References
1. Antonio Cruz-Lemus, J., Genero, M., Piattini, M.: Metrics for UML Statechart
Diagrams. In: Genero, M., Piattini, M., Calero, C. (eds.) Metrics for Software
Conceptual Models, pp. 237–272. Imperial College Press, London (2005)
2. Bultan, T., Fu, X.: Specification of realizable service conversations using collabo-
ration diagrams. Service Oriented Computing and Applications 2(1), 27–39 (2008)
3. Desel, J., Yakovlev, A. (eds.): Proceedings of 2nd Workshop on Application of
Region Theory (Jun 2011)
4. Esparza, J., Silva, M.: Circuits, Handles, Bridges and Nets. Lecture Notes in Com-
puter Science 483, 209–242 (1991)
5. Harel, D., Kugler, H., Pnueli, A.: Synthesis revisited: generating statechart mod-
els from scenario-based requirements. In: Kreowski, H.J., Montanari, U., Orejas,
F., Rozenberg, G., Taentzer, G. (eds.) Formal Methods in Software and Systems
Modeling, pp. 309–324. Springer (Jan 2005)
6. Jungnickel, D.: Graphs, Networks and Algorithms. Springer, 3rd edn. (2007)
7. Liang, H., Dingel, J., Diskin, Z.: A Comparative Survey of Scenario-based to State-
based Model Synthesis Approaches. In: 2006 International workshop on Scenarios
and state machines: models, algorithms, and tools. pp. 5–11 (2006)
8. Miyamoto, T., Kurahata, H., Fujii, T., Hosokawa, R.: Synthesis of state machine
diagrams from communication diagrams using petri nets. Innovations in Systems
and Software Engineering 6, 39–46 (2010)
9. Murata, T.: Petri nets: Properties, analysis and applications. Proc. IEEE 77(4),
541–580 (Apr 1989)
10. OMG: Unified modeling language, http://www.uml.org/
11. Su, J., Bultan, T., Fu, X., Zhao, X.: Towards a theory of web service choreographies.
In: Proceedings of the 4th international conference on Web services and formal
methods. pp. 1–16 (2008)
12. Thomas, E.: Service-Oriented Architecture. Prentice Hall (2004)
13. Whittle, J., Jayaraman, P.K.: Synthesizing hierarchical state machines from ex-
pressive scenario descriptions. ACM Transactions on Software Engineering and
Methodology 19(3), 1–45 (Jan 2010)