# Service-Oriented Synthesis of Distributed and Concurrent Protocol Specifications

Authors: Jehad Al Dallal; Kassem Saleh
Journal: Journal of Computer Systems, Networks, and Communications
 (2008)

---

## Abstract

Several methods have been proposed for synthesizing computer communication protocol specifications from service specifications. Some protocol synthesis methods based on the finite state machine (FSM) model assume that primitives in the service specifications cannot be executed simultaneously. Others either handle only controlled primitive concurrency or have tight restrictions on the applicable FSM topologies. As a result, these synthesis methods are not applicable to an interesting variety of inherently concurrent applications, such as the Internet and mobile communication systems. This paper proposes a concurrent-based protocol synthesis method that eliminates the restrictions imposed by the earlier methods. The proposed method uses a synthesis method to obtain a sequential protocol specification (P-SPEC) from a given service specification (S-SPEC). The resulting P-SPEC is then remodeled to consider the concurrency behavior specified in the S-SPEC, while guaranteeing that P-SPEC provides the specified service.


---

## Body

## 1. Introduction

A protocol can  be defined as an
agreement for the orderly and timely exchange of messages among communicating
entities. A full protocol description comprises a precise format for valid
messages (syntax), rules for the orderly message exchanges (grammar), and vocabulary of valid messages that can be exchanged with their clear meaning
(semantics).In protocol design, interacting entities
are constructed to provide a set of specified services for distributed service
users. While designing a communication protocol, semantic and syntactic errors
may exist. Semantic design errors cause incorrect services to be provided to
distributed service users. Syntactic design errors can cause the protocol to
deadlock. There are three common types of syntactic design error, including (1) an unspecified reception error, when the protocol reaches a state where it
is not able to handle the message that may arrive; (2) a deadlock error, when
the protocol is at a nonfinal state, all channels are empty, and no transmission
transition is specified; (3) a livelock error, when the protocol entities are locked
in a loop exchanging messages that are not contributing to the provision of the
desired service.A communication system is most
conveniently structured in layers. The service access point (SAP) is an interaction
point through which a layer can communicate with the upper layer or service
users, or with the lower layer. A layer can service several SAPs. The
communication is performed using service primitives (SPs). The SP identifies
the type of the message and the SAP at which it occurs.From the user’s viewpoint,  at a high
level of abstraction, the layer can be viewed as a black box where only interactions with
the user, identified by SPs, are observable. The specification of the service
provided by the layer is defined by the ordering of the visible SPs and is
called service specification (S-SPEC). At a refined and lower level of
abstraction, the service provided by the layer is performed using a number of
cooperating protocol entities. The number of protocol entities is equal to the
number of SAPs available at the layer. In a distributed system, the protocol
entities are geographically distributed and exchange protocol messages through
a communication medium. The protocol specification (P-SPEC) consists of the
specification of each of the protocol entities, each describing the
interactions needed to deliver the specified service. Figure1 shows the two levels
of abstraction of a communication service. Both S-SPEC and P-SPEC can be
modeled using finite state machines (FSMs).A communication system at two levels of abstractions.
(a)
Communication service(b)
Communication protocolIn autonomous communication systems such
as the Internet and mobile communication systems, a user can initiate a service
at any time. As a result, distributed users at different SAPs may issue
simultaneous service requests; consequently, it is possible that two or more
users will simultaneously issue service requests to each other. This situation leads
to message collision. If the protocol specification is not properly designed to
deal with this situation, an unspecified reception error may occur.For example, mobile games use WiFi and Bluetooth
technologies [1]. In such games, distributed players use different
machines to play with each other simultaneously and communicate over wireless
networks. If the communication protocol providing this game service is improperly
designed, the game will be blocked indefinitely or will function improperly.Concurrent clients and servers can
communicate over the Internet using TCP/IP standard or nonstandard protocols
[2]. For example, a concurrent client for the TIME service
can send requests to multiple servers one at a time and receive responses in an
arbitrary order. An unspecified reception error may occur or a deadlock may be
reached in the client if its protocol is not designed properly.Protocol specifications
are more complex to specify than service specifications because of their
refined nature. Therefore, in a top-down design approach, it is quite natural
to start the protocol design process from a complete and unambiguous service
specification. The construction or derivation of a protocol specification from
a given service specification is calledprotocol synthesis. Instead of
applying a sequence of design, analysis, error detection, and correction
iteratively until the design is error-free, the protocol synthesis approach
does not require any further validation of the synthesized protocol specification.
The correctness of the synthesized protocol must be guaranteed as a direct
by-product of the synthesis method [3]. The synthesis
approach is used to construct or complete a partially specified protocol
design, such that the interactions between the constructed or completed
protocol entities proceed without encountering any logical error while
providing the specified service. Several protocol synthesis methods have
appeared in the literature [4–16]. The methods introduced  by Saleh and Probert [4], Higashino et al.
[7],  Yamaguchi et al. [8], Bista et al. [11], Maneerat et al. [12], Yamaguchi
et al. [13], Maneerat et al. [14], Dallal [15], and Stakhanova et al.
[16] are either not based on the FSM model or support only sequential
applications. The method introduced by Saleh and Probert [9] supports only
controlled nonsequential applications. The methods introduced by Khoumsi
[5], Park and Miller [6], and Kakuda et al. [10] support nonsequential
applications that have restrictions on the service specification model topology
or on the allowed ordering of service primitives in the service specification.This paper introduces a method for the
synthesis of protocol specifications that do not necessarily start from
sequential service specifications. The synthesis method extends the synthesis
method introduced in Saleh and Probert [4] to derive the sequential P-SPEC.
The synthesis method then remodels the sequential P-SPEC to consider the
concurrency behavior specified in the S-SPEC. The synthesis method supports
uncontrolled concurrent applications and is free of the restrictions imposed on
service specification by the earlier methods. The synthesis method introduced
uses FSMs for modeling both service and protocol specifications. This paper
does not address the multithreading problem in which an application with
different threads runs within one or more processors. Instead, it addresses the
more complex problem of concurrency in which an application consists of distributed
protocol entities that are running concurrently in geographically distributed
processors.The paper is organized as follows. Related
research is overviewed in Section2. In Section 3, the models used for the
service and protocol specifications are defined. In Section 4, the concurrent
protocol synthesis method is introduced. Finally, Section 5 concludes the paper
and discusses possible extensions in future work.


