LOTOSによる分散システムの全体記述と各ノードの動作記述 : 等価性と変換アルゴリズムについて(理論計算機科学とその周辺)

理論計算機科学とその周辺 研究集会 1992.1.29-31 LOTOSによる分散システムの全体記述と各ノードの 動作記述

-

等価性と変換アルゴリズムについて -東野輝夫, 安本慶一, 谷口健一 大阪大学基礎工学部情報工学科

Service Specification

and

Protocol Specifications in

LOTOS

-

Equivalence and Synthesis

-Teruo Higashino, KeiichiYasumoto andKenichi Taniguchi

Department of Information andComputer Sciences

Osaka University, Osaka560Japan

Abstract

LOTOS is a language developed within ISO for the

formal description of communication protocoIs and

distributed systems. In LOTOS, requirements for a

distributedsystemarecalleda“service specification“. Each

node exchangessynchronization messages to ensure the

temporalordering for theexecution ofeventsinaservice

specification. Theactions of each node

are

described

as

a

“protocol specification“. In this paper, we introduce a

method to derive protocol specifications from a service

specificationwritten inaLOTOS based language. Inorder

toderive the protocolspecifications,wemakethe syntax treeofagivenservice specification and givesomeattributes

foreach node inthe tree. The protocolspecificationsare

derived automaticallybyevaluating theseattributes.The

derived protocol specifications satisfy the given service

specification.Wealso explainaLOTOS simulator forthe

execution ofderivedprotocolspecifications.

1. Introduction

LOTOS$(1- 4)$_{isalanguage developed withinISOfor the}

formal description of communication protocols and

distributedsystems. Recently,thespecificationsofmany

OSI protocols

are

described in LOTOS$(2,6)$

_.

Requirements for

a

distributed system

are

describedas a

”service$specification^{\prime\prime(7)}$

.

InLOTOS,service primitives of

each nodein adistributedsystem

are

called $events^{\prime 1}$,and

the temporal ordering of the execution of events are

described

as

aservicespecification. Onthe protocollevel,

several nodes cooperate to provide the required service.

They exchange synchronization messages to

ensure

the

temporal ordering of the execution ofevents through a

communication medium. In thecommunication medium,

we

assume

thatthere is

a

communication channel fromeach

node $i”$toanyothernode $j^{t\prime}$,and that thecommunication

channel is modeled

as

aFIFO queue whose capacity is

infinite. The actions of each node are described

as

a

“protocol specification“. That is,aprotocol specification of

anode specifiesthe temporalordering oftheexecutionof

both the events of the node and sending/receiving

interactions of synchronizationmessages.

Inorder to getprotocolspecifications satisfyingagiven

service specification, therearetwotechniques:(l)analysis

and (2)synthesis. Verification and testing are analysis

techniques. These techniques

are

usedfor detecting design

errors

such

as

deadlocks,unspecified receptions andso on.

Although

some

analysis techniqueshavebeen proposedto

determine whether givenprotocol specificationssatisfy a

service specification, usuallyit takes muchtimeto

ensure

that given protocol specifications satisfy a service

specification. Asatechmquetodesign distributedsystems,

it is desirable that the designerdescribes only aservice

specification and protocolspecificationscanbederived from

the service specification automatically. Some synthesis

techniques have been proposed$(8- 14)$

.

_{In thispaper, we}

will introduce a synthesis technique to derive protocol

specifications from

a

service specification written in a

LOTOS based language. This synthesis technique

uses

only service specifications and it does not require any

furtherinformation. The technique has been proposedin

Ref. (15)andextended in

_Ref:

(16-21). Thispapergivesa surveyfor this synthesis technlque.

Inorder to observe theexecution of LOTOSprograms,

some

LOTOS simulators (interpreters) have been

deveIoped. These simulators are used for simulating theexecution ofservicespecifications. In order

tosimulate theexecution ofprotocolspecifications,weneed

thefacility fortheexchangeof synchronizationmessagesin additionto theordinary facilities of LOTOS simulators. We

have developedaLOTOS simulator PROSPEX(PROtocol

SPecification EXecutor) for the execution of protocol

specifications(24). Supposethatthereare $N$nodes in a

distributedsystem. We

use

$N$ PROSPEX tosimulate $N$

protocolspecifications. That is, eachPROSPEX simulates

a protocol specification and exchanges synchronization

