数理解析研究所講究録
918 巻 1995 年 72-84

72

Protocol Synthesis from Service Specifications
Described byGraph Rewriting Rules
Akira Takura

Takafumi Sera

Tadashi Ohta

ATR Communication Systems Research Laboratories
2-2 Hikaridai, Seika-cho, Soraku-gun, Kyoto 619-02 Japan
Abstract
A protocol synthesis method is proposed to derive
communications software from service specifications of
distributed systems. A communications service specification can be described as a set of graph rewriting
rules. Each rule specifies a global state transition ofmultiple terminals associated with an event occurringat one of the terminals. The communications system
is regarded as a black box in this description. A rule
is represented by a pair of labeled directed graphs. The
state of all the terminals in a communications sys$tem$ is also represented as a labeled directed graph.
In this graph representation, a communications service specification describes a set of rules to find theappropriate graph representing the condition part of arule; its resultant is substituted for an isomorphic subgraph in a graph representing a communications$tem$ . The isomorphic subgraph detection is known to
be $NP$-complete. The derived distributed programs operate within a time practical for application because of
the limited number of terminals usually associated witha communications service. Accordingly, the proposed
software specification generation method can be used
to develop communications soflware. The proposed
software generation method can be applied to manykinds of distributed system based on state transition
systems.
$sy_{S-}$

1Introduction

Communications software generation from service
specifications is a promising way to reduce the costof developing reliable communications software. This

paper proposes a communications software generation method from service specifications that can be
described without detailed knowledge of communications systems or communications service implementation methods.
Many specification languages including SDL [1] andLOTOS [2] have been proposed for specifying communications software or protocols $[3, 4]$ . When theselanguages are used to develop communications software, stepwise refinement of specifications is needed[5, 6, 7]. Cameron et al. [5] uses rule-based language
L.O for implementing a real-life protocol. Tsai et al. [6]uses frame-and-rule oriented requirement specification
language FRORL. In these methods, specifications are
incrementally refined to obtain protocol specifications;however, they could not synthesize protocol specifications from service specifications.
Bochmann and Gotzhein $[8, 9]$ , Chu and Liu [10],Saleh and Probert [11], and Kakuda et al. [12] proposes protocol synthesis methods from service specifications. In these methods, all actions at service accesspoints and their execution orders are described. In thispaper, a specification description language STR (State
Transition Rule) [13] is used for describing communications service specifications. In STR communications
service specifications can be described by specifying
terminal behavior which can be recognized from outside of a communications system. With this method,
we can describe specifications without detailed knowledge of the target communications system. A service isdefined as a set of production rules. Consequently, we
do not have to describe the execution order of eventsat service access points.
STR assumes that a communications system consists of homogeneous processes that correspond to ter-

73

minals. Processes sharing a relationship form a global
state. Each STR rule specifies a global state transition of terminals for an input event that has occurred
at a terminal. In this service specification description,
terminals are defined as service access points in a communications system. Since communications systems
are geographically distributed systems, we generate acommunications protocol that can operate using local
state of terminals when global state transitions areaccess points SAPI,, SAP . Within the communications system, protocol entities cooperate to provide
services by exchanging messages. This communication
between protocol entities is provided by the service
provider of lower layers. In communications services
including telephone services terminals correspond to
SAP in Fig. 1.

given.

User 1The state of a terminal connected to a communications system is represented by a subgraph of a labeled
directed graph that represents the state of all the terminals. Using this graph representation, an STR rulecan be regarded as a graph rewriting rule consisting of
an initial graph and a next graph. Kawata et al. [14]proposes a protocol synthesis method with a restriction: in the initial graph of an STR rule, there is a pathgoing through all labeled vertices. This restriction is
imposed for the sake of reducing the number of communications between processes. The synthesized pro-fro communication among vertices
tocol makes
in an initial graph. This paper presents a new methodthat obtains local state transition systems from service specifications described by global state transition-fro comrules. The synthesized protocol makes
munication among vertices in an initial graph; however, there is no restriction imposed on initial graphs.
The proposed protocol synthesis method from service specifications takes a step toward automated software generation. Communications software can be obtained from synthesized protocol specifications by using a stepwise refinement method [15].
Section 2 defines communications service specifications and protocol synthesis. Section 3 briefly reviews
STR. .In section 4 we define a problem to be solved.
Section 5 proposes a protocol synthesis method. Finally we show an example of the proposed protocol
synthesis method.

$\cdots$$\mathrm{n}$User 2User$\mathrm{n}$$\mathrm{t}_{\mathrm{O}-}\mathrm{a}\mathrm{n}\mathrm{d}$Figure 1: Layered architecture model$\mathrm{t}_{0-}\mathrm{a}\mathrm{n}\mathrm{d}$2.2Bochmann, Gotzhein $[8, 9]$ , Chu et al. [10], andSaleh et al. [11] propose protocol synthesis methods
assuming the relation between services and protocols
illustrated in Fig. 1. Kakuda et al. [12] propose aprotocol synthesis method that includes simultaneous
occurrence of multiple events at different SAPs. A
communications system provides users with communications services through SAPs. In this modeling,
service specifications and protocol specifications aredefined as follows [16]:

.

and

2

Service Specifications
Protocol Synthesis

2.1

Communications Software Model

Protocol synthesis generates error-free protocols
from service specifications. Most protocol synthesis
methods assume alayered architecture as in Fig. 1. A
communications system provides communications services for users who access the system through service

Service and Protocol Specifications.

The service specification describes what services
the protocol entities of the lower protocol layer
provide for users in the upper protocol layer. The
services provided by the lower protocol layer are
based on a set of service primitives that describe
the operations at service access points throughwhich the services are provided.
The protocol specification describes interactions
among protocol entities of the lower protocol
Interactions are defined in terms oflayer.
services provided to the upper protocol layerand services available from the communication
medium.

74

Hereafter, a protocol entity is called a process.

3Service
guage

3.1

STR

Specification

Lan-

A vertex that has a label or an edge incident from
it is called labeled. Other vertices are called unlabeled.
For each vertex in an initial graph, there must be apath from the vertex where an event occurred.
dial-tone(A), idle(B)dial(A,B):
ring-back(A,B), ringing(B,A).

A service is defined as a set of STR rules. An STR
rule has the form:
initial state

event:

Figure 2: An example of an STR rulenext state.

The “initial state” and the “next state” represent
global states of terminals. A global state is represented by a set of local states. A local state is represented by a set of state primitives. A state primitive may have two arguments to express terminals.
The first argument represents the terminal having thestate primitive. If the second argument is specified,
the terminal designated by the first argument holds a
relation of the primitive to the terminal specified by
the second argument. Therefore, the local state of aterminal is defined as the set of state primitives whose
first argument designates the terminal. A state primitive represents a terminal state which is recognizablefrom outside of a communications system.
”
may also have two arguments to exThepress terminals. It represents a logical input to theterminal designated by the first argument. If the second argument is described in an event, it represents aterminal identifier given by the event.

transition$[eggA][eggB]\underline{\mathrm{d}\mathrm{i}\mathrm{a}\mathrm{l}}$dial-tone–$\overline{\mapsto}\mathrm{A}\mathrm{O}^{\mathrm{B}}\underline{\mathrm{n}\mathrm{n}\mathrm{g}\mathrm{b}\mathrm{a}\mathrm{C}\mathrm{k}}$rmgingidle

Figure 3: Graph representation of an STR rule
A global state for all the processes in a communications system is called a system state; the graphdenoting the system state is called a system graph.

3.3