## 2. Related Research

Two approaches are used in
designing communication protocols: analysis and synthesis. In the analysis
approach, a sequence of design, analysis, error detection, and correction is
applied iteratively to produce error-free design. In the synthesis approach,
the protocol design is constructed or completed in such a way that no further
validation is needed. Some protocol synthesis methods start the derivation
process from a complete service specification [4–10, 12, 13, 14, 15] and others do not [17, 18]. The protocol synthesis methods can be further classified according to
the models used, which include finite state machines [4, 6, 7, 9, 10, 15], Petri nets [8, 13], and LOTOS-like [5, 12, 14].Some of the FSM-model-based
service-oriented protocol synthesis methods consider the concurrency behavior
of the protocol entities, including Park and Miller [6], Saleh and Probert
[9], and Kakuda et al. [10]. In Park and Miller [6], a concurrent
timed protocol synthesis method is introduced, with three restrictions. The
first restriction is that the S-SPEC model is assumed to be cyclic. The second
restriction is that if a path p includes a transition associated with an
event that passes through a SAP s, any other path executed in parallel
with p cannot include a transition associated with an event that passes
through the same SAP s. As a result, the main concurrency problem,
message collision, is not resolved. The last restriction is that all the
outgoing transitions from a choice state have to be associated with events that
pass through the same SAP.Kakuda et al. [10] introduced a concurrent
protocol synthesis method, with two restrictions. The first restriction is that
the S-SPEC model must be a tree. The second is that if a collision occurs
between two protocol entities, the parallel path that has the higher priority
proceeds and the events that have not been executed in the other path yet are
cancelled. This is called controlled concurrency. In controlled concurrency, if
a message collision occurs, the problem is not solved by handling the collision
in such a way that all parallel paths proceed without canceling some or all of
their events.Finally, in Saleh
and Probert [9], a concurrent protocol synthesis method is introduced. The
synthesis method extends the sequentially based synthesis method introduced earlier
by them in Saleh and Probert [4]. After applying the three steps of their
original method, the extended method added transitions to solve the controlled concurrency
problem. If a message collision occurs, either all parallel paths have to be
re-executed or the parallel path that has the highest priority proceeds and the
events not yet executed in the other paths are cancelled. This solution is not
practical because it results in canceling or re-executing some events.In this paper, the introduced synthesis
method solves the true concurrency problem. In our method, if a message
collision occurs, all parallel paths proceed without canceling or re-executing
any event. In addition, our method eliminates all the restrictions imposed by
the methods introduced in Park and Miller [6] and Saleh and Probert [9],
and therefore is applicable to a wider range of applications.


## 3. Model Definition

Both the service and protocol
specifications are modeled using FSM-based models. A FSM consists of a finite
number of states and transitions. It is only suitable for modeling the sequential
behavior of systems. The work we are developing here addresses the synthesis of
protocol specifications from a service specification exhibiting concurrent
behaviors. Therefore, in this section, the FSM is extended to model the
concurrent behaviors in the service specification. The extended model is called
the extended finite state machine (EFSM). Each protocol entity is a
sequentially based subsystem, and therefore, a traditional FSM can be used
without extension to model the protocol entities. In this section, the models
used are formally defined in the context of the layered communication system
introduced in Section1.


### 3.1. Service Specification Model

The service specification described in
the EFSM defines sequences of primitives exchanged between users and processes
through the service access points at both upper and lower layers. A service
specification specifies a concurrent behavior if two or more service primitives
pass through different SAPs simultaneously.Definition 1.
A service
specification S-SPEC is modeled by an EFSM denoted by a tuple (Ss,Ts,σ), where
(1)
Ss is a nonempty finite set of service
states. Each state s∈Ss is
a choice, fork, joint, or leaf state. A choice state is a state that has one or
more outgoing transitions and only one transition is executed. A fork state,
denoted by ∥, is a state that has two or more outgoing transitions associated
with service primitives that pass through different SAPs, and all these outgoing
transitions are executed simultaneously. A joint state is a state that has two
or more incoming transitions and one or more outgoing transitions. A state
could be both a fork state and a joint state. Finally, a leaf state is a terminal
sink state that does not have any outgoing transitions. As in Park and Miller
[6], we assume in our work that there exists a unique joint state for each
fork state, and vice versa;(2)
Ts is a finite set of transitions, such that
each transition t∈Ts is
a 3-tuple 〈tail(t), head(t), SP〉, where tail(t) and head(t) are, respectively, the tail and the head states of t,
and SP is the service primitive that defines the service event, its
type, and the index of the SAP, denoted by SAP(SP),  at which the SP is observed. There are
two types of service primitive directions. An SP of type↑ is
directed upward from the protocol entity to the upper SAP (U-SAP) and directed
to the service user at the upper layer. An SP of type↓ is
directed downward from the service user at the U-SAP and directed to a protocol
entity. All service primitives in the S-SPEC involve the U-SAP only;(3)
σ∈Ss is the initial service state.
A pathp in the ESFM is specified
by the sequence of states (si,sj,…,sk)
traversed by a set of successive transitions, where sj=successive(si)p.
The key difference between the EFSM and the traditional FSM is the presence of
the fork state. Parallel paths are specified by the sequence (si,sj,…,sk), where si is a fork state
and sk is either a joint or leaf state.
Figure2 shows a service specification S-SPEC.
This example demonstrates a simple data transfer application, consisting of three
entities: a server and two machines available at three SAPs. The service
described in the S-SPEC is a server-controlled transfer of data between two
machines. The server and the two machines are processing concurrently. The
service is initiated by the server user by issuing a Next SP downward to
the sever machine. This service request results in two concurrent upward
requests Next SP at SAP2 and SAP3. The user at SAP2 issues a downward Data SP. Similarly, the user at SAP3 issues
a downward Data SP. The downward Data SP at SAP2 will
result in an upward Data SP at SAP3 and similarly, the
downward Data SP at SAP3 will result in an upward Data SP at SAP2. Then, the service cycles back after receiving Next SP downward from the server user. In this example, if one or both machines have
nothing to exchange, they send NULL data message. In this example, Ss={s1,s2,s3,s4,s5,s6,s7}, Ts={〈s1,s2,↓Next1〉,〈s2,s3,↑Next3〉,〈s3,s4,↓Data3〉,〈s4,s7,↑Data2〉,〈s2,s5,↑Next2〉,〈s5,s6,↓Data2〉,〈s6,s7,↑Data3〉,〈s7,s2,↓Next1〉}, and σ={s1}.
For the transition t=〈s1,s2,↓Next1〉, the states s1 and s2 are, respectively, the tail and head states of t, and the
SP is ↓Next1.
For the SP, the event is Next, SAP(SP)=1, and the type is ↓. States s1, s3, s4,
s5, and s6 are choice states and states s2 and
s7 are fork and joint states, respectively. Paths (s2, s3, s4, s7)
and (s2, s5, s6, s7) are parallel
paths.Figure 2
A service specification example.