messageseach other.

InSection2,

we

introduceaLOTOS based language for describing service specifications. InSection3, amethod

for deriving protocol specifications from a service

specification is explained. Our LOTOS simulator

PROSPEX is introduced inSection4. 2. Service Specifications

2.1 LOTOS

In LOTOS,

a

distributed system is described

as

a

collectionofprocesses. A specialprocessistreated

as

the

mainprocess. Aprocessconsistsofabehavior expression

(asequenceof eventsandoperators)where

some

operators

define thetemporalordering of theexecution ofevents. Let

$P$ and $B$ be a process and a behavior expression,

respectively. Aprocess definition is describedas $P:=B”$.

Iftheprocess$P$isinvoked,thentheeventsinthebehavior

expression $B$ areexecuted. The following operatorsare usedin behavior expressions.

(1)Thesequentialexecutionofsimpleinteractions“;“

A behavior expression $|\prime a$ ; $B’$ represents that the

behaviorexpression $B”$is executable after theevent $a”$is

executed.

(2)Non-deterministic choice of alternatives $[]’$

Abehavior expression $B_{1}$ $[]$ $B_{2’’}$ represents thatonly

one

ofthebehavior expressions $B\iota’’$and $B2”$isexecuted.

If

an

eventin $B_{1’’}$isexecuted,thenonlythe eventsin $\prime B]’$

are

executableandthe eventsin $B2’$

are

notexecuted.

(3)Independent parallelism $111”$

Abehavior expression $B_{1}111B_{2’’}$represents thatboth

behavior expressions $B_{1^{1\prime}}$ and $B2’$ are executable in parallel. The events in $B_{1}$ and $\uparrow\prime B_{2}$“ are executed

(4)Dependent parallelism withrendezvousinteractions“Il”

A behavior expression $B_{1}\downarrow[g1,..,g_{n}]1B_{2^{t\prime}}$ represents that both behavior expressions $||B_{1}$ ‘ and $B_{2’’}$ are

executable in parallel. The events in $B_{1}$ and $B2”$

belongingto $\{g1,..,g_{n}\}$ mustbe executed as rendezvous

interactions. If alleventsin $B1”$and $B_{2’’}$

are

contained in

$\{g\iota\cdot.,g_{n}\}$, then$|\prime B_{1}\downarrow[g1,..,g_{n}]1B_{2^{\prime 1}}$ maybedescribed

as

$\prime\prime B_{1}$ I$B_{2’’}$

.

(5)Sequentialcomposition $>>’’$

A behavior expression $B_{1}>>B2’’$represents that the

behavior expression $B_{2’’}$is executable aftertheexecution

of thebehavior expression $B1”$isfinished successfully.