Application of STR Rules($‘ \mathrm{e}\mathrm{v}\mathrm{e}\mathrm{n}\mathrm{t}$3.2Graph Representation

We use graph representation of an STR rule to generate communications protocol from service specifications described with STR. An STR rule can be represented by two graphs. The initial graph corresponds
to the initial state and an event; the next graph corresponding to the next state. Both an initial and anext graphs are called rule graphs. Figure 3 shows thegraph representation of the rule described in Fig. 2.
A rule graph consists of a set of vertices and directed edges. Each vertex has its own name and somevertices have labels. A vertex is denoted by a circle.
The name of a vertex is written in a circle, and thelabel of a vertex is written near the circle. Each edge
has labels that are written near it. An initial graphhas a label that shows an event. A vertex designatedby the first argument of this label is called an event
vertex.

According to an STR rule, in a system graph asubgraph that is isomorphic to the initial graph ofthe rule should be replaced by the next graph of therule. Figure 4 illustrates how an STR rule is applied.
If there are two rules $r1$ and $r2$ such that the initialgraph of $r1$ is isomorphic to a subgraph of the initialgraph of $r2$ , then $r2$ is superior to $r1$ . We denote $r1$$<r2$ iff $r2$ is superior to $r1$ . This is not total-order.
Thus, there still exists the possibility that multiple
rules may be applied. When multiple rules can beapplied, a rule may be arbitrarily selected.

4

Problem

Let $g=(V, E, v^{0})$ be a rooted labeled directed
graph that has a set of vertices , a set of directededges $E$ and a root vertex . For each vertex of arooted directed graph, there is a path fromto thevertex. The set of vertices of is denoted by $V(g)$ .
The set of edges of is denoted by $E(g)$ . The root of
is denoted by root $(g)$ . A labeled directed graph isdenoted by $g=(V, E)$ with a set of vertices and aset of directed edges $E$ .
$V$

$g$

$v^{0}$$v^{0}$

$g$

$g$

$g$

$g$

$V$

75

3. If $(u, v)$ is an edge of $sp(g)$ , then every vertex
between root $(g)$ and as well as between
and appears before in $sp(g)$ .
$\mathrm{r}oot(g)$

$u$

$u$

$v$

The problem to be solved is formally defined as follows.

Definition 3 (Problem)
Let $R=\{r_{1}, \ldots, r_{n}\}$ be a set of $STR$ rules. Let $G=$
be a set of initial graphs of R. Let $G’=$
be a set of next graphs of R. Let $g=(V, E)$
be a system graph.
such thatFind a pair of graphs $(sg(v^{0}, g),$$sg(v^{0}, g)$ is isomorphic to $g_{i}\in G$ , and there is no
is isomorgraph isomorphic to $g_{k}\in G$ such thatphic to a subgraph of . Then change $sg(v^{0}, g)$ to be.
isomorphic to$\{g_{1}, \ldots, g_{n}\}$$\{g_{1}’’, \ldots, g_{n}\}$$g_{i})$$g_{i}$$g_{k}$$g_{i}’\in G’$

The following lemma is satisfied for subgraph isomorphism. We use this lemma to construct a distributed algorithm.

Figure 4: Application of STR rules
Definition 1 (Subgraph isomorphism)
Let $g=(V, E)$ be a labeled directed graph and$(V_{1}, E_{1,1}v)0$
be a rooted labeled directed graph. The
graph contains a subgraph $g’=(V’, E’, v^{0})$ isomor$ph.ic$ to
if and only if there exist sub.s. $et_{S}V’\subset V$ and$E’\subset E$ such that $v^{0}\in V’,$ $|V’|=|V_{1}|,$ $|E’|=|E_{1}|$ ,and there is one to one mapping : $V_{1}arrow V’$ thatsatisfies the following conditions.
$\dot{g}_{1}=$$g$$g_{1}$

$f$

$a$

Lemma
Let $g=$be a labeled directed graph andbe a rooted labeled directed graph.
with the set of edges
Let be a spanning path of$(u_{m-1},$ um)} where, and $V_{1}=${$\{u_{1}, \cdots, u_{m}, u_{m+1}, \cdots, u_{n}\}$ .
The graph contains
if anda subgraph $g’=(V’, E’, v^{0})$ isomorphic toonly if $|V’|=|V_{1}|,$ $|E’|=|E_{1}|$ , and there is a mapping: $V_{1}arrow V’$ that satisfies the following conditions.
inand unlabeled
For any labeled verticesin ,verices$f(u_{1}^{0})=v^{0}$ ,$u_{i}\neq u_{j}\Rightarrow f(u_{i})\neq f(u_{j})$ ,$f(u_{i})\neq f(u_{k})$ ,$u_{k}\neq u\iota\Rightarrow f(u_{k})\neq f(u_{l})$ ,$(u_{i}, u_{j})\in E_{1}\Leftrightarrow(f(u_{i}), f(uj))\in E’$ ,$(V, E)$$g_{1}=(V_{1}, E_{1,1}v)0$$p$$(u_{1},$$g_{1}$$u_{2}),$$u_{1}=v_{1}^{0}$$\cdots,$$g$$g_{1}$$f$$u_{i},$$f(v)1v_{1}(x, y)\in E00=.\Rightarrow(f(x), f(y))\in E’$..

$(f(x), f(y))\in E’\Rightarrow(x, y)\in E_{1}$$\alpha(x)\subset\alpha(f(x))$$\beta((_{X}, y))\mathrm{c}\beta((f(X), f(y)))$is a function to get a set of labels attachedwhere
on a vertex and is a function to get a set of labels
attached on an edge.
$\alpha$$\beta$$u_{k},$$u_{l}$$u_{j}$$V_{1}$$V_{1}$$\alpha(u_{i})\subset\alpha(f(u_{i}))$$\beta((u_{i}, u_{j}))\subset\beta((f(u_{i}), f(uj)))$$\beta((u_{i}, u_{k}))\subset\beta((f(u_{i}), f(uk)))$

If

$g$

$g_{1}\subset g$

has a subgraph isomorphic to$g_{1}$, then we write.

Definition 2 (Spanning path)
For a rooted labeled directed graph , a spanning path$sp(g)$ is defined as a path that satisfies the following
conditions.
$g$

1. The vertices of $sp(g)$ is the set of labeled vertices
in .
$g$

2. The root of $sp(g)$ is root $(g)$ .

This lemma implies that we can determine applicability of a rule by traversing along its spanning path.

5

Definitions

Protocol synthesis is to generate a distributed algorithm to find an isomorphic subgraph in a systemgraph. Each protocol entity holds a local state of aterminal. Then protocol synthesis is defined to derive protocol entity specifications with local states

76

from communications service specifications describedby global state transition rules.
When a protocol entity receives an input from aterminal or some other protocol entity, it determines
a rule to be applied or sends another protocol entity
a request to inquire a surrounding global state determining an applicable rule. This communication forstate inquiry is perfomed sequentially. Finally a ruleis determined. The rule is informed the protocol entities that are inquired their states. Then each protocol
entity changes its state according to the rule.
A spanning path is determined for each rule. The
communication for state inquiry goes along a spanning path. If there are isomorphic subgraphs in multiple initial graphs, it is determined at the same time
whether a system graph contains a subgraph isomorphic to the subgraphs. This reduces communication
between protocol entities. For this purpose, we utilize a spanning path of a tree generated by overlapping spanning trees of the initial graphs of an event.
This spanning path is called a provisional communication path. A synthesized protocol communicates alongprovisional communication paths. We give these definitions. Note that sometimes a vertex and a process
are used for the same meaning.
Letdenote a set of initial graphs with an event$\mathrm{C}(e)$$e$graph $r2$ . Consequently, there are four vertices $<r1$ ,$\{r1, r2, r3, r4\}>,$ $<r2,$ $\{r2, r4\}>,$ $<r3,$ $\{r3\}>$and $<r4,$$\{r4\}>\mathrm{i}\mathrm{n}$this rule inclusion graph.

$rl)$$r\mathit{2})$$r\mathit{3})$$r\mathit{4})$$\mathrm{u}$: event