### 3.2. Protocol Specification Model

The protocol specification consists of
the specifications of the protocol entities that cooperate to provide the
service described in the service specification.Definition 2.
The protocol entity
specification PE-SPECi is modeled by a FSM denoted by a tuple (Spi,Tpi,σpi),
where
(1)
Spi is a nonempty finite set of states of
protocol entity i. Each state spi∈Spi is an image of one or more S-SPEC states. A state spi can be an
image of more than one S-SPEC state if two or more S-SPEC states are combined
during the protocol synthesis process. A path pp in the
PE-SPECi is an image of path ps in the S-SPEC if
each state in pp is an image of one or more states in ps,
and each state in ps is a preimage of a state in pp.
A parallel path in PE-SPEC is an image of a parallel path in S-SPEC. Each state
can be either a sending or a receiving state. A sending state is a source state
of a transition associated with an SP. A receiving state is a source state of
transitions such that all of them are associated with receiving events;(2)
Tpi is a finite set of transitions such that
each transition t∈Tpi is
a 3-tuple 〈tail(t), head(t), Ei〉, where tail(t) and head(t) are, respectively, the tail and the head states of t,
and Ei is a protocol event that can be either: (1) an SP that
passes through SAPi, (2) an SP that passes through SAPi and an event message E sent to PEj denoted by !ej,
or (3) an event message E received from PEj denoted by ?ej.
An event of the second type is denoted by E/!ej;(3)
σpi∈Spi is the initial protocol state.
Figure3 shows the three PE-SPECs synthesized
from S-SPEC in Figure 2. For PE-SPEC1, Spi={s1,s2,s7}, Tpi={〈s1,s2,Next/!next2,3〉,〈s2,s7,?data2〉,〈s2,s7,?data3〉,〈s7,s2,Next/!next2,3〉},
and σpi={s1}.
States s1 and s7 are, respectively, the images of states
s1 and s7 in the S-SPEC shown in Figure 2. State s2 is the image of the states s2, s3, s4, s5,
and s6 in the S-SPEC. As a result, the path (s2, s7)
in PE-SPEC1 is the image of path (s2, s3, s4, s7)
in S-SPEC, and it is therefore a parallel path because it is an image of a
parallel path in S-SPEC. Finally, states s1 and s7 are
sending states, and state s2 is a receiving state.Figure 3
The PE-SPECs synthesized from the S-SPEC given in Figure2.In this paper, we assume that the
communication medium between the protocol entities is reliable, and the
messages are delivered in a first-in-first-out (FIFO) order.


## 3.1. Service Specification Model

The service specification described in
the EFSM defines sequences of primitives exchanged between users and processes
through the service access points at both upper and lower layers. A service
specification specifies a concurrent behavior if two or more service primitives
pass through different SAPs simultaneously.Definition 1.
A service
specification S-SPEC is modeled by an EFSM denoted by a tuple (Ss,Ts,σ), where
(1)
Ss is a nonempty finite set of service
states. Each state s∈Ss is
a choice, fork, joint, or leaf state. A choice state is a state that has one or
more outgoing transitions and only one transition is executed. A fork state,
denoted by ∥, is a state that has two or more outgoing transitions associated
with service primitives that pass through different SAPs, and all these outgoing
transitions are executed simultaneously. A joint state is a state that has two
or more incoming transitions and one or more outgoing transitions. A state
could be both a fork state and a joint state. Finally, a leaf state is a terminal
sink state that does not have any outgoing transitions. As in Park and Miller
[6], we assume in our work that there exists a unique joint state for each
fork state, and vice versa;(2)
Ts is a finite set of transitions, such that
each transition t∈Ts is
a 3-tuple 〈tail(t), head(t), SP〉, where tail(t) and head(t) are, respectively, the tail and the head states of t,
and SP is the service primitive that defines the service event, its
type, and the index of the SAP, denoted by SAP(SP),  at which the SP is observed. There are
two types of service primitive directions. An SP of type↑ is
directed upward from the protocol entity to the upper SAP (U-SAP) and directed
to the service user at the upper layer. An SP of type↓ is
directed downward from the service user at the U-SAP and directed to a protocol
entity. All service primitives in the S-SPEC involve the U-SAP only;(3)
σ∈Ss is the initial service state.
A pathp in the ESFM is specified
by the sequence of states (si,sj,…,sk)
traversed by a set of successive transitions, where sj=successive(si)p.
The key difference between the EFSM and the traditional FSM is the presence of
the fork state. Parallel paths are specified by the sequence (si,sj,…,sk), where si is a fork state
and sk is either a joint or leaf state.
Figure2 shows a service specification S-SPEC.
This example demonstrates a simple data transfer application, consisting of three
entities: a server and two machines available at three SAPs. The service
described in the S-SPEC is a server-controlled transfer of data between two
machines. The server and the two machines are processing concurrently. The
service is initiated by the server user by issuing a Next SP downward to
the sever machine. This service request results in two concurrent upward
requests Next SP at SAP2 and SAP3. The user at SAP2 issues a downward Data SP. Similarly, the user at SAP3 issues
a downward Data SP. The downward Data SP at SAP2 will
result in an upward Data SP at SAP3 and similarly, the
downward Data SP at SAP3 will result in an upward Data SP at SAP2. Then, the service cycles back after receiving Next SP downward from the server user. In this example, if one or both machines have
nothing to exchange, they send NULL data message. In this example, Ss={s1,s2,s3,s4,s5,s6,s7}, Ts={〈s1,s2,↓Next1〉,〈s2,s3,↑Next3〉,〈s3,s4,↓Data3〉,〈s4,s7,↑Data2〉,〈s2,s5,↑Next2〉,〈s5,s6,↓Data2〉,〈s6,s7,↑Data3〉,〈s7,s2,↓Next1〉}, and σ={s1}.
For the transition t=〈s1,s2,↓Next1〉, the states s1 and s2 are, respectively, the tail and head states of t, and the
SP is ↓Next1.
For the SP, the event is Next, SAP(SP)=1, and the type is ↓. States s1, s3, s4,
s5, and s6 are choice states and states s2 and
s7 are fork and joint states, respectively. Paths (s2, s3, s4, s7)
and (s2, s5, s6, s7) are parallel
paths.Figure 2
A service specification example.