(6)Disablingoperator“$[>’’$

Disablingoperator$”[>’’$ represents theinterruption ofa

particular sequence of events by

a

disabling event. A behavior expression$|\prime B_{1}[>B2’’$representsthat thebehavior

expression $B\iota’’$ is executable until

an

event $|d’’$ of the

behavior expression $B2”$is executed. If $d”$isexecuted,

then only theeventsin $B2”$

are

executable.

As anotheroperator, there is thehiding operator(see

Ref. $(1,4))$

.

An algebraic language ACT ONE isused

torepresent thevalues and data structuresin LOTOS. A

sub-language ignoring the values and data structures in LOTOS is called”Basic LOTOS“.

2.2 Language to Describe Service Specif\ddagger cations The specification language used in

our

derivation algorithmis functionally equivalenttoBasicLOTOS, except

that the disabling operator and hiding operator

are

not

supported. The language is used todescribe bothservice

specifications and derived protocol specifications.

Suppose thataLOTOS program$L$consists of thetuple

$L=<P_{1},P_{2},..,P_{n}>ofn$ processes $P_{1},$$P_{2},\ldots,P_{n}$, and that

the firstprocess $P_{1}$ isthemainprocess. We define the

syntaxofeachprocessdefinition using the production rules

(1)$\sim(12)$ in Table 1. In Table 1,

“Process-def‘

is the

starting symbol.

“Proc-Id“

and ”Event Id“mustbe defined

as

identifiers using

some

terminal symbols. Thekeywords “process,$”:=”$and “endproc” and theoperators $>>^{\prime\prime\prime\prime}11’’$, $|111^{t\prime},$ $\prime\prime[]’$‘, “;“ and“exit“

are

treated

as

terminal symbols.

“Event-subset“

isaset

of”Event-Id”.

A

_{“Proc-Id”}

denotes

a process, which is written as an “Identifier”. An

“Event-Id“

maydenoteeither:

$- a,servic_{1}e_{\_{ode_{whereIdentifier’’denotestheservice}}^{rim,itiveinteraction:Itiswrittenas}}$

primitive itself and ffNode“ denotes the node

name

at

which the interactiontakes place. For example, $a^{2}$“

denotes the service primitive $|a’’$atthenode 2(here,we

assume

that each interaction takes place at only

one

node).

-

an

interaction of sending

message:

Itis written

as

si$(m)”$

which

means

the sending of themessage $|m’’$tothe node

$i_{;}’’$

-

an

interaction of receiving message : It is written as

$ri(m)”$which

means

thereceivingofthemessage $|m^{\prime 1}$ fromthe node $|i’’$

.

Interactionsofsending/receivingmessages

are

onlyusedin protocol specifications.

2.3 Example of Service Specif\ddagger cations

Letusconsider

an

example in Fig. 1. In Fig. 1, there

are

3 nodes. Suppose that the

user

wants to copy

some

elementsinafileof the node 1 into another file ofthenode

3, but the

reverse

order. At the node1,we

can

onlyexecute

read “_whichis

a

_{service primitive interaction reading}

a

elementfrom the file. Atthe node3,

we can

onlyexecute

$write^{3}$“_{which is}a serviceprimitive interaction writing

a

receivingelementinto the file. Thenode2has

a

stack. At

the node 2,

we can

execute either $tpush^{2}$“

or

_{$pop^{2}$“.}

$Push^{2}$“

inserts the last receiving element in the local stack.

$Pop^{2}$ “ extracts the _past pushed elementfrom the local

stack. Forsimplicity oftheexplanation,wedo notconsider

thecontentsoftheelements. Aservice specificationofthis

exampleis writtenasfollowsusingthe production rulesin

Table1

:

$L=<A>$

process$A:=$($read^{1}$ ;$push^{2}$;$A>>pop^{2}$_;$write^{3}$_;exit)

$[]$read ;$wri\ddagger e^{3}$; exitendproc

3. Derivation of Protocol Specifications

In this section, we will explain a method for the

derivation of protocol specifications. The derivation algorithm of thispaperistheextended version of those in Ref. $(15,18)$

.

For

more

complex service specifications containingthedisablingoperatoranddata parameters,see thederivation algorithms in Ref.$(19,20)$

.

3.1

Example of Protocol Specifications

First,wewillgive

an

exampleof protocolspecifications.

Fortheservice specification$L$inSection2.3,wederivethe

following protocol specifications $L_{1},$$L_{2}$ and

L3.

Here,

some

_int.egers

such

as

8, 14 and 17

are

used

as

the

synchronuzationmessages.

Node1:

$L_{1}=<A>$

process$A;=read^{1};s2(14);r2(17)$_{; A}

$[]$$read^{1_{;s_{3}}}(35);s_{2(8);}$exit endproc

Node2:

$L_{2}=<A>$

process$A:=(r1(14);push^{2};$ ($s](17)$;exit Ill$s3(17)$;exit)

$>>A>>r3(11);pop^{2};s3(25)$_;exit) $[]$$r1(8)$; exit endproc

Node3:

$L_{3}=<A>$

process$A:=$($r_{2(]7);A}>>s2(11);r2(25);write^{3}$;exit)

$[]$$r1(35);write^{3}$; exit endproc

Fig.2represents

an

executionprocessoftheseprotocol specifications. The dotted lines in Fig. 2 denote the

exchange of synchronization

messages.

Fig. 2: An Execution Process of Protocol Specifications

Table 1: Syntax of Specification Language and Attribute Evaluation Rules

3.2 Principles for Deriving Protocol Specifications

Inthissection,

we

willexplaintheprinciples for deriving

protocolspecifications.Thebasicideaofthederivationisto

use

thenotion

_{of”projection“:}

That is,first,the events ofa

node $p”$

are

selectedfromagiven service specification,and

thenthesending/receivinginteractions of synchronization

messagesbetween the node $p”$and other nodes

are

added.

3.2.1 Attributes

The information concerning the exchange of synchronization messages is implicitly defined in each

service specification. This information is found by

assigning

some

attributestothenonterminal symbols ofthe

$s$yntaxtreeof the service specification. See Ref. (26) for

details of attribute grammars. Inthis paper,

we use

the

following three attributes (here, exp(x) represents the

behavior expression which is derived from the nonterminal

symbol $x”$).

SP(x):Thesetofnodes where thefirsteventsofexp(x)are

executed. It is called Starting Places ofthe

nonterminal symbol $x^{\mathfrak{l}\prime}$

.

EP(x):Thesetofnodeswhere the lasteventsofexp(x)are

executed. Itis called Ending Places of $x”$

.

AP(x):_{The set}of all nodeswhere theeventsofexp(x)are

executed. Itis called All Places of $x^{1\prime}$

.

Theseattributesarecalculated

as

thesynthesizedattributes usingtheattribute evaluationrulesin Table 1. The syntax tree for the process A described in Section 2.3 and the

attributes for

some

nonterminal symbols ofthe tree are

described in Fig. 3. Although theparameter $x^{\prime 1}$ of the

attributesSP(x),EP(x)andAP(x)_{is a}nonterminal symbol,

we

may

use

exp(x)instead of$|\prime x’’$

.

Thatis,

we

may

use

$SP(\exp(x))$instead ofSP(x)if thereisnoconfusion.

WegivetheattributesSP(x), EP(x)andAP(x)notonly

for the nonterminal symbols but also for the leaves

correspondingto eventidentifiers andprocessidentifiers. If

“Event-Id“

is $Identifier^{Node’’}$, then we define

SP(Event Id)$=EP(Event_{-}Id)=AP(Event_{-}Id)=$_{Node}. The attributes corresponding to

process

identifiers are

treated

as

variables. Weequatethevariables of suchaleaf

node,forinstance$A$,withthe valuesobtained by synthesis

for therootnode $Process_{-}def^{1}$correspondingtothe

same

processidentifierA. If the equation“SP(A) $=SP(A)uX”$

holds, then”SP(A)$=X^{t\prime}$is obtained

as

the solution. For

the process A in Fig. 3, the attributeSP(A), EP(A) and

AP(A)

are

treated

as

variables. We find the equations

“SP(A) $=\{1\}’’$, “EP(A) $=EP(A)u\{3\}’’$ and “AP(A) $=$

AP(A) $\cup\{1,2,3\}’’$

.

Therefore,thesolutions

are

“SP(A)$=$

$\{1\}’’$, “EP(A) $=\{3\}’’$ and “AP(A) $=\{1,2,3\}’’$

.

These

attributes

are

used to deternine which nodes need to

synchronize theirevents.

3.2.2 Basic idea of Derivation

(1)The sequential execution“;”and $>>^{1\prime}$

For a behavior expression of the form $a^{i}$ ; _$B”$

, we

assume

thatthe node $i”$mustsend

some

synchronization

messages to the Starting Places of $B”$ after $a^{i}$“ is

executed, and that the nodes belonging to the Starting

Places of $B”$mustreceivethesesynchronizationmessages

beforeanyeventof $B”$isexecuted. Forexample, for the

behavior expression $a^{1}$ ; $b^{2}$ ; $c^{1}$ ; exit“,we derive the

following protocol specifications $(here, ’|m]’’$and $m2”$

representthe synchronizationmessages).