Figure 5: Example of initial graphs.

Rule inclusion graph Let
be a connected subgraph that has an event vertex and is isomorphic
to subgraphs of more than one element in.
Letdenote the set of elements ofthathave as their subgraphs. An ordered paira vertex of the rule inclusion graphof
if a graph generated from by adding
an edge is a subgraph of an element of, and. An ordered pair $<r,$isalso a vertex of the rule inclusion graph ofif. There is an edge from $<s,$
to $<t,$iff (1), and (2) there is noother element $<u,$
that
and
.
$s$

$\mathrm{C}(e)$$\mathrm{D}(s)$$\mathrm{C}(e)$

$<$

$s$

$s,$

$\mathrm{D}(s)>\mathrm{i}\mathrm{s}$$s’$$\mathrm{C}(e)$$s$$\mathrm{C}(e)$$\mathrm{D}(s)\neq \mathrm{D}(s’)$$\mathrm{D}(r)>$$\mathrm{C}(e)$$r\in \mathrm{C}(e)$$\mathrm{D}(s)>$$s\subset t$$\mathrm{D}(t)>$$\mathrm{D}(u)>\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{h}$$s\subset u$

Figure 6: Example of a rule inclusion graph$u\subset t$

Rule inclusion graphs are used for determining orders of inquiring rule applicability. If there is an edge
from $<s,$
to $<t,$in a rule inclusion graph, then graph is examined before graphwhether they are included in a system graph.
Figure 5 represents initial graph examples. Figure
6 shows the rule inclusion graph for the set of initialgraphs in Fig. 5. The rule graph $r1$ is the maximum
subgraph common to the rule graphs $r2$ and $r3$ , andthe maximum subgraph of the rule graph $r4$ is the rule$\mathrm{D}(s)>$$\mathrm{D}(t)>$$s$Rule covering tree Let $g_{r}=(v_{r}, e_{r}, v^{0})$ be the initial graph of a rule . Let $t_{r}=(w_{r}, f_{r}, v^{0})$ be
a spanning tree of . A rule covering tree isdefined as follows:$r$$g_{r}$$\mathrm{c}_{r}$$t$The set of vertices of$\mathrm{c}_{r}$is$\mathrm{v}_{r}$, and root $(c_{r})=v^{0}$ .

The edges from the same vertex are arranged
clockwise by lexicographic order of edge labels.
The set of edges of is the union of and theedges satisfying the following two conditions:$\mathrm{c}_{r}$$\mathrm{e}_{r}$77

1. If a leaf vertex of has a label, there exists
an edge whose initial vertex is the leaf vertex of.
$\mathrm{t}_{r}$$\mathrm{t}_{r}$has a label of an ordered
2. An edge $ab$ ofpair. The first element of the label is the labelof in , and the second element is the label of$ab$ in.
$\mathrm{c}_{r}$$a$$\mathrm{v}_{r}$$\mathrm{e}_{r}$2. For each element inisomorphic to .
$g$$\mathrm{C}(e)$, there is a subgraph$g$

3. If vertices and in rule covering trees
and , respectively, are overlapped, then every
vertex between root $(S)$ and is overlapped to
the vertex in satisfying that its depth is theandis a vertex between
same as that ofroot $(t)$ and .
$u$

$s$

$v$

$t$

$u’$

$u$

$v’$

$t$

$u’$

$v’$

$v$

A rule covering tree is uniquely determined for aspanning tree of an initial rule graph. A rule covering tree must satisfy the following two conditions fordefining a rule overlapping tree. Let be a spanning
tree of the initial graph for rule , and a rule covering
tree generated from .
(1) is an unlabeled subgraph of the initial graphfor rule .
for the two(2) Let be a vertex of . Assume
vertices and in the rule inclusion graph that has avertex whose first element is . If is a vertex of ,and is not a vertex of , then an edge from one ofthe vertices in to is included.
Figure 7 shows rule covering trees for the initialgraphs in Fig. 5.
$s$

$t$

$r$

$s$

$s$

4. If deges and are overlapped, then the labels of and are the same or the one is includedin the other.
$f$

$e$

$f$

$e$

5. The overlapping is performed in the lexicographic order of the labels of edges with the same
initial vertex.

$r$

$u$

$g$

$g\subset h$

$s$

$h$

$r$

$u$

$h$

$u$

A rule overlapping tree is used for examining at thesame time whether the common subgraphs in multiple
rule graphs are included in a system graph.

$g$

$g$

$u$

Provisional communication path A provisionalis defined as a pathcommunication path forwhose vertices is the vertices in the rule overlapsuch that:ping tree of$\mathrm{C}(e)$$\mathrm{C}(e)$1. The initial vertex is the event vertex.
2. Let and be two graphs constituting thefirst elements of two vertices in the rule inclusion. If
is a vertex in bothgraph forand ; if is not a vertex of but a vertex of ,then appears before .
$h$