## 3.2. Protocol Specification Model

The protocol specification consists of
the specifications of the protocol entities that cooperate to provide the
service described in the service specification.Definition 2.
The protocol entity
specification PE-SPECi is modeled by a FSM denoted by a tuple (Spi,Tpi,σpi),
where
(1)
Spi is a nonempty finite set of states of
protocol entity i. Each state spi∈Spi is an image of one or more S-SPEC states. A state spi can be an
image of more than one S-SPEC state if two or more S-SPEC states are combined
during the protocol synthesis process. A path pp in the
PE-SPECi is an image of path ps in the S-SPEC if
each state in pp is an image of one or more states in ps,
and each state in ps is a preimage of a state in pp.
A parallel path in PE-SPEC is an image of a parallel path in S-SPEC. Each state
can be either a sending or a receiving state. A sending state is a source state
of a transition associated with an SP. A receiving state is a source state of
transitions such that all of them are associated with receiving events;(2)
Tpi is a finite set of transitions such that
each transition t∈Tpi is
a 3-tuple 〈tail(t), head(t), Ei〉, where tail(t) and head(t) are, respectively, the tail and the head states of t,
and Ei is a protocol event that can be either: (1) an SP that
passes through SAPi, (2) an SP that passes through SAPi and an event message E sent to PEj denoted by !ej,
or (3) an event message E received from PEj denoted by ?ej.
An event of the second type is denoted by E/!ej;(3)
σpi∈Spi is the initial protocol state.
Figure3 shows the three PE-SPECs synthesized
from S-SPEC in Figure 2. For PE-SPEC1, Spi={s1,s2,s7}, Tpi={〈s1,s2,Next/!next2,3〉,〈s2,s7,?data2〉,〈s2,s7,?data3〉,〈s7,s2,Next/!next2,3〉},
and σpi={s1}.
States s1 and s7 are, respectively, the images of states
s1 and s7 in the S-SPEC shown in Figure 2. State s2 is the image of the states s2, s3, s4, s5,
and s6 in the S-SPEC. As a result, the path (s2, s7)
in PE-SPEC1 is the image of path (s2, s3, s4, s7)
in S-SPEC, and it is therefore a parallel path because it is an image of a
parallel path in S-SPEC. Finally, states s1 and s7 are
sending states, and state s2 is a receiving state.Figure 3
The PE-SPECs synthesized from the S-SPEC given in Figure2.In this paper, we assume that the
communication medium between the protocol entities is reliable, and the
messages are delivered in a first-in-first-out (FIFO) order.


## 4. Synthesizing Concurrent Protocol Specifications

The synthesis of concurrent protocol specifications method
introduced in this paper extends a sequentially based synthesis method
introduced by Saleh and Probert [4]. In their method, three steps are
applied to obtain the PE-SPECs. In the first step, projected service
specifications are derived by projecting the S-SPEC onto each SAP. In the
second step, a set of transition synthesis rules are applied to the transitions
of the projected service specifications to obtain the sequentially based
PE-SPECs. In the third step, the PE-SPECs are optimized to obtain the final
PE-SPECs as shown in Figure 3. When the S-SPEC includes concurrent behaviors,
the PE-SPECs obtained may cause an unspecified reception error. For instance,
the S-SPEC given in Figure 2 shows that the transitions outgoing from state s2 is executed simultaneously. When the PE-SPECs function concurrently, the
transitions associated to event Next in both PE-SPEC2 and
PE-SPEC3 execute simultaneously. After that, the transition
associated to event ↓Data/!data3 in PE-SPEC2 is executed
causing an unspecified reception error to occur in PE-SPEC3.
Similarly, the transition associated to event ↓Data/!data2 in
PE-SPEC3 is executed causing an unspecified reception error to occur
in PE-SPEC2.In our extension, more states and
transitions are added to the derived protocol entities to handle the
concurrency behaviors. The synthesis algorithm, the additional transition
synthesis rules, and the conditions for applying the transition synthesis rules
are illustrated below. The syntactic and semantic correctness of our extended synthesis
method are provided in Appendix.


### 4.1. The Synthesis Algorithm

Starting from a service specification
modeled in EFSM, the algorithm outlined in Algorithm1 automatically derives the
concurrent protocol entities that provide the set of services given in the
S-SPEC. In the first step, the sequential protocol entities are derived using
Saleh and Probert [4] synthesis method. In the second step, using the
algorithm outlined in Algorithm 2, the protocol entities are remodeled to consider
their concurrent execution.


### 4.2. Additional Transition Rules