Node1:$a^{1}$;_$s2(ml)$; _{$12(m2);c^{1}$}; exit Node2: $rl(ml);b^{2};sl(m2)$;exit

process$A:=$($readl$ ; push2;$A>>pop2;write3;exit$) $[]$readl ; write3;exitendproc

Fig. 3: Syntax Tree of Process A and Attribute Evaluation

Forabehavior expression of the form $B1>>B2’’$ ,we assume that the nodesbelongingto theEnding Places of $|\prime B_{1}$

“

must send some synchronization messages to the Starting Places of $B_{2^{t\prime}}$ after the lastevent of $B_{1’’}$ is

executed, and that the nodes belonging to the Starting

Places of $B2^{tt}$ must receive these synchronization

messagesbeforeanyeventof $B_{2^{\dagger\prime}}$is executed.

(2)Non-deterministicchoiceof altematives$\uparrow|[]’’$

Supposethat thebehaviorexpression $a^{1}$ ;$b^{2}$;$c^{3}$;exit

$[]d^{1}$ ;$e^{3}$;exit“

is given. If thesynchronizationmessages

described in the above (1)

are

added to this behavior expression,then thefollowing protocol specifications

are

obtained.

Node1:$a^{1}$;_$s2(ml)$; exit

$[]$$d^{1};s3(m3)$;exit