$g$

$g\subset h,$ $u$$\mathrm{C}(e)$

$h$

$g$

$v$

$h$

$g$

$v$

$u$

3. Let be a graph corresponding to a vertex. For anyin the rule overlapping graph forgraph corresponding to a vertex in the rule, assume
such that
inclusion graph forthat and are vertices in , but not in . In ,if is a vertex in the path from the event vertex
to , or there is a vertex in the path from theevent vertex to such that is in the path fromthe event vertex to and is not a vertex in ,then appears before .
$h$$\mathrm{C}(e)$$g$$g\subset h$$\mathrm{C}(e)$

$u$

$h$

$v$

$g$

$h$

$u$

$w$

$v$

$w$

$u$

$w$

$v$

$u$

$g$

$v$

4. A unique label is attached to each edge.
Figure 7: Example of rule covering trees

We note that the vertex sequence of the provisional
includes the sequence ofcommunication path for
as a subsea spanning path for each element of
quence. It implies that state inquiry along a provisional communication path may determine a rule tobe applied.
$\mathrm{C}(e)$$\mathrm{C}(e)$Rule overlapping tree A rule overlapping tree for.
is generated by overlapping graphs inconditions.
following
satisfiesthe
The tree$\mathrm{C}(e)$1. All the roots of the initial graphs inoverlapped.

$\mathrm{C}(e)$$\mathrm{C}(e)$isInquiry message An inquiry message is a uniquemessage for each edge between adjacent vertices

78

in a provisional communication path. In the synthesized protocol, an inquiry message has thefollowing information in addition to its message

name.

Figure 8 shows the rule overlapping tree for the
initial graphs in Fig. 5 and its provisional communication path.

Actual communication path An actual communication path is a provisional communication
path whose vertices are actual process identifiers
to be inquired. Each process decides which process to send an inquiry message by using thisinformation.
Temporary decided rule The rule with thehighest priority in the rules satisfying their rule
application conditions, i.e. their initial graphs
are included in the system graph.

Rule candidates The remaining rules to bechecked for applicability. When a process receives an inquiry message it screens rule candidates included in a received inquiry message bychecking its local state.

Connection information Process informationnecessary for connection tests.
Visited processes A sequence of visited processes after an event occurred.
Temporary process sequence A process sequence for the current temporary decided rule.

Branches A branch consists of a process identifier and an inquiry message. When a process receives an inquiry message, the process compares
its state with a subgraph of the rule overlapping
tree corresponding to the inquiry message for obtaining a new inquiry message and branches (i.e.
actual communication paths). This subgraphis the intersection of the rule overlapping tree
and rule covering trees corresponding to rules
contained in the rule candidates of the inquiry
message. If plural actual communication paths
to be inquired are obtained, the remaining actual communication paths except arbitrary one
are stored as elements of inquiry messages inbranches. Process identifiers are determined as
the processes to which the obtained inquiry messages are sent.

Provisional communication path$[egg1]\underline{\mathrm{m}1}\underline{\mathrm{m}}[egg2] 2\mathrm{r}^{\mathrm{m}}34arrow \mathrm{O}\underline{\mathrm{m}}5[egg6] 34\underline{\mathrm{m}5}$

Figure 8: Example of a rule overlapping tree
Response message A message denoting whether toapply a rule or nothing at all. When a rule isindicated, it contains information which process
the received message corresponds to.

