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 synthesize 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 problem. The proposed method is evaluated using a metric for intelligibility.
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)[
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 synthesize 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
synthesize the concrete model from the abstract specification. Harel et al. proposes
a methodology for synthesizing statechart models from scenario-based
requirements[
In SOA, the problem to synthesize the concrete model from an abstract
specification is known as the choreography realization problem[
Bultan and Fu formally introduced the choreography realization problem in
[
Miyamoto et al. have proposed a method to synthesize hierarchical state
machines from the choreography given in communication diagrams[
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.
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 messages generated by asynchronous calls, and Mrep is the set of reply messages to synchronous messages. Let Ms = Msop and Ma = Maop ∪ Mrep. Correspondence between the synchronous call and its response is given by the function 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.
Service1 Answer
Service2
Req1
Check2 ReplyCheck2 Check3
Service4 Service5
Info1 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 σ = m1m2 · · · 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.
σ = Req1 Check1 Req1_rep Check2 Check3 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 region, 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 pseudostates 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 conts1m(·) = contsm(·) and contism(·) = contsm(contis−m1(·)) (i > 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[
Due to space limitations, the details of operational semantics of state machines 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.
/!m ?m /!m
?m s11 s12 sm1 /!m s21 s22 sm2
?m rm s11 s12 sm1 s21 s23 sm2 !m !rm s11 s12 sm1 s21 s23 sm2 !m !rm s11 s12 sm1 s11 s12 sm1 s21 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 sendreceive 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).
The proposed method represents the dependency relation between message send
an receive events by using Petri nets[
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•.
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 Tfork, 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 an event for the transition.
A : T 7→ Σ assigns
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 nonnegative integers and B = {true, false}. The initial state (M0, X0) of MMG is given as follows:
M0(p) = (1 if p = ps
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, X0) obtained by the firing of transition t is given as follows:
X0(t0) = (true
if t0 = t
X(t0) otherwise.
M 0(p) = M (p) − W (p, t) + W (t, p), and 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, J F (t) ⊆ T is a set of starting vertices of handles
terminating at t. Please refer to [
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. |Tfork| = |Tjoin| 2. Tfork ∩ Tjoin = ∅ 3. For any pair of handles H, H0 in the MMG, only one of following conditions holds: (a) H and H0 share the same starting vertex and the same terminal vertex, and (b) the starting vertices of H and H0 are different and the terminal vertices of H and H0 are different. 4. If A(t) = $m, then t • • = {t0}, A(t0) =?ref er(m).
From the definition of CMMG, for all t ∈ Tfork (resp. t ∈ Tjoin) |F J (t)| = 1 (resp. |J F (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(· · · ) Behavior(t) = if A(t) ∈ {$m | m ∈ Msop} 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 expressions show a synchronous call, an asynchronous call, and a reply for a synchronous 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. 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. 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 2 A ← {f iredt | t ∈ St0∈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); while t 6= te do ev ← Event(t); const ← Constraint(t); beh ← Behavior(t); if ev = const = beh = ε ∧ |t • | = 1 then
t ← t • •; continue; if A(t) ∈ {$m | m ∈ Ms} then t ← t • •; if |t • | ≥ 2 then s0 ← new CompositeState(); cont(s0) ← r; forall the p0 ∈ t• do r0 ← new Region(); cont(r0) ← s;
RN G(p0•, r0, F J (t)); t ← F J (t) ; else s0 ← new SimpleState(); cont(s0) ← r; t ← t • •; new Transition (s, ev, const, beh, s0); s ← s0; f s ← new FinalState(); 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.
Service6-init !Check5 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 [
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 Tfork and Tjoin in the MMG. 7. Perform Algorithm 1. !Req1_rep !Check1 !Check3 ?Req1_rep !Check2 ?Check1 Construction of dependency relation ⇒cd The dependency relation ⇒cd⊆ Σcd × Σcd on the set of events is given by the following expression: cd cd ⇒cd=Dcd ∪ {($m, !m) | m ∈ Ms } ∪ {(!m, ?m) | m ∈ Ma } ∪ {(?m1, !m2) | m1 ∈ Mcad, m2 ∈ Mcad, (!m1, !m2) ∈ Dcd} ∪ {(?m1, $m2) | m1 ∈ Mcad, m2 ∈ Mcsd, (!m1, !m2) ∈ Dcd} ∪ {(!m1, $m2) | m1 ∈ Mcsd, m2 ∈ Mcsd, (!m1, !m2) ∈ Dcd}
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 relation ⇒cd shown in Fig. 7, are shown in Fig. 8. Here, since ($Req1, ?Req1rep),
A B (D) C
Fig. 10. Finding one-to-one correspondence ($Req1, ?Answer) ∈⇒ccd for Service1, a relation (?Req1rep, ?Answer) is added
Service1. in ⇒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.
G(t) = (!Check1 if A(t) = !Check2
!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[
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.
Conversion into state machines By performing Algorithm 1, state machines
shown in Fig.s 12, 14, 13, 15, 16, and 6 are obtained.
Service1-init
$Req1
Antonio et al. have experimentally evaluated the relationship between metrics
and intelligibility of the state machines by measuring time to understand state
machines[
Req1 / /send Check1 to Service3; fired_Check1=true; Ack1 / /send Check3 to Service5; ReplyCheck2 [fired_Check2] / /send Answer to Service1; [fired_Check1] / send Check2 to Service4; fired_Check2=true;
Fig. 14. State machine of Service2
Check2 / /Service6.Check5();
Info1 / / send ReplyCheck2 to Service2;
Check3 / /send Info1 to Service4;
Fig. 16. State machine of Service5
is evaluated by comparing with Bultan’s method[
The Bultan’s method[
The state space generation method[
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 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 independent 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
In this paper, we considered the approach to the choreography realization problem 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 proposed method by using metrics about intelligibility of the generate state machines.