Node2: $\text{ロ_{}exit}^{r1(m1);b^{2};s3(m2);}$exit

Node3: $r2(m2);c^{3}$_;exit

$[]$ $r1(m3);e^{3}$;exit

Thereisnoeventsintherightside of $[]”$ofthebehavior

expression forthenode2. Therefore,

_an

emptyalternative of the form $B$ $[]$ exit“ is obtained

as

the protocol

specificationof the node 2. If the right side of $[]”$ is

chosen at the node1 by executing theevent $d^{1\prime}’$,the node 2

cannot knowit. Then,

a

wrong temporalordering ofthe

executionofeventsmay

occur.

This problem

occurs

when

theAll Places for the behavior expressions of the both sides of“

$[]$“

are

different. Therefore,we

assume

thatthe node

executing the first event ofany alternative must send synchronization messages to all nodes of the choice expressions which donotparticipate in the alternative. For

the above behaviorexpression $a^{1}$;$b^{2}$;$c^{3}$;exit

$[]$$d^{1}$;$e^{3}$;

exit“,wederive the following protocol specifications.

Node 1:$a^{1}$;_{$s2(m_{1);}$} exit

$[]$$d^{1}$; $s3(m3);s2(m4)$;exit Node2: $rl(ml);b^{2};s3(m2)$;exit $[]$ $rl(m4);exit$ Node3: $r2(m2);c^{3}$_;exit $[]$ $r1(m_{3);e^{3};exit}$

Here, $m4”$is the synchronizationmessagestoinformthat

theright side$of”[]”$ischosen.

(3)Process invocation

LetusconsidertheprocessAdescribed in Section2.3.

SincetheprocessAmaybe invoked recursively, it defines

$write^{3})^{n}$for

some

$n\geq 0$

.

If theprocessAisinvoked and the left side of choice operator $t’[]”$ is chosen, then a new

instance of$A$,say$A’$,is activated. Again,if the$left\cdot side$of

“_$[]$“ _{is chosen, then another instance of $A$,} say _$A”$

, is activated. Supposenowthat the rightsideof“

$[]$”ischosen

for thisnewinstance$A^{t}’$,then theprocess$A^{tt}$willterminate

with theexecution ofthesequence read; $write^{3}$_{; exit“.}

After$A^{t}$’ terminates, thesequence $pop^{2};write^{3\prime\prime}$ will be

executed and$A’$willalso terminate. Then,the processA

willbereactivated,andthesequence $pop^{2};write^{3}$“_willbe

again executed(seeFig.2).

Itisnatural toassumethat all nodesina processshould

synchronize whenever theprocessis activated. Therefore,

forabehavior expression of the form $a^{i};P’’$, we

assume

thatafter $a^{i}$“ isexecuted, the node $i^{t\prime}$

must send

some

synchronizationmessagestotheAllPlacesof $\uparrow P^{\prime 1}$

.

In the

protocolspecificationsdescribed inSection3.1, the node2

sends synchronizationmessages to thenodes 1 and3after

$notbeIo^{1\prime}ngtheAllPlacesofP,thentheprocessi’d’en^{1}tifer\prime\prime push^{2}isexecuted(seeFig_{f\prime}.2_{t\prime}).Here,ifanodep’do_{1}es$

$P”$ is replaced by “exit” in the derived protocol

specification for the node $p”(^{1}exit^{\dagger\prime}$ is an event

representingthesuccessfulterminationofa process,and it has

no

observationaleffects).

3.2.3 Restrictions for Derivation

In this paper, we treat only the service specifications

satisfyingthefollowing restrictions.

[Restrictions]

(R1) Foreachbehavior expression oftheform $B1$ $[]$$B_{2^{\prime\dagger}}$,

all starting interactions of $\dagger\prime B]^{t\prime}$ and all starting

interactions of $B_{2’’}$mustbe associated with the

same

node $q”$

.

That is,_{$SP(B])=SP(B1)=\{q\}$} must hold.

(R2) Foreachbehavior expressionof the form $B_{1}$ $[]$$B2”$,