Figures 9 and 10 show actual communication paths
when the graphs are included in a system graph. The
dotted arrows represent communication between processes and the inquiry messages attached to them.
In the example of Fig. 9, inquiry messages are communicated along a provisional communication path.
Process A sends a message ml $(r1, r2, r3, r4)$ that
implies rules $r1,$ $r2,$ $r3$ and $r4$ are rule candidates.
When receives it, determines rule $r1$ is includedin the system graph, and rules $r2,$ $r3$ , and $r4$ are to
be checked for their applicability. Then sends a
message $\mathrm{m}2(r2, r3, r4)$ . When receives the message$\mathrm{m}2(r2, r3, r4))\mathrm{C}$ sends $\mathrm{m}3(r2, r3, r4)$ tothat isincluded in the received message as an actual communication path. In the end receives a meesage,$r4)$ and determines that rule $r4$ is included in the system graph. Since $r4$ is not included in any other initialgraph, detemines that rule $r4$ is to be applied. Then
sends processes
and a response message
indicating that each process changes its state according to rule $r4$ . also changes its state.
In the example of Fig. 10, inquiry message are communicated along a provisional communication pathbut some intermediate processes are skipped. When
receives a message $\mathrm{m}1(r1, r2, r3, r4),$ determines$\mathrm{B}$$\mathrm{B}$$\mathrm{B}$$\mathrm{B}$$\mathrm{D}$$\mathrm{E}$$\mathrm{m}4(r3$$\mathrm{E}$$\mathrm{E}$A provisional communication path indicates inquiry messages used for examining whether rulegraphs are included in a system graph, and their communication paths. An inquiry message usually implies
multiple rules to be checked whether they are included
in a system graph.

$\mathrm{C}$$\mathrm{C}$$\mathrm{A},$$\mathrm{B},$$\mathrm{C}$$\mathrm{D}$$\mathrm{E}$$\mathrm{B}$$\mathrm{B}$79

Figure 9: Example of communication along a provisional communication paththat rule $r1$ is a temoporary determined rule, rules$r2$ and $r4$ are not included in the system graph, andrule $r3$ is to be checked its applicability. In the end
determines rule $r3$ is the rule to be applied.

$\mathrm{F}$Figure 11: Example of non-tree initial graphs

arate state transition segments are generated. One segment receives a predetermined inquiry message in the provisional
communication path, sends another inquiry message along the provisional communication path, and then changes to thenext state. The other segment receives
a response message that includes a deterchanges to the next state.
mined ruleFigure 10: Example of communication skipping intermediate processes
Figure 11 shows an example of non-tree initialgraphs. Figure 12 shows the rule overlapping tree
and its provisional communication path for non-tree
initial graphs in Fig. 11. Figure 13 illustrates provisional communication paths and inquiry messages forthe rules in Fig. 11.

State transition segment One or two state transition segments are generated for each labeledvertex in the initial graph of a rule.

.

.

$\mathrm{a}\ldots \mathrm{n}\mathrm{d}$Connection test A connection test is used to identify graphs that include plural vertices in a provisional communication path. Let and be twovertices in a provisional communication path,and is nearer to the event vertex than . A con$j$$\dot{i}$nection test decides if the edges from excluding
the edge in the provisional communication path
are connected to vertices or vertices connectedby edges from .
$\dot{i}$

$j$

$j$

Figure 14 shows state transition segments of a verobtained from messages in thetex with the label
provisional communication path. Connection tests areomitted in this figure.
Figure 15 shows two initial graphs that need a connection test to distinguish them. The provisional communication path in these two initial graphs is the path
1,2,3. Figure 16 shows subgraphs that can be identified by processes 1 and 3. The two initial graphs in
Fig. 15 are distinguished when process 3 receives amessage that edge is connected to process 4.
$\mathrm{B}$When a vertex is the last vertex in a provisional communication path, a state transition segment is generated such that it
receives a predetermined inquiry message
in the provisional communication path; it
sends a response message and changes tothe next state determined by a rule.

When a vertex is not the last vertex in aprovisional communication path, two sep-$j$$\dot{i}$$\mathrm{b}$

80

.

$rl$

$r2.\cdot$

Provisional communication path$\underline{\mathrm{m}1\backslash r_{J}‘}-$$\underline{\mathrm{m}\angle 1^{\Gamma\angle})}arrow$$\underline{\mathrm{m}s(r\mathit{4}|}arrow$$\underline{\mathrm{m}\angle(\prime \mathit{5})}arrow$$\underline{\mathrm{m}\mathrm{J}(\Gamma \mathrm{J}J}arrow$$[egg1]\underline{\mathrm{m}1}\mapsto 2\mathrm{m}2\mathrm{m}3\mathrm{m}\mathrm{o}3\mathrm{R}4\mathrm{r}54$$r\mathit{3}$:Figure 12: Example of a rule overlapping tree for complicated rules

6

Protocol Synthesis$r\mathit{4}.\cdot$

The protocol synthesis algorithm consists of the following six steps.
(1) Classification of rule graphs
Rules are classified into sets of rules for the same
event. Let
be the set of a rule graph with an
event . For each rule graph set we initially apply
steps 2 to 5, finally, step 6 is applied.
(2) Generation of rule inclusion graph
Generate a rule inclusion graph for each rule graphset.
(3) Generation of rule overlapping tree
Generate a rule overlapping tree.
(4) Determination of provisional communication path and inquiry messages
Determine a provisional communication path andinquiry messages from a rule overlapping tree.
(5) Generation of state transition segments
Generate state transition segments for each vertex
of a rule covering tree corresponding to each rule .
The initial state of a state transition segment is thefirst element of the label attached to an edge incident
from the vertex in the rule covering tree.
(6) Synthesis of process specification
Synthesize a state transition segment from the initial state until no new state is generated. Assume
a new state is generated. Collect all state transition segments whose initial state is included in as a
subgraph. The collected state transition segments aresynthesized as follows.
$\mathrm{C}(e)$

$e$

$r$

$s$

$s$

.

$\underline{\mathrm{m}1(r\mathrm{J}J}arrow$

If two kinds of state transition segments corre-$\underline{\mathrm{m}1(r\mathit{4})}-$$\underline{\mathrm{m}\angle(r4\mathrm{I}}arrow$$\underline{\mathrm{m}\mathrm{J}(r*)}arrow$

Figure 13: Communication for identifying rules in Fig.
11
spond to the final vertex of an initial graph in theprovisional communication path, a middle vertex
is included, and their received messages are thesame, the following synthesis occurs.

The next states of these state transition segments
are changed to the same states as their initialstates. In the synthesized process specification,
the rule candidates of the inquiry message to besent are the intersection of the rule candidates of
the received inquiry message and the set of rules
whose state transition segments are synthesized.
Other information is obtained as described in theabove preliminaries.

-When the resulting rule candidate set is
not empty, the synthesized process sends
the obtained inquiry message to the nearest process in the provisional communication path following the rules contained in
the inquiry message.
-When the resulting rule candidate set is
empty and the branches in the received

81$4^{1}\mathrm{b}\mapsto^{\mathrm{a}}\mathrm{O}$$\mathrm{d}2^{3}$

Figure 16: Subgraphs identifiable with local states
thesized as they are. Each state transition segment is synthesized as described above. Figure
17 illustrates how collected state transition segments are synthesized into a process specification.
$\subset\supset \mathrm{K}.\cdot.\cdot\iota \mathrm{w}\epsilon \mathrm{s}\mathrm{t}\mathrm{a}5\mathrm{e}_{\mathrm{i}_{\mathrm{V}\epsilon}}$$\square$: sendFigure 14: State transition segments

Figure 15: Two graphs requiring a connection test for
identification

message are empty, two possible conditions
exist: if the temporary decided rule is contained in the received inquiry message, therule should be applied; if the temporary
decided rule is not contained, a special response message is sent to all the visitedprocesses.

.

-When the resulting rule candidate set is
empty but the branches in the received
message is not empty, the process sends
an inquiry message to find a more superior
rule than the temporary decided rule.

If the above does not occur, the following happens.

The collected state transition segments are syn-Figure 17: Synthesis of state transition segments
In the synthesized protocol specification, the rulecandidates are screened as communication progresses,
and then a rule to be applied is determined. Oncea rule is determined to be applied at a process, theprocess sends response messages indicating the determined rule to the visited processes. There are two
types of response messages: a message indicating arule and no rule to be applied. A process that receives
a response message changes to the state designated by
the state transition segment corresponding to the determined rule. A process that receives a no rule message returns to the state prior to receiving the inquiry

message.

The above protocol synthesis algorithm is implemented as a communications software generation sys-82

. We have implemented some services on a PBX
by using automatic generated software.

$\mathrm{t}\mathrm{e}\mathrm{m}$$\mathrm{r}1)$$[eggA]\underline{\mathrm{s}\mathrm{t}\mathrm{a}\mathrm{r}\mathrm{t}}[eggB]$

idle

7

idle

ExampleWe explain an example of process specification generation. Figure 18 expresses a service specification. In
this service we need two terminals “data sender terminal” and “data receiver terminal”. Data sender terminal starts data transmission by an event “start” whenboth the sender and the receiver which is specified by“start” are in the state “idle”. The sender can always
stop sending data by an event “stop”. The receiver
can always request the sender to pause sending databy an event pause and to resume to sending data by
an event “resume”. Figure 19 shows a global statetransition diagram for this data sending protocol withpause function.
rule 1) idle (A) , idle (B) start:, receiving
sending.
, receiving
rule 2) sending
stop (A):idle (A) , idle (B).
, sendingrule 3) receiving
pause (A):, -wait-wait.
,
rule 4) -wait
itresume (A):,receivingsending$(\mathrm{A},\mathrm{B})$$(\mathrm{A},\mathrm{B})$$(\mathrm{A},\mathrm{B})$$(\mathrm{A},\mathrm{B})$$\mathrm{r}3)$