To obtain the concurrent PE-SPECs from
the sequential ones, the procedure shown in Algorithm2 is applied. According to
this procedure, only the parallel paths are remodeled. First the parallel paths
are partitioned according to the type of events associated to the first
transition in each path. Then, the paths in each partition are remodeled
according to the type of the image of the fork state (i.e., sending or
receiving state).Step 1: partitioning parallel paths
In the protocol entities, the image of
the fork state can have one or more outgoing transitions. In the case where
there is only one outgoing transition, no message collision can occur. Hence,
no modification is required. In the case where there is more than one outgoing
transition from a states, which is an image of a fork state, the
outgoing paths from state s are partitioned into two groups according to
the type of the event associated to the first transition in each path. There are
two possible types of such events: a service primitive or an event reception.
Paths in which the first transition is associated to a service primitive are
placed in the first group and the others are placed in the second group.
Paths in the first group are initiated
by the protocol entity under consideration. On the other hand, the paths in the
second group are not initiated until the protocol entity has received the
required event. When the protocol entity can execute more than one path in the
first group, it has to select one of them. Once the first transition of a
parallel path in the first group has been executed, the parallel path is
selected and the other parallel paths in the same group are disabled. However,
this case is different for the parallel paths in the second group. To
summarize, when an image of a fork state in a protocol entity is reached, one
of the paths—if there are any—in the first
group is executed along with all paths in the second group. The first two steps
of the procedure given in Algorithm3 illustrate how to partition the parallel
paths.Before the parallel paths are remodeled,
one more refinement action is required for the paths in the second group. Each
path in the second group is divided into subpaths. Each subpath starts with a
transition associated with a receiving event and contains only one such
transition. The use of these subpaths is illustrated below. The third step of
the procedure given in Algorithm3 shows how to divide the paths in the second
group into subpaths.For example, in PE-SPEC1 given in Figure 3, state s2 is an image of a fork state and has more
than one outgoing transition; therefore, the outgoing parallel paths from state
s2 are partitioned into two groups: G1 and G2.
The first group is empty because none of the outgoing transitions from state s2 is associated with a service primitive. Figure 4(a) shows the content of the
second group. The subpaths of the parallel paths given in Figure 4(a) are the
same as the parallel paths because each of the parallel paths contains only one
transition. For PE-SPEC2 given in Figure 3, the outgoing parallel
paths from state s2 are partitioned into two groups. The first and
second groups, G1 and G2, include the paths that start
with a transition associated with a service primitive and a receiving event,
respectively. Figure 4(b) shows the contents of both groups. The subpaths of
the parallel path contained in G2 are the same as the parallel path,
because the parallel path contains only a transition associated with a
receiving event, followed by a transition associated with a service primitive.Application of partitioning procedure on the PE-SPECs given in Figure3.
(a)
G2 for PE-SPEC1(b)
G1 and G2 for PE-SPEC2Step 2.1: remodeling parallel paths starting at a sending image of a fork state
In a PE-SPEC that has a sending image of a fork state, the
first group of the parallel paths is not empty. As discussed earlier, one of
the parallel paths in the first group can be executed along with all the parallel
paths in the second group. This means that at any state for a path in the first
group, any subpath of any parallel path in the second group has to be allowed
to execute, or an unspecified reception error can occur. This can be modeled by
making each state in the first group a source state for the first transition in
each subpath of each path in the second group.
This solution solves the unspecified
reception error problem until the protocol entities reach the image of the
joint state. When any of the protocol entities reach the image of the joint
state, they have to wait for the other protocol entities to reach their images
of the joint state, or an unspecified reception error can occur because of the
divergence between the protocol entities. According to the solution for the
unspecified reception error discussed above, the protocol entity can either
leave the image of the joint state by executing the outgoing transition from
the image of the joint state or execute one of the subpaths added to the image
of the joint state. An unspecified reception error can occur if the protocol
entity executes the outgoing transition from the joint state without executing
the other added transitions. Therefore, it is important to ensure that none of
the protocol entities leaves the image of the joint state unless all other
protocol entities have reached their corresponding state. In other words, it
must be ensured that none of the protocol entities leaves the image of the
joint state unless the last subpath of each parallel path has been executed.
This can be modeled by (1) adding copies of the parallel paths in the first
group, (2) connecting these copies using the last subpaths of the paths in the
second group, and (3) redirecting the outgoing transition from the image of the
joint state to be initiated from the state reached by executing all the last
subpaths under consideration. Note that if the image of the joint state is a
source state for a transition associated to a receiving event, the image of the
joint state cannot be left unless the event message is sent by some other
protocol entity. Therefore, the solution illustrated above has to be applied
only in a protocol entity where the image of the joint state is a source state
of a transition associated to a service primitive.The solutions for the unspecified
reception problem and the divergence problem discussed above are given formally
in the procedure shown in Algorithm4. For PE-SPEC2 given in Figure 3, the
procedure given in Algorithm 4 is applied because s2 is a sending
state. Step 1 of the procedure is not applicable because joint state s7 is not a sending state. In Step 2, copies of the subpath of G2 are
added to each state contained in G1, as shown in Figure 5(a). Step 3
is not applicable because Step 1 is not applicable. Step 4 is not applicable
because there are no redundant transitions connected to the images of the fork
and joint states. Finally, in Step 5, the path contained in G2 is
removed from PE-SPEC2. The resulting PE-SPEC2 is shown in
Figure 5(b). PE-SPEC3 and PE-SPEC2 given in Figure 3 are
similar to each other; therefore, the same synthesis steps apply. The resulting
PE-SPEC3 is shown in Figure 5(c).An application of the procedure given in Algorithm4 for the PE-SPEC2 and PE-SPEC3 given in Figure 3.
(a)
PE-SPEC2: Step 2(b)
PE-SPEC2 after Step 5(c)
PE-SPEC3Step 2.2: remodeling parallel paths starting at a receiving image of a fork state
When the image of the fork state is not
a source state for any transition associated to a service primitive, the first
group, formed using the partitioning procedure given in Algorithm3, is empty. In
this case, to prevent the occurrence of an unspecified reception error, the
subpaths of each parallel path in the second group have to be added to each
state in each other path in the group. Each state in a parallel path in the
group must be made as a source state for the first transition in each subpath
of each other path in the group. If the protocol entity under consideration has
a sending image of a joint state, the divergence problem has to be solved using
the same technique illustrated for Step 2.1.The procedure given in Algorithm5
formally illustrates the remodeling technique for the parallel paths starting
at a receiving image of a fork state. For PE-SPEC1 given in Figure
3, the procedure given in Algorithm 5 is applied because s2 is a
receiving state. Since the paths in G2 given in Figure 4(a) end at
state s7, which is a sending state, Step 1 of the procedure is
applied. In Step 1.3, a copy of each of the parallel paths is added to PE-SPEC1,
as shown in Figure 6(a). In Step 1.4, copies of s2 and their
associated transitions are deleted from the copied paths, as shown in Figure
6(b). In Step 1.5, the parallel paths are connected to their copies, as shown
in Figure 6(c). In Step 1.6, states s7′ and s7′′ are
joined together in state s7′. In Step 1.8, the outgoing transition
from state s7 is redirected to initiate from state s7′.  Figure 6(d) shows the application of Steps
1.6 and 1.8. Steps 2, 3, and 4 of the procedure do not make any changes to
PE-SPEC1, given in Figure 6(d), because the first group of parallel
paths is empty, there are just two paths in the second group, and each of the
parallel paths includes one transition.An application of the procedure given in Algorithm5
for the PE-SPEC1 given in Figure 3.
(a)
Step 1.3(b)
Step 1.4(c)
Step 1.5(d)
Step 1.6 and 1.8