thesetof Ending Places of $B_{1}$“and$|\prime B_{2’’}$mustbethe

same.

(R3) For each behavior expression of the form $B_{1}$III$B2”$

or $B$_] $1[g],..,g_{n}]1B_{2’’},$$B_{1}$ and$B2$must not invoke

the

same

process. Thatis,ifaprocess$P$is invoked in

$B_{1}$,then theprocess$P$mustnotbeinvokedin$B_{2}$

.

Restriction Rl simplifies the decision of which

altemative should be selected. Restriction R2andR3

are

introduced in order to simplify the derivation algorithm described in Section3.3. Forexample, ifR3does nothold,

thenthe

same

processes$P$maybe invoked in paralleland

thesame events$a^{i}$in_$P$may be executedsimultaneously.

Forsuchacase, thesynchronizationmessagessentafterthe

events $a^{i}$

are

executed must be different. This lets the derivationalgorithm

more

complex.

3.3 A Derivation Algorithm

Inthissection,

we

propose aderivation algorithm. The

algorithmisexecuted

as

follows:

Step 1: Constmctthe syntax treeTree$(p_{k})$of eachprocess

definition $p_{k};=B’’$inagiven service specification

$L=<P],P_{2},\ldots,P_{n}>$ using the production rules in

Table 1.

Step2:Calculate theattributesSP,EP and APateach node of thetreesTree$(P_{1}),$$Tree(p_{2})$and Tree$(p_{n})$using

theattribute evaluation rules in Table 1.

Step3:Foreach node $p^{1\prime}$in thedistributed system,using

$whicharedefnedinTab1es2and3,ca1cu1a\iota e^{T_{t}}\iota heattributee_{1}va1uationru1efortheattribute_{f_{e}}’’$

attribute $T_{P}$ ateach node ofthetrees Tree$(P_{1})$,

Tree$(p_{2})$and Tree$(p_{n})$.

Let Pspec$(P_{k},p)$denote the valueoftheattribute$T_{p}$atthe

rootnodeofTree$(p_{k})$

.

Then,the protocolspecification $L_{P’’}$

for

a

node $p’$isdefined

as

follows:

$L_{P}=<Pspec(P_{1},p),Pspec(P_{2},p),..,Pspec(P_{n},p)>$

Since the attributes SP, EP, AP and $T_{p}$

are

all the

synthesized attributes, the values of the attributes are

calculated from the leaf nodes to the root node. The

attribute$T_{P}$in Step3 isdefinedbasedonthe ideadescribed

Nod伽1–

in Section 3.2.2. Forexample, theattributeevaluationrule

(9) in Table 2 represents a derivation algorithm for

expressions of the form $|a^{i}$ ; _$B”$

.

The function

$Synch_{-}Left_{p}$ represents that ifthe node $p”$ belongs to

$EP(a^{]})$_,thatis,_{if $p=i”$}holds, _{then the}node $p”$must send

some

synchronizationmessagestotheallnodesbelonging

to SP(B) (see Table 3). The function $Synch_{-}Right_{P}$

represents that ifthe node $\dagger P’$ belongs to SP(B), thenlt

mustreceive the synchronization message from thenode $i”$

(seeTable3).

In general, thedifferent synchronizationmessagesmust

be usedforthedifferentsynchronizations. Forexample,in

theprotocol specificationsinSection3.1,different integers

such as 8, 14, and 17

are

used as the synchronization

messages. Wemaysaythatthesynchronization isdefined

between the nonterminal symbolsinthe syntax tree for each

process definition of a given service specification.

Therefore, we give the node number (integer) $N(e)^{\prime I}$ to

eachnode $e”$ofthe syntaxtree,and

use

the nodenumbers

as thesynchronizationmessages (seeTable3): By using

theabove derivation algorithm,the protocol specificationsin Section 3.1 arederived from the service specification in Section 2.3. The node numbersin Fig. 3 areusedas the

synchronizationmessagesfor this example.

We have developed the program which derives the

protocol specifications from a given service

specification(20). By using this program, the protocol specificationsarederived automatically.

4. Simulator for Execution of Protocol Specif\ddagger cations

Inordertoobserve theexecution processesofLOTOS

programs, some LOTOS simulators have been

developed$(4,22- 24)$

_.

_{These simulators}

_can