Figure 20: Graph representation of STR description
for data sending protocol$(\mathrm{B},\mathrm{A})$$(\mathrm{A},\mathrm{B})$$\mathrm{r}$$[eggB] \mathrm{i}\mathrm{d}\mathrm{l}\mathrm{e}$$(\mathrm{B},\mathrm{A})$$(\mathrm{A},\mathrm{B})$$\mathrm{r}$$\mathrm{r}2)$$(\mathrm{B},\mathrm{A})$$\mathrm{s}$$(\mathrm{B},\mathrm{A})$$\mathrm{s}-\mathrm{w}\dot{\mathrm{a}}$$(\mathrm{B},\mathrm{A})$$(\mathrm{A},\mathrm{B})$$(\mathrm{B},\mathrm{A})$.

Figure 18: STR description for data sending protocol

In this example each rule makes a rule overlappingtree. Using this graph representation and the rule
overlapping trees, we can get state transition segments
which are parts of the objective protocol entity specification. Figure 21 shows state transition segments
for the STR rules in Fig. 18. The messages used ininter-process communication are generated from theprovisional communication paths.
Figure 22 shows a protocol entity specification synthesized from state transition segments in Fig. 21. In
Fig. 22 the messages “ ”, “ ”, “ ”, “ ” represent request message, the messages “ ”, “ ”, “ ”,“”
response message. In this specification actions tosend or receive”norule” are omitted. “Norule” is a special response message to indicate there is no rule to be
applied. In the generated protocol entity specification,
when the protocol entity receives an unexpected request message, the protocol entity is assumed to send
the message “norule” to the sender of the request mes$\mathrm{m}1$$\mathrm{m}2$$\mathrm{m}3$$\mathrm{r}1$$\mathrm{m}4$$\mathrm{r}2$$\mathrm{r}3$$\mathrm{r}4$

sage.

8
Figure 19: Global state transition diagram for data
sending protocol with pause function
We show the graph representation for the service
specification in Fig. 18.