### 4.3. Comparison with Other Methods

In the following, we compare our method
for handling concurrency with the two methods we have surveyed earlier in the
paper in Section2.The synthesis method introduced in Park
and Miller [6] cannot be applied to the S-SPEC given in Figure 2 due to
restriction 2. This restriction states that if a path p includes a
transition associated with an event that passes through a SAP s, any
other path executed in parallel with p cannot include a transition
associated with an event that passes through the same SAP s. In Figure
2, the events that pass through SAPs 2 and 3 are associated with the
transitions of both parallel paths, hence violating the second restriction. As
a result, the main concurrency problem due to message collision is not
resolved.The
synthesis method described in Kakuda et al. [10] cannot be applied to the
S-SPEC in Figure 2 because it violates the first restriction of their method.
This restriction states that the S-SPEC model must be a tree. Consequently,
their method cannot deal with the specified concurrent behavior.


## 4.1. The Synthesis Algorithm

Starting from a service specification
modeled in EFSM, the algorithm outlined in Algorithm1 automatically derives the
concurrent protocol entities that provide the set of services given in the
S-SPEC. In the first step, the sequential protocol entities are derived using
Saleh and Probert [4] synthesis method. In the second step, using the
algorithm outlined in Algorithm 2, the protocol entities are remodeled to consider
their concurrent execution.


## 4.2. Additional Transition Rules

To obtain the concurrent PE-SPECs from
the sequential ones, the procedure shown in Algorithm2 is applied. According to
this procedure, only the parallel paths are remodeled. First the parallel paths
are partitioned according to the type of events associated to the first
transition in each path. Then, the paths in each partition are remodeled
according to the type of the image of the fork state (i.e., sending or
receiving state).Step 1: partitioning parallel paths
In the protocol entities, the image of
the fork state can have one or more outgoing transitions. In the case where
there is only one outgoing transition, no message collision can occur. Hence,
no modification is required. In the case where there is more than one outgoing
transition from a states, which is an image of a fork state, the
outgoing paths from state s are partitioned into two groups according to
the type of the event associated to the first transition in each path. There are
two possible types of such events: a service primitive or an event reception.
Paths in which the first transition is associated to a service primitive are
placed in the first group and the others are placed in the second group.
Paths in the first group are initiated
by the protocol entity under consideration. On the other hand, the paths in the
second group are not initiated until the protocol entity has received the
required event. When the protocol entity can execute more than one path in the
first group, it has to select one of them. Once the first transition of a
parallel path in the first group has been executed, the parallel path is
selected and the other parallel paths in the same group are disabled. However,
this case is different for the parallel paths in the second group. To
summarize, when an image of a fork state in a protocol entity is reached, one
of the paths—if there are any—in the first
group is executed along with all paths in the second group. The first two steps
of the procedure given in Algorithm3 illustrate how to partition the parallel
paths.Before the parallel paths are remodeled,
one more refinement action is required for the paths in the second group. Each
path in the second group is divided into subpaths. Each subpath starts with a
transition associated with a receiving event and contains only one such
transition. The use of these subpaths is illustrated below. The third step of
the procedure given in Algorithm3 shows how to divide the paths in the second
group into subpaths.For example, in PE-SPEC1 given in Figure 3, state s2 is an image of a fork state and has more
than one outgoing transition; therefore, the outgoing parallel paths from state
s2 are partitioned into two groups: G1 and G2.
The first group is empty because none of the outgoing transitions from state s2 is associated with a service primitive. Figure 4(a) shows the content of the
second group. The subpaths of the parallel paths given in Figure 4(a) are the
same as the parallel paths because each of the parallel paths contains only one
transition. For PE-SPEC2 given in Figure 3, the outgoing parallel
paths from state s2 are partitioned into two groups. The first and
second groups, G1 and G2, include the paths that start
with a transition associated with a service primitive and a receiving event,
respectively. Figure 4(b) shows the contents of both groups. The subpaths of
the parallel path contained in G2 are the same as the parallel path,
because the parallel path contains only a transition associated with a
receiving event, followed by a transition associated with a service primitive.Application of partitioning procedure on the PE-SPECs given in Figure3.
(a)
G2 for PE-SPEC1(b)
G1 and G2 for PE-SPEC2Step 2.1: remodeling parallel paths starting at a sending image of a fork state
In a PE-SPEC that has a sending image of a fork state, the
first group of the parallel paths is not empty. As discussed earlier, one of
the parallel paths in the first group can be executed along with all the parallel
paths in the second group. This means that at any state for a path in the first
group, any subpath of any parallel path in the second group has to be allowed
to execute, or an unspecified reception error can occur. This can be modeled by
making each state in the first group a source state for the first transition in
each subpath of each path in the second group.
This solution solves the unspecified
reception error problem until the protocol entities reach the image of the
joint state. When any of the protocol entities reach the image of the joint
state, they have to wait for the other protocol entities to reach their images
of the joint state, or an unspecified reception error can occur because of the
divergence between the protocol entities. According to the solution for the
unspecified reception error discussed above, the protocol entity can either
leave the image of the joint state by executing the outgoing transition from
the image of the joint state or execute one of the subpaths added to the image
of the joint state. An unspecified reception error can occur if the protocol
entity executes the outgoing transition from the joint state without executing
the other added transitions. Therefore, it is important to ensure that none of
the protocol entities leaves the image of the joint state unless all other
protocol entities have reached their corresponding state. In other words, it
must be ensured that none of the protocol entities leaves the image of the
joint state unless the last subpath of each parallel path has been executed.
This can be modeled by (1) adding copies of the parallel paths in the first
group, (2) connecting these copies using the last subpaths of the paths in the
second group, and (3) redirecting the outgoing transition from the image of the
joint state to be initiated from the state reached by executing all the last
subpaths under consideration. Note that if the image of the joint state is a
source state for a transition associated to a receiving event, the image of the
joint state cannot be left unless the event message is sent by some other
protocol entity. Therefore, the solution illustrated above has to be applied
only in a protocol entity where the image of the joint state is a source state
of a transition associated to a service primitive.The solutions for the unspecified
reception problem and the divergence problem discussed above are given formally
in the procedure shown in Algorithm4. For PE-SPEC2 given in Figure 3, the
procedure given in Algorithm 4 is applied because s2 is a sending
state. Step 1 of the procedure is not applicable because joint state s7 is not a sending state. In Step 2, copies of the subpath of G2 are
added to each state contained in G1, as shown in Figure 5(a). Step 3
is not applicable because Step 1 is not applicable. Step 4 is not applicable
because there are no redundant transitions connected to the images of the fork
and joint states. Finally, in Step 5, the path contained in G2 is
removed from PE-SPEC2. The resulting PE-SPEC2 is shown in
Figure 5(b). PE-SPEC3 and PE-SPEC2 given in Figure 3 are
similar to each other; therefore, the same synthesis steps apply. The resulting
PE-SPEC3 is shown in Figure 5(c).An application of the procedure given in Algorithm4 for the PE-SPEC2 and PE-SPEC3 given in Figure 3.
(a)
PE-SPEC2: Step 2(b)
PE-SPEC2 after Step 5(c)
PE-SPEC3Step 2.2: remodeling parallel paths starting at a receiving image of a fork state
When the image of the fork state is not
a source state for any transition associated to a service primitive, the first
group, formed using the partitioning procedure given in Algorithm3, is empty. In
this case, to prevent the occurrence of an unspecified reception error, the
subpaths of each parallel path in the second group have to be added to each
state in each other path in the group. Each state in a parallel path in the
group must be made as a source state for the first transition in each subpath
of each other path in the group. If the protocol entity under consideration has
a sending image of a joint state, the divergence problem has to be solved using
the same technique illustrated for Step 2.1.The procedure given in Algorithm5
formally illustrates the remodeling technique for the parallel paths starting
at a receiving image of a fork state. For PE-SPEC1 given in Figure
3, the procedure given in Algorithm 5 is applied because s2 is a
receiving state. Since the paths in G2 given in Figure 4(a) end at
state s7, which is a sending state, Step 1 of the procedure is
applied. In Step 1.3, a copy of each of the parallel paths is added to PE-SPEC1,
as shown in Figure 6(a). In Step 1.4, copies of s2 and their
associated transitions are deleted from the copied paths, as shown in Figure
6(b). In Step 1.5, the parallel paths are connected to their copies, as shown
in Figure 6(c). In Step 1.6, states s7′ and s7′′ are
joined together in state s7′. In Step 1.8, the outgoing transition
from state s7 is redirected to initiate from state s7′.  Figure 6(d) shows the application of Steps
1.6 and 1.8. Steps 2, 3, and 4 of the procedure do not make any changes to
PE-SPEC1, given in Figure 6(d), because the first group of parallel
paths is empty, there are just two paths in the second group, and each of the
parallel paths includes one transition.An application of the procedure given in Algorithm5
for the PE-SPEC1 given in Figure 3.
(a)
Step 1.3(b)
Step 1.4(c)
Step 1.5(d)
Step 1.6 and 1.8