_{simulate the} execution of service specificationswritten in LOTOS. Our LOTOS simulator, PROSPEX, can also simulate the

execution of protocol specifications. If$N$ protocol

specifications

are

given, then $N$ PROSPEX

are

used to

simulate them in parallel. We use each PROSPEX interactively. PROSPEX readsabehavior expression $B”$

written in LOTOSandshowswhich events areexecutable for $B^{\prime 1}$

.

The

user

chooses

one

executableevent $e”$ from

thecandidates whichPROSPEX shows.Then,PROSPEX

executes the event $e^{\prime 1}$ and calculates which events

are

executableafter $|e’’$isexecuted. Thesimulation isdoneby

repeating these operations. In PROSPEX, the

sending/receivinginteractions

can

be executedautomatically

withoutinteractionsfromtheuser.

NodQl$\prod$

(a) (b)

PROSPEX is executed

on

UNIX workstations,andit

shows theseexecutionprocessesgraphicallyonX-window.

For example,supposethatthe protocol specification$L_{1}$in

Section 3.1 is given. PROSPEX draws the syntaxtree of thebehavior expression of the process $|A’’$_(seeFig.$4(a)$₎

onX-window.Eachleafcorresponds toeitheranevent,an

sending/receiving interaction

or a

process. The dotted

rectanglescorresponds toexecutableevents. In Fig.4(a),

two events read “_{of the bothsides of the choiceoperator}

“_$[]$“

are

_{executable.lfthe}user_{cricks read} “

ofthe left side

of $[]”$,then the eventisexecuted and the syntax treein Fig.

4(a)isreplaced by thatin Fig.4(b). Thisshows that the

event $read^{11}$is executed and

a

newbehavior expression,

say$B’$,is obtained. For$B’$,thesending interaction$s2(14)$

andreceiving interaction$r_{2(17)}$ayeexecutedautomatically

without interactions from the user. Then, the behavior expression$B’$ is replaced bythe processA. Since some

events in the process A

are

executable, the node

corresponding to Aisreplaced by the syntaxtree ofthe

behavior expression of A automatically. The replaced

syntaxtreeisthe

same as

thatin Fig.4(a).Even if thesize

of

a

syntax tree becomes large, PROSPEX calculates a

suitable size for drawingthe treeonthegiven windowand

drawsit.

5. Conclusion

In this paper, a derivation algorithm of protocol specificationsfrom

a

service specification is introduced.In

general,theprotocol specifications derived fromaservice specification

are

notsimple

even

if

a very

simpleservice

specification such

as

theexampledescribed in Section2.3is given. Therefore,

our

approach to derive protocol

specifications from

a

service specification is a good

approach to design distributed systems. For service

specifications written in Full LOTOS, the derivation

algorithmin Ref. (20)is useful. Theformal proofofthe

correctnessof the derivation algorithm isafuture work.

References

(1) ISO: “Information Processing System-Open Systems Interconnection -LOTOS- A Formal Description Technique based

on

the Temporal Ordering of Observational$Behaviour^{\prime 1}$,IS8807,1989.

(2) P. H. J.

van

Eijk, C.A. Vissers and M. Diaz : “The Formal Description TechniqueLOTOS”,NonhHolland,

1989.

(3) T. BolognesiandE. Brinskma: “Inrroductionto theISO Specification LanguageLOTOS”, ComputerNetworks

and ISDN Systems, Vol.14,No. 1,pp25-59, 1987.

(4) K.Takahashi,H. Kaminaga and N. Shiratori: ‘LOTOS

Features with Survey of Their Support Processing

Systems”, J. IPS of Japan, Vol.31, No. 1, pp.35-46,

1990(in Japanese).

(5) ISO: ”Information Processing System-Open Systems Interconnection - Basic Reference Model”, IS 7498,

1984.

(6) K. Ohmaki and K.$Futatugi;\prime\prime Early$Experience witha

Formal Description Technique : LOTOS“, J. IPS of

Japan, Vol. 31, No. 10, pp.1400-1413, 1990 (in

Japanese).

(7) C. Vissers and L. Logrippo

:

“The Importance of the Concept of Service in the Design of Data

CommunicationsProtocols”, Proceedings ofthe Fifth

IFIPWorkshop

on

Protocol Specification, Verification

and Testing,NorthHolland,pp.3-17, 1985.

(8) R.Probert and K. Saleh: “Synthesis of Communication Protocols

:

Survey and Assessment“, IEEE Trans. Comput., Vol. 40,No. 4,pp.468-476, 1991.

(9) P. Zafiropulo, C.H. West,H. Rudin,D.D.Cowan and

D. Brand

:

$|Towards$ _{Analyzing and Synthesizing}

Protocols“, IEEE Trans. Commun., $Vol.\cdot$COM-28,

No.4, pp.651-661, 1980.

(10) C.V. Ramamoorthy, S. T. Dong andY. Usuda : ‘An

Implementation ofanAutomated Protocol Synthesizer

(APS)and its Applicationtothe X.21 Protocol“, IEEE Trans. Software Eng., Vol. SE-II, No.9, pp. 886-908,

1985.

(11) C.V.,Ramamoorthy,Y.Yaw,R.Aggarwaland J.Song

: “Synthesis of Two-Party Error-Recoverable

Protocols , Proceedings of the ACM SIGCOMM 86

Symposium, pp.227-235, 1986.

(12) P.Merlinand G.

von

Bochmann:“OntheConstruction

of Submodule Specifications and Communication

Protocols”, ACM Trans. Program. Lang. & Syst.,

No.1, pp.1-25, 1983.

(13) M. Gouda and $Y_{;}$ Yu

:

“Synthesis of Communicating

FiniteStateMachines withGuaranteed Progress”, IEEE Trans. Commun., Vol. COM-32, No. 7, pp.779-788,

1984.

(14) P. M. Chu and M.T. Liu: ”Protocol Synthesis inaState TransitionModel“, Proceedings IEEE COMPSAC’88,

pp.505-512, 1988.

(15) G.vonBochmannand R. Gotzhein: “DerivingProtocol

SpecificationsfromService Specifications”, Proceedings of the ACM SIGCOMM 86 Symposium, Vermont,

USA,pp.148-156, 1986.

(16) T.Higashino, T.Kimoto, K.Taniguchiand M. Mori:

“Synthesis of Protocol Machines from Service Specification, Technical Report of IPS of Japan,

88-SF-26-5, 1988(inJapanese).

(17) R.GotzheinandG.vonBochmann:“DerivingProtocol

Specifications from Service Specifications Including

Parameters“, ACM Trans. Comput. Syst., Vol. 8, No.

4,pp.253-283, 1990.

(18) F. Khendek, G. von Bochmann and C. Kant : “New

resultsonderiving protocol specifications from services specifications, Proceedings of the ACM

SIGCOMM’89,pp.136-145, 1989.

(19) C. Kant, T. Higashino and $G_{;}$ von Bochmann :

“Deriving Protocol Specifications from Service Specifications Written in BasicLOTOS”,(submittedfor

publications).

(20) T. Higashino, R. Katou, K. Yasumoto and K.

Taniguchi: “Deriving Protocol Specifications from

Service Specification Written in LOTOS with Data

Parameters,Technical Report of IEICE$of$Japan,

IN91-111,1991 (inJapanese).

(21) R. Langerak

:

“Decomposition of Functionality; a

Correctness-Preserving LOTOS Transformation“,

Proceedings ofthe Tenth International IFIP WG 6. 1 Symposium

on

Protocol Specification, $Te$sting and

Verification,NorthHolland,pp.229-242, 1990.

(22) J. Tretmans

:

“Hippo

:

A LOTOS Simulator“, The Fornal Description TechniqueLOTOS,North-Holland,

pp.391-396, 1989.

(23) R. Guillemot, M. Haj-Hussein and L. Logrippo :

“Executing Large LOTOS Specifications”, Proceedings oftheEighthInternational IFIPWG 6.1 Symposiumon

Protocol Specification, Testing andVerification,North

Holland, pp.399-410, 1988.

(24) K. Yasumoto, T. Higashino and K. Taniguchi :

“Execution of Protocol Specifications Written in

$LOTOS^{\prime\dagger}$,Technical Report of IEICE of Japan,

IN91-112,1991 (inJapanese).

(25) H. Ehrig and B. Mahr : “Fundamentals of Algebraic

Specification 1”, EATCS Monographs onTheorelical

ComputerScience,Vol. 6,Springer-Verlag, 1985. (26) A. Aho, R. Sethi and J. D. Ul[man : ttCompilers

Principles, Techniques and Tools”, Addison-Wesley,