Conclusion

A protocol synthesis method is proposed by representing communications service specifications by aset of graph rewriting rules. The synthesized protocol
implements a distributed algorithm that finds and re-83

Figure 21: State transition segments for data communication protocol

Figure 22: Protocol entity specification for data communication protocol

References
places a subgraph isomorphic to an initial rule graphin a system graph with the next graph. Isomorphic
subgraph detection is known as one of NP-complete
problems [17]; however, the generated protocol operates within a time practical for application becauseof the limited number of terminals usually associatedwith a communications service.
The proposed protocol synthesis method can beused to generate communications software from service specifications. This enables those who are notspecialists in communications systems to participate
in developing communications software.

Recrevised[1] CCITT,
ommendation Z.100, “CCITT Specification and
Description Language (SDL),” May 1992.
[2] T. Bolognesi and E. Brinksma, “Introduction to
the ISO Specification Language LOTOS,” $C_{om}-$put. Networks ISDN Syst., vol. 14, pp. 25-59,

1987.
[3] M. Faci, L. Logrippo, and B. Stepien, “Formal
Specification of Telephone Systems in LOTOS:
the Constraint-Oriented Style Approach,” $C_{om}-$put. Networks ISDN Syst., vol. 21, pp. 53-67,

1991.

Acknowledgments
We sincerely thank Dr. Kohei Habara, Chairmanof the Board of ATR Communication Systems Research Laboratories, for his guidance and encouragement in this research. In addition to Dr. Nobuyoshi
Terashima, President of ATR Telecommunication System Research Laboratories, we also wish to thank ourcolleagues for their helpful discussions.

[4] L. Drayton, A. Chetwynd, and G. Blair, “Introduction to LOTOS through a worked example,”
Comput. Commun., vol. 15, no. 2, pp. 70-85,
Mar. 1992.
[5] E. J. Cameron, D. M. Cohen, T. M. Guithner,
W. M. Keese Jr., L. A. Ness, C. Norman, and H.
N. Srinidhi, “The L.O Language and Environmentfor Protocol Simulation and Prototyping,” IEEE

84

Trans. on Comput., vol. 40, no. 4, pp. 562-571,
Apr. 1991.
[6] J. J. P. Tsai, T. Weigert, and H.-C. Jang, “A Hybrid Knowledge Representation as a Basis of Requirement Specification and Specification Analysis,” IEEE Trans. on Software Eng., vol. 18, no.
12, pp. 1076- 1100, Dec. 1992.
[7] C. Dendorfer and R. Weber, “From Service Specification to Protocol Entity Implementation-An
Exercise in Formal Protocol Development,” Proc.
IFIP Twelfth Int. Symp. Protocol Specification,
Testing, Verification, pp. 163-177, 1992.
[8] G. v. Bochmann and R. Gotzhein, “Deriving
Protocol Specifications from Service Specifications,” Communications, Architectures
Protocols, Proc. ACM SIGCOMM ’(Vermont,
USA), pp. 136-145, Aug. 1986.
$\xi j$$\mathit{8}\theta$[9] R. Gotzhein and G. v. Bochmann, “Deriving
Protocol Specifications from Service Specifications Including Parameters,” ACM Rans. $C_{om}-$put. Systems, vol. 8, no. 4, pp. 255-283, Nov.
1990.
[10] P. M. Chu and M. T. Liu, “Synthesizing Protocol Specifications from Service Specification in
the FSM Model,” in Proc. Comput. Networking
Symp., pp. 505-512, Apr. 1988.
[11] K. Saleh and R. L. Probert, “A Service-Based
Method for the Synthesis of Communications
Protocols,” Int. J. Mini and Microcomput. Special Issue on Distributed Systems, vol. 12, no. 3,
pp. 197-103, 1990.
[12] Y. Kakuda, M. Nakamura, and T. Kikuno,“Automated Synthesis of Protocol Specifications
from Service Specifications with Parallelly Executable Multiple Primitives,” IEICE Trans. Fundamentals, vol. E77-A, no. 10, Oct. 1994.

[13] Y. Hirakawa and T. Takenaka, “Telecommunication Service Description Using State Transition
Rules,” Proc. Sixth Int. Workshop on Software
Specification and Design (Como, Italy), pp. 140147, Oct. 1991.
[14] K. Kawata, A. Takura, and T. Ohta, “On a Communication Software Generation Method from
Communication Service Specifications Describedby a Declarative Language,” Proc. Fifth International Conference on Computing and Information(Sudbury, Canada), pp. 116-122, May 1993.
[15] A. Takura, K. Kawata, T. Ohta, and N.
Terashima, “Communication Software Generation Based on Two-Layered Specifications andExecution Environment,” IEEE GLOBECOM’93(Houston, Texas), pp. 362-368, Dec. 1993.

[16] M. T. Liu, “Protocol Engineering,” Advances in
Computers, vol. 29, Academic Press, 1989.
[17] M. R. Garey and D. S. Johnson, Computers
and Intractability, A Guide to the Theory of$NP$ -Completeness. NY: W. H. Freeman and Co.,

1979.