## 4.3. Comparison with Other Methods

In the following, we compare our method
for handling concurrency with the two methods we have surveyed earlier in the
paper in Section2.The synthesis method introduced in Park
and Miller [6] cannot be applied to the S-SPEC given in Figure 2 due to
restriction 2. This restriction states that if a path p includes a
transition associated with an event that passes through a SAP s, any
other path executed in parallel with p cannot include a transition
associated with an event that passes through the same SAP s. In Figure
2, the events that pass through SAPs 2 and 3 are associated with the
transitions of both parallel paths, hence violating the second restriction. As
a result, the main concurrency problem due to message collision is not
resolved.The
synthesis method described in Kakuda et al. [10] cannot be applied to the
S-SPEC in Figure 2 because it violates the first restriction of their method.
This restriction states that the S-SPEC model must be a tree. Consequently,
their method cannot deal with the specified concurrent behavior.


## 5. Conclusions and Future Work

In this paper, a synthesis method for
concurrent protocol specifications from service specifications is introduced.
Both the service and protocol specifications are modeled using FSM-based
models. The service specification FSM-based model is extended to model
concurrency behaviors. The synthesis method first uses a previously introduced
method to synthesize sequentially based protocol specifications, then the
synthesis method remodels the derived protocol specifications by adding new
states and transitions to handle the concurrency behavior specified in the
service specification. In contrast with methods introduced earlier, the
synthesis method introduced here solves the true concurrency problem such that
if a message collision occurs, all parallel paths proceed without canceling any
event. In addition, the synthesis method introduced here eliminates all the
restrictions imposed by the earlier methods. As a result, the synthesis method
is applicable to a wider range of concurrent applications.The synthesis method introduced in this
paper does not consider medium channel delays and timing requirements that can
be provided in the service specification. In the future, we plan to study the
assignment of timing constraints to a service specification that has
concurrency behavior. In addition, we plan to extend the introduced synthesis
method to map the timing constraints associated with the transitions of the
service specification model to the transitions of the protocol specification
models.Algorithm 1:The synthesis algorithm.
Synthesis algorithm. Derivation of concurrent protocol specification from a service specification.Input: EFSM-based service specification.Output: Concurrent FSM-based PE-SPECs.Steps:(1) apply the sequential-based protocol synthesis method introduced in Saleh and Probert [4],(2) apply the From_Sequential_To_Concurrent_PEs procedure given in Algorithm 2 to obtain the concurrent PE-SPECs.Algorithm 2:  Procedure for obtaining concurrent-based PE-SPECs from sequentially based PE-SPECs.
Procedure:   From_Sequential_To_Concurrent_PEsInputs: Sequentially based PE-SPECs modeled using FSMs.Outputs: Corresponding concurrent-based PE-SPECs modeled using FSMs.Steps:for each PE-SPEC dofor each state s which is an image of a fork state in PE-SPEC doif  state s has more than one
outgoing transition then(1) apply
Partition_Parallel_Paths procedure,(2) if
s is a sending state then(2.1) apply Re-Model_Parallel_Paths_for_Sending_State procedure,(2.2) else apply Re-Model_Parallel_Paths_for_Receiving_State procedure.Algorithm 3:  Partitioning procedure.
Procedure:    Partition_Parallel_PathsInputs: A PE-SPEC and an image of a fork state s in the PE-SPEC model.Outputs: Groups of parallel pathspartitioned at state s and a set of sub-paths of each path in a group.Steps:(1)G1=G2={},(2)for each transition t outgoing from state sdo(2.1) if
t, which is the first transition in an image of a parallel path p, is associatedwith a service primitive thenG1=G1∪p
else
G2=G2∪p,(3)for each path p in G2do(3.1) SUBp={}{set of sub-paths of p},(3.2) s0=s,(3.3) while (s0 is
not a joint or free state) do(3.3.1) s1=successive(s0)p,(3.3.2) while (s1 is
not a joint or free state and the outgoing transition from s1 is notassociated with a receiving event) do(3.3.2.1) s1=successive(s1)p,(3.3.3) SUBp=SUBp∪ subpath of p from s0 to s1,(3.3.4) s0=s1.Algorithm 4: A procedure for remodeling the PE-SPEC to consider the concurrency behavior
in the case where there is a sending image of fork state.
Procedure:  Re-Model_Parallel_Paths_for_Sending_State.Inputs:– a PE-SPEC that has an image state s of a fork
state such that s is a sending state,– G1, G2, and the subpaths found
using the Partition_Parallel_Paths procedure given in Algorithm 5.Outputs: a remodeled PE-SPEC that has additional states and
transitions to consider theconcurrency behavior of the service specification.Steps:(1)if  the paths in G1 and G2 end with an image of a joint state and this joint
image state is a sending state then(1.1) LastSUBs ={},(1.2) for each path in G2do(1.2.1) LastSUBs = LastSUBs ∪ last sub-path in SUBp,(1.2.2) SUBp=SUBp− last sub-path in SUBp.(1.3) add to the
PE-SPEC model ∑i=1nC(n,i) copies of each path in G1,
where n=|G2| (i.e.,number of paths in G2) and C(n,i)=n!/(i!(n−i)!),(1.4) connect each path in G1 and its copies together using all subpaths in LastSUBs suchthat each combination of the subpaths is covered once. Connecting two paths using asubpath includes connecting each state in one of the paths to its corresponding state inthe other path using the subpath,(1.5) join all
copied states that have no outgoing transitions together in a state j,(1.6) delete all
redundant transitions connected to state j,(1.7) redirect the
outgoing transitions from the joint state image to be initiated from state j,(2)for each state sg in G1do(2.1) for each path p in G2,(2.1.1) for each sub-path in SUBpdo(2.1.1.1) add a copy of
the subpath to state sg such that the state sg is, respectively,the tail and head state of the first and last transitions in the subpath.(3)if  there are copied paths
created using Step 1.3 then(3.1) for each copied path c of an original path p do(3.1.1) let q be the path from any state in p to its copied state in c,(3.1.2) for each subpath sp added in Step 2.1.1.1 to a state in p
do(3.1.2.1) if
sp is a subpath of a path g and
none of the transitions in q is a subpath in path gthen(3.1.2.1.1) for each state sc in
path cdo(3.1.2.1.1.1) add a copy of
the subpath sp to state sc such that the state sc is,
respectively,the tail and head state of the first and last transitions in the
subpath.(4) Delete
redundant transitions connected to the images of the fork and joint states.(5) Remove all paths in the groups in the setG2 excluding the images of the fork and joint states in these paths.Algorithm 5: A procedure for remodeling the PE-SPEC to consider the concurrency behavior in the case where there is a receiving image of fork state.
Procedure:  Re-Model_Parallel_Paths_for_Receiving_StateInputs:– a PE-SPEC that has an image state s of a fork
state such that s is a receiving state,– G1, G2, and the subpaths found
using the Partition_Parallel_Paths procedure given in Figure 10.Outputs: a remodeled PE-SPEC that has additional states and
transitions to consider the concurrencybehavior of the service specification.Steps:(1)if   the paths in G2 end with an
image of a joint state and this state is a sending state then(1.1) LastSUBs ={},(1.2) for each path p in G2do(1.2.1) LastSUBs = LastSUBs ∪ last sub-path in SUBp,(1.3) add to the
PE-SPEC model ∑i=1nC(n,i) copies for each path in G2,
where n is |G2|−1,(1.4) delete the
copies of the image of the fork state and their associated transitions from the
copied paths,(1.5) for each path p in G2do(1.5.1) LastSUBnp=LastSUBs− last
sub-path in SUBp,(1.5.2) connect the
path p and its copies together using all subpaths in LastSUBnp such that eachcombination of the subpaths is covered once. Connecting two
paths using a subpathincludes connecting each state in one of the paths to its
corresponding state in the otherpath using the subpath,(1.6) join all
copied states that have no outgoing transitions together in a state j,(1.7) delete all
redundant transitions connected to state j,(1.8) redirect the
outgoing transitions from the joint state image to be initiated from state j,(1.9) for each path in G2(1.9.1) SUBp=SUBp−
last subpath in SUBp,(2)for each path g  in G2do(2.1) for each path p in the
set G2−gdo(2.1.1) for each state sg  in
path g excluding the image of the fork state do(2.1.1.1) for each sub-path sp in SUBp
do(2.1.1.1.1) add a copy of
the subpath sp to state sg such that the state sg  is, respectively,the tail and head state of the first and last transitions in the
subpath sp.(3)if  there are copied paths
created using Step 1.3 then(3.1) for each copied path c of an original path p
do(3.1.1) let q be any path from any state in p to its copied state in c(3.1.2) for each subpath sp added in Step 2.1.1.1.1 to a state in p
do(3.1.2.1) if
sp is a subpath of a path g and
none of the transitions in q is a subpath in path g
then(3.1.2.1.1) for each state sc in
path   c
do(3.1.2.1.1.1) add a copy of the subpath sp to state sc such that the state sc is, respectively,the tail and
head state of the first and last transitions in the subpath.(4) Delete redundant transitions connected to the image of the joint state.



---

*Source: 794960-2008-09-14.xml*