Deriving Self-Stabilizing Protocols for Services Speci.ed in LOTOS 
Monika Kapus-Kolar Jožef Stefan Institute, POB 3000, SI-1001 Ljubljana, Slovenia monika.kapus-kolar@ijs.si 
Keywords: distributed service implementation, automated protocol derivation, LOTOS 
Received: September 6, 2002 

A transformation is proposed which, given a speci.cation of the required external behaviour of a distributed server and a partitioning of the speci.ed service actions among the server components, derives a behaviour of individual components implementing the service. The adopted speci.cation language is close to Ba­sic LOTOS. Unlike in other protocol derivation algorithms based on LOTOS-like languages, distributed con.icts in the given service are allowed, and resolved by self-stabilization of the derived protocol. 
1 Introduction 
In top-down distributed systems design, one of the most dif.cult transformations is decomposition of a process into a set of co-operating subprocesses. Such a transformation is considered correct if it preserves, to the required degree, those actions of the process which are considered essential. Such actions are often referred to as the service that the pro­cess offers to its environment, i.e. the process is observed in the role of a server. 
A service consists of atomic service actions, of which the most important are service primitives, i.e. atomic interac­tions between the server and its users, executed in service access points. In addition, one might decide to introduce some hidden service actions, to represent various impor­tant events within the server. 
When decomposing a server, the .rst step is to decide on its internal architecture. It can be represented as a set of server components (e.g. one component per service access point), with channels for their communication. We shall assume that all components are on the same hierarchical level, for a multi-level architecture can always be obtained by gradual decomposition. 
The next step is to assign individual service actions to individual server components, paying attention to the loca­tion and capability of components. 
The .nal step is to specify details of the inter-compo­nent communication, i.e. to derive an ef.cient protocol implementing the service, where ef.ciency is measured in terms of the communication load. While the .rst two steps require creative decisions, protocol derivation can be au­tomated. Given a formal speci.cation of the architecture of a server, of its service and of its distribution, one can mechanically decide on the protocol exchanges necessary to implement the speci.ed distributed causal relations and choices between service actions. 
A protocol is typically much more complex than the ser­vice it implements. Besides, one usually does not care about the exact nature of an otherwise satisfactory proto­col. Therefore, algorithms for automated protocol deriva­tion are most welcome! They automate exactly that part of server decomposition which is the most dif.cult for a hu­man, requiring simultaneous reasoning about the numerous co-operating parties. 
Even if one decides for automated protocol derivation, it remains possible to strongly in.uence the resulting pro­tocol, by introducing dummy hidden service actions. For example, introducing a pair of consecutive service actions executed by two different server components introduces a protocol message from the .rst to the second component. Pre.xing each of a set of alternatives by a service action at a particular component makes the choice local to the component. In other words, instead of spending time on protocol design, one should rather concentrate on detailed service design, specifying all important dynamic decisions as explicit service actions [16]. By various allocations of the actions to server components, service implementations with various degrees of centralization are obtained. 
A prerequisite for automated protocol derivation is that the service is speci.ed in a formal language. It is desir­able that the derived behaviours of individual server com­ponents are speci.ed in the same language as the service, so that the same algorithm can be used for further decom­position. 
It is desirable that a protocol derivation algorithm is to a large extent compositional, so that it can cope with large service speci.cations, provided that they are well struc­tured. Moreover, a compositional algorithm re.ects the ser­vice structure in the derived protocol speci.cation, increas­ing the service designers’ con.dence into the automatically generated implementation. 
It is dif.cult to construct a general protocol derivation al­gorithm with high-quality results and low complexity. Typ­ical algorithms work on small classes of service speci.ca­tions. 
Protocol synthesis has been subject to intensive research since the middle eighties. An exhaustive survey can be found in [26], so we provide no systematic review of the existing methods and refer to them only where necessary for comparison with the proposed solutions. 

The protocol derivation transformation proposed in our paper is an enhancement of that in [10]. As in [10], we assume that a server consists of an arbitrary .xed num­ber of components exchanging the necessary protocol mes­sages asynchronously, over reliable, unbounded, initially empty .rst-in-.rst-out (FIFO) channels with a .nite, but unknown transit delay. The adopted speci.cation language is a syntactically simpli.ed sublanguage of LOTOS [7, 2], a standard process-algebraic language intended primarily for speci.cation of concurrent and reactive systems. Ser­vice primitives are not allowed to carry parameters, neither do we allow speci.cation of real-time constraints. How­ever, the principles for enhancing a basic protocol deriva­tion method to cope with data and real time are well known [11, 12, 23]. 
For a service containing distributed con.icts, a precise implementation takes care that they never cause divergence in service execution. Firstly one should try to make all con­.icts local to individual components, by inserting auxiliary hidden service actions, but that is acceptable only as long as no external service choice is undesirably converted into an internal server choice. For the remaining distributed con.icts, divergence prevention requires extensive inter-component communication [9, 20, 21]. Although even such protocols can be derived compositionally [17], the commu­nication costs they introduce are usually acceptable only if exact service implementation is crucial or during the pe­riods when server users compete strongly for the service. In a typical situation, the probability of a distributed con­.ict is so low that divergence should rather be resolved than prevented. 
In LOTOS, there are two process composition operators allowing speci.cation of service actions in distributed con­.ict, the operator of choice and the operator of disabling. In [10], only local choice is allowed. For disabling, the derived protocols are supposed to self-stabilize after diver­gence, but the proposed solution is not correct in the gen­eral case [15]. Besides, [10] has problems with implemen­tation of parallel composition [15]. In an unpublished re­sponse to [15], Bochmann and Higashino proposed some solutions for the problems, but have not integrated them into their protocol derivation algorithm and have not been able to specify the solution for disabling in LOTOS. 
We specify self-stabilization upon disabling purely in the adopted LOTOS-like language, and also suggest how to implement distributed choice. Further improvements over 
[10] are implementation solutions for processes with suc­cessful termination as a decisive event, for processes which might enter inaction without .rst declaring successful ter­mination, for combining terminating and non-terminating alternatives, for process disabling with multiple initiators, and for interaction hiding and renaming. The proposed so­lutions can be seen also as an improvement over [3], an­other algorithm for the purpose in which we have identi.ed a bug [15]. 
Name of the construct Syntax 
Speci.cation w ::= spec b where D endspec 
D ::= set of d 
Process de.nition d ::= p(x) is b | p is b 
Process name p ::= ProcIdenti.er 
Parameter name x ::= ParIdenti.er 
Behaviour b ::= 
Inaction stop 
Successful termination | . 
Sequential composition | b1 »b2 
Action pre.x | a; b2 
Choice | b1[]b2 
Parallel composition | b1|[G]|b2 
Disabling | b1[> b2 
Hiding | hide G in b1 endhide 
Renaming | ren R in b1 endren 
Process instantiation | p(v) | p 

G ::= set of g 
Interaction gate g ::= s | h 
Data value v ::= term of type n * 
Index n ::= 1 | 2 

R ::= set of r 
'
Gate renaming r ::= g/g 
Action a ::= i | s | h | ho 
Service primitive s ::= u c 
Service-primitive type u ::= PrimIdenti.er 
Server component c ::= CompIdenti.er 

cc n ccc
Auxiliary gate h ::= s , | r , | a, | bc, | t 
Data offer o ::= !v | ?v | ?x:v 

Table 1: The adopted speci.cation language 
The paper is organized as follows. Section 2 introduces the adopted speci.cation language and its service speci.­cation sublanguage, some building blocks for the derived protocol speci.cations, and the adopted protocol correct­ness criterion. Section 3 describes the adopted principles of protocol derivation. The derivation is guided by various service speci.cation attributes. In Section 4, we introduce rules for attribute evaluation and suggest how to obtain a well-formed service speci.cation. Section 5 comprises dis­cussion and conclusions. 


2 Preliminaries 
2.1 	Speci.cation language and its service speci.cation sublanguage 
The language employed, de.ned in Table 1 in a Backus­Naur-like form, is an abstract representation of some LO­TOS constructs, in the exclusive setting of the protocol derivation problem. Not shown in the table are parentheses for control of parsing, the syntax for sets, and shorthands. 
A b denotes a behaviour, i.e. a process exhibiting it, for instance a server as a whole, an individual server compo­nent, a service part or some other partial server behaviour. For a particular server, let C denote the universe of its com­ponents. 
spec . where D endspec = spec . where D endspec .|[G]|b = b|[G]|. = b a; . = a; . . »b = b». = b .; b = b hide G in . endhide = . ren R in . endren = . 
Table 2: Absorption rules for . 
stop denotes inaction of the speci.ed process. 
. denotes successful termination. 
In some cases, the protocol derivation mapping de.ned below introduces an . specifying execution of no actions. . is similar to ., because execution of no actions is successful by de.nition. With the help of the absorption rules in Ta­ble 2, it will be possible to make the derived speci.cations free of .. 
i denotes an anonymous internal action of the speci.ed process. Besides internal actions, processes execute inter­actions with their environment. Such an external action is primarily denoted by the interaction gate on which it oc­
c
curs. If it is a service primitive, it is speci.ed as a uand denotes a type u interaction between server component c and a service user. If it is an action on an auxiliary gate h, it might be associated with a data offer o, that has to match with the data offer of the process environment. The only data that our processes can handle are strings of zero or more elements 1 and/or 2. 
A component c can send messages to another compo­
'
nent c' over gate sc , while creceives them over gate rc, . 
c, c For speci.c purposes, c' will sometimes call the gate an 
c 
(accept), where n will be a partial context identi.er. If c' is unable to immediately handle a message received on gate rc, , it will store it into a FIFO buffer and subsequently 
c 
claim it on an internal gate bc. Gate t will always be an internal gate of a server component, serving for hidden in­teraction of its parts. 
A data offer "!v" denotes exactly the data value speci.ed by the term v. A data offer "?x : v" or "?v" denotes any data value which has a pre.x speci.ed by v. When the interaction occurs, one of the values legal for the data offer is selected, and if variable x is speci.ed, stored into it for future use. 
"b1 »b2" denotes a process .rst behaving as b1, and after its successful termination as b2, where . of b1 is interpreted in "b1 »b2" as i. "a; b2" is the special case of the sequential composition where b1 is an individual action, so that no i is needed for transfer of control to b2. 
"b1[]b2" denotes a process ready to behave as b1 or as b2. Sometimes we will use "[]" as a pre.x operator, where choice from an empty set of processes is equivalent to stop. 
"b1|[G]|b2" denotes parallel composition of processes b1 and b2, where G speci.es the degree and form of their syn­chronization. An action on a gate listed in G or a . can only be executed as a common action of the two processes, while the processes execute other actions independently. The usual shorthand for "|[]|" is "|||". Sometimes we will use "|||" as a pre.x operator, where parallel composition of an empty set of processes speci.es an .. 
Informatica 27 (2003) 57–73 59 
No. e 
(1) w::= spec b where D endspec 
(2) 
d ::= p is b 

(3) 
b ::= stop 

(4) 
b ::= . 

(5) 
b ::= b1 »b2 


(6) 
b ::= a; b2 

(7) 
b ::= b1|[S]|b2 

(8) 
b ::= b1[]b2 


(9) b ::= b1[> b2 
(10) 
b ::= hide S in b1 endhide 

(11) 
b ::= ren R in b1 endren 


(12) 
b ::= p 

(13) 
a ::= s | i S ::= set of s r ::= u2 c /uc 1 


Table 3: Service speci.cation sublanguage 
"b1[> b2 " denotes a process with behaviour b1 poten­tially disabled upon the start of process b2. While b1 is still active, the process might terminate by executing . in b1. 
"hide G in b1 endhide" denotes a process behaving as b1 with its actions on the gates listed in G hidden from its environment. For the environment, the hidden actions are equivalent to i. 
"ren R in b1 endren" denotes a process behaving as b1 with its visible gates (and thereby the actions on them) renamed as speci.ed in R, where in an r, the .rst and the second item respectively de.ne the new and the old name. 
Explicit processes can be de.ned and instantiated, possi­bly with an input parameter. In the original LOTOS syntax, explicit processes are de.ned on formal gates, that are asso­ciated with actual gates upon process instantiation. In our simpli.ed language, gate instantiation can be expressed as renaming of the gates on which a process is originally de­.ned applied to the particular process instance. 
A speci.cation w de.nes a behaviour b and the processes instantiated in it, except for the processes prede.ned in Section 2.2. If D is empty, "where D" may be omitted. If it is a service speci.cation (Table 3), then 1) any speci.ed action must be a service primitive or an i, 2) gate renam­ing is allowed only locally to individual server components, and 3) all the explicitly speci.ed processes must be without parameters. Some rows in Table 3 are numbered, so that the corresponding rows in some of the remaining tables can re­fer to them. In all our example service speci.cations, every i and every . is furnished with a superscript denoting the server component responsible for it. 
The relation used throughout the paper for judging equivalence of behaviours is observational equivalence "." [2], i.e. we are interested only into the external be­haviour of processes, that is in the actions which they make available for synchronization with their environment (all actions except i and actions transformed into i by hiding). 

2.2 	Some building blocks for protocol speci.cations 
The contribution of our paper lies in functions for generat­ing protocol speci.cations in the proposed language. These speci.cations will be based on some characteristic patterns, for generation of which we de.ne some auxiliary functions (Table 4). 
Sc(C, v) := |||c,.(C\{c})scc , !v Rc(C, v) := |||c,.(C\{c})rcc , !v Ec(C, C ' , v) := (if (c . C) then Sc(C ' , v) else . endif |||
if (c . C ' ) then Rc(C, v) else . endif) Pc(S) := {u c|(u c . S)}
'c 'c
Pc(R) := {(u /uc)|((u /uc) . R)} 
Table 4: Auxiliary speci.cation-generating functions 
Sc(C, v) generates a speci.cation of parallel sending of protocol message v from component c to each member of C other than c. Likewise, Rc(C, v) speci.es parallel receiving of v at c from each member of C other than c. 
'
Ec(C, C , v) speci.es exchange of message v in such 
'
a way that each component in C receives it from every component in C other than itself. 
Pc(S) and Pc(R) are projection functions. Pc(S) ex­tracts from S the service primitives belonging to compo­nent c, while Pc(R) extracts from R the renamings of such primitives. 
We also assume that there are three prede.ned processes. Processes "Loop" and "Loop(v)" execute an in.nite series of "g" or "g?v" actions, respectively. Shorthands for in­stantiation of the processes on a gate g for a pre.x v are "Loop(g)" and "Loop(g?v)", respectively. 
Process "FIFO(v)" is an unbounded FIFO buffer ready to store messages with pre.x "v" and to terminate when­ever empty. A shorthand for instantiaton of the process on an input gate g1 and an output gate g2 for a pre.x v is "FIFO(g1, g2, v)". To specify that a FIFO(g1, g2, v) should accept all kinds of messages, one sets v to an empty string, that we denote by .. Such are the buffers pairwise connecting server components. They constitute the com­munication medium, de.ned as 
Medium is |||c c, , rc, 
=c, FIFO(sc , .)
c 

2.3 	Protocol correctness criterion 
Given a service behaviour b, we derive a bc for each indi­vidual component c. The protocol must satisfy the mini­mal correctness criterion that every protocol message sent is also received. We further expect that in the absence of distributed con.icts, the server behaves towards its users precisely as required (see Table 5). Note that ". (b » .)" might also be suf.cient, because successful termination of a distributed server, as an act of multiple server compo­nents, does not qualify as one of the regular service actions, 
i.e. service actions assigned to individual components. 
If b contains distributed con.icts, precise service exe­cution is expected only for those server runs which do 
M. Kapus-Kolar 
(Service . b) . ((|C| > 1) . (Service . (b».))) where Service = hide G in (|||c.Cbc)|[G]|Medium 
endhide 
,
c c
G = .c c, , rc }
=c, {s 
Table 5: Precise service implementation 
not reveal any of the con.icts. When divergence in ser­vice execution occurs, the server should continue to sup­port only the direction of service execution with the highest pre-assigned priority, while the directions competing with it must be abandoned as quickly as possible. 
For a "b1[> b2", it is appropriate that b2 has a higher pri­ority than b1. We adopt this arrangement also for "b1[]b2". There are, however, two exceptions. If the server compo­nents responsible for the start of b2 manage to agree on successful termination of b1 before b2 starts, b2 must be abandoned. In the case of "b1[]b2", b2 must be abandoned already when the components manage to agree on the start of b1. 



3 Principles of protocol derivation 
3.1 	Service attributes and the concept of a well-formed service speci.cation 
When mapping a service speci.cation subexpression into its counterparts at individual server components, one refers to its various attributes. A subexpression attribute reveals some property of the subexpression itself or some property of the context in which it is embedded. Computation of service attributes is discussed in Section 4.1. 
There is always a dilemma whether to conceive a very general mapping, i.e. a mapping with very few restrictions on the attributes, or a simple mapping with a very restricted applicability. We take the following pragmatic approach. 
Above all, we try to avoid restrictions on the speci.ca­tion style (see [28] for a survey of the most typical styles) because, even if a service speci.cation can be restyled au­tomatically, the derived protocol speci.cation will re.ect the new style, and as such be hardly comprehensible to the designers of the original speci.cation. 
On the other hand, we rely without hesitation on restric­tions which can be met simply by introducing some addi­tional hidden service actions. Such insertion can always be automated and causes no restructuring of the service speci­.cation. Besides, there is usually more than one way to sat­isfy a restriction by action insertion. By choosing one way or another, it is possible to in.uence the derived protocol, 
i.e. its ef.ciency and the role of individual server compo­nents. Hence by relying strongly on such restrictions, we not only simplify the protocol derivation mapping, but also make space for protocol customization. 
A service speci.cation satisfying all the prescribed re­strictions is a well-formed speci.cation. We postpone sug­gestions for obtaining such a speci.cation to Section 4.2. 

3.2 	Compositional approach to service implementation 
When mapping a service speci.cation in a compositional way, we map each of its constituent process speci.cations, including the main service process. Mapping a speci.ca­tion of a process p, we map speci.cations b of the individ­ual parts of the behaviour speci.ed by its body. 
During service execution, each instantiation of such a p gives rise to a new instance of the behaviour speci.ed by such a b. Each such instance is an individual service part and, as such, expected to be implemented in an indepen­dent way. In other words, such an instance represents a special context, that .rst of all needs a dynamically unique identi.er. The identi.er can then be included in all proto­col messages belonging to the particular instance, to make its distributed implementation communication-closed. The simplest way to produce such an identi.er is to concate­nate (speci.ed by operator "·") z, the dynamically unique identi.er of the particular instance of p, and C I (b), the dy­namically unique context identi.er of b within the body of p [14]. 
Mapping a speci.cation of a process p onto a c results in a speci.cation of a local process p with a formal parameter "z". When the local process is instantiated, "z" propagates into its body the identi.er of the particular process instance, so that it can be used in the associated protocol messages. The main service process is instantiated only once, so its "z" can be assigned statically. For a dynamically created process instance, "z" is the identi.er of its instantiation. Those properties are re.ected in Table 6, more precisely described below. 
(1) 	Tc(w, z) := spec Termc(b, z) where {Tc(d)|(d . D)} endspec 
(2) Tc(d) := p(z) is Termc(b1, z) 
(12) T ' c(b, z) := p(z·C I (b)) 
Table 6: Mapping T for a service speci.cation and map­ping T' for process instantiation 
Tc(b, z) will be the basic function for mapping a service part b onto a component c within a context z. Sometimes the implementation of a b generated by mapping T will be enriched with some additional protocol messages report­ing its successful termination to server components not yet knowing it. The mapping which generates such enriched implementation will be called Termc(b, z). Mapping T of a structured b combines the mappings Term of its con­stituent parts. 
For a b, it might be that a c has no duties in its distributed implementation, i.e. that c is not a participating component of b (formally ¬P Cc(b), i.e. not a member of P C (b)). In such a case, Tc(b, z) will be . or stop, while in the case of P Cc(b), Tc(b, z) will more precisely be called T' c(b, z). 
In the following, let Term(b, z) denote a Term imple­mentation of b, i.e. all Termc(b, z) plus the protocol chan­nels. Likewise, T(b, z) denotes a T implementation. 
Informatica 27 (2003) 57–73 61 
In an environment of competing service parts, it is im­portant to have a simple characterization of all protocol messages belonging to a particular part b. In a T(b, z), such a message will carry either identi.er C I (b) or identi­.er C I (b ') of a subpart b ' of b. To indicate that messages of the second type also belong to b, C I (b ') will in all cases have C I (b) as a pre.x. In a Term(b, z), the addition­ally introduced messages will carry identi.er C I +(b). As T(b, z) is a part of Term(b, z), C I (b) will have C I +(b) as a pre.x. So it will be possible to specify readiness to receive any message belonging to a Term(b, z) simply by ?z·C I +(b) in the receptions. 
The basic building blocks of context identi.ers, hence also of protocol messages, are 1 and 2, because they refer typically to parts b1 and b2 of a b. That is, of course, not the only possible choice. By changing 2 to 0, for example, one could obtain pure binary identi.ers. In any case, it is important that the number of different messages on individ­ual channels is kept low, for message encodings can then be short. For that reason, messages (i.e. the context iden­ti.ers they contain) are re-used extensively, except where that could corrupt their dynamic uniqueness. 
Example 1 For the example service in Table 7, it is crucial that the implementations of the two concurrent instances of process Proc use different protocol messages. Likewise it is important that protocol messages are re-used, because Proc is instantiated an in.nite number of times. 
The reception buffers of the three components (see Sec­tion 3.9) are not shown in the example, to make the spec­i.cations more readable. The buffers are not crucial for deadlock prevention, anyhow. 


3.3 	Termination types 
For a b representing the entire service that is being imple­mented, it is evident that its successful termination (if any) must be implemented as . (or as its . equivalent) at each of the server components. In other words, each Termc(b, z) must be terminating, i.e. each c must be a terminating component of b for mapping Term, formally T C +(b), i.e. 
c 
c must be an element of T C +(b). If a b is not the last part of the service, T C +(b) is
c 
not mandatory. It is sometimes better to let Termc(b, z) .nish by stop instead, i.e. ¬T C +(b) [14]. Such in­
c 
action at c is later disrupted by activities of c outside Termc(b, z). If b never successfully terminates, formally ¬T M (b), ¬T C +(b) is the only option. 
c 
If T C +(b), one has to decide whether c should detect or 
c 
declare termination of b already within the Tc(b, z) part of Termc(b, z), i.e. whether T C +(b) should imply T Cc(b),
c 
i.e. that c is an element of T C (b). If T C +(b) but not 
c 
T Cc(b), formally RTc(b), c terminates Termc(b, z) upon receiving termination reports "z·C I +(b)" from all the end­ing components of T(b, z) [14] (see Table 8). Where the danger exists of such a report being received already within Tc(b, z), care is taken that it is different from any message referred to within Tc(b, z). Hence protocol Term(b, z) 

w = spec ren a ./A. , b. /B. , c ß /Cß in Proc endren ||| ren d./A. , e . /B. , fß /Cß in Proc endren where Proc is (((A.; ..)|||(B. ; .. ))»(Cß ; Proc)) endspec T.(w, .) . spec ren a ./A. in Proc(1) endren ||| ren d./A. in Proc(2) endren 
. .

where Proc(z) is (A.; sß !z; rß !z; Proc(z)) endspec Tß (w, .) . spec ren c ß/Cß in Proc(1) endren ||| ren fß/Cß in Proc(2) endren 
ßß ßß
where Proc(z) is (((r.!z; .)|||(r. !z; .))»Cß; ((s.!z; .)|||(s. !z; .)) »Proc(z)) endspec T. (w, .) . spec ren b. /B. in Proc(1) endren ||| ren e . /B. in Proc(2) endren where Proc(z) is (B. ; sß . !z; rß . !z; Proc(z)) endspec 
Table 7: An example of multiple process instantiation 
Tc(b, z) := if P Cc(b) then T ' c(b, z) else if T Cc(b) then . else stop endif endif Termc(b, z) := if T C c +(b) then if T Cc(b) then (Tc(b, z) if ECc(b) then »Sc((T C +(b) \ T C (b)), z ·C I +(b)) endif) else ((Tc(b, z)[> .)|||Rc(EC (b), z ·C I +(b))) endif else Tc(b, z) endif 
Table 8: Functions T and Term 
has two phases, namely protocol T(b, z) and exchange of termination reports. 
A c is an ending component of b for mapping T, for­mally E Cc(b), i.e. c is a member of E C (b), if it might be the last component to execute an action within T(b, z). If E Cc(b), c must, of course, declare termination already within Tc(b, z), i.e. ECc(b) by de.nition implies T Cc(b), and thereby T C +(b).
c 
In many cases, we are free to decide whether T C +(b)
c 
should imply T Cc(b) or not, but it is not always directly evident how our decision would in.uence the overall num­ber of the involved protocol messages. Therefore we fol­low the classical solution that T C +(b) should always im­
c 
ply T Cc(b) (i.e. ¬RTc(b)), except where that would lead to an erroneous service implementation (discussed in the operator-speci.c sections). If there are no such cases, map­ping Term systematically reduces to mapping T, i.e. there is a single mapping function, like in the earlier approaches [3, 10]. 
If ¬P Cc(b), T Cc(b) will always be equal to T C +(b),
c 
reducing Termc(b, z) to a mere . or stop (see function T in Table 8). Hence the components participating in the distributed implementation of a b remain those listed in P C (b), even if we enhance the mapping function from T to Term. 
For a protocol T(b, z), we de.ne that it successfully ter­minates when all Tc(b, z) with T Cc(b) successfully ter­minate. Likewise, successful termination of Term(b, z) requires successful termination of all Termc(b, z) with T C +(b). 


3.4 Implementation of inaction 
A stop has no participating component, so the .rst rule in Table 8 implies that every server component implements it as a stop. 

3.5 	Implementation of successful termination 
In some cases, it is crucial to have in mind that success­ful termination . is also a kind of an action. These are the cases where it is in a decisive position, like an initial . in a "b1[]b2" or the . of b1 or an initial . of b2 in a "b1[> b2 " [14]. So one selects, as convenient, for each . a server com­ponent responsible for its execution, its only participating component. Mapping T' for the component is a . (Table 9). 
(4) T ' c(b, z) := . 
Table 9: Mapping T' for successful termination 

3.6 	Implementation of hiding and renaming 
The only properties of actions within a service part b that in.uence protocol message exchange are their position within b and their assignment to server components. That is not changed by hiding or local renaming, so implemen­tation of those operations is trivial (Table 10). 
(10) 
T ' c(b, z) := hide Pc(S) in Termc(b1, z) endhide 

(11) 
T ' c(b, z) := ren Pc(R) in Termc(b1, z) endren 


Table 10: Mapping T' for hiding and renaming 

3.7 	Implementation of action pre.x 
To map an "a; b2" onto a participant c (Table 11), one .rst needs Pc(a), the projection of a. If c is not the executor of a, i.e. its only participant, the projection is empty. If a is a service primitive, its executor is evident from its identi.er. If it is an i, one selects its executor as convenient. 
If a component c might be the .rst to execute an ac­tion within Term(b2, z), it is a starting component of b2, formally S Cc(b2), i.e. c is a member of SC (b2). Such a c is responsible for preventing a premature start of 
(13) Pc(a) := if P Cc(a) then a else . endif 
(6) 	T ' c(b, z) := (Pc(a); Ec(P C (a), SC (b2), z ·C I (b)) »Termc(b2, z)) 
Table 11: Mapping T' for action pre.x 
Term(b2, z), i.e. it must not start Termc(b2, z) until it executes a or receives a report "z · C I (b)" on it. Hence protocol T(b, z) has three phases, namely execution of a, exchange of reports on a, and protocol Term(b2, z). 

3.8 	Implementation of sequential composition 
For a b speci.ed as "b1 » b2", we require that b1, at least sometimes, successfully terminates, because otherwise b2 would be irrelevant. 
Protocol T(b, z) (Table 12) has three phases, namely protocol Term(b1, z), exchange of reports "z ·C I (b)" on its termination, and protocol Term(b2, z). Where dan­ger exists that a message belonging to the second phase is received already within a Termc(b1, z), care is taken that it is different from any message referred to within Termc(b1, z). It is crucial that every c with duties within the second or the third phase terminates Termc(b1, z) in all the terminating runs of b1, i.e. that T C +(b1) is true. 
c 
(5) T ' c(b, z) := (Termc(b1, z) »Ec(EC +(b1), S C (b2), z ·C I (b)) »Termc(b2, z)) 
Table 12: Mapping T' for sequential composition 
As in the case of action pre.x, reports on termination of the .rst phase are sent to the starting components of b2, but now their senders are the ending components of Term(b1, z) [19]. A c is an ending component of b1 for mapping Term, formally EC +(b1), i.e. c is a member of 
c 
E C +(b1), if it might be the last component to execute an action within Term(b1, z). It is crucial that a terminat­ing b1 has at least one ending component, and that in ev­ery non-terminating run of such a b1, there is at least one ending component c not terminating Termc(b1, z), so that start of Term(b2, z) is prevented. 
We want the second phase (i.e. termination reporting) to completely isolate Term(b2, z) from Term(b1, z), so that protocol messages from Term(b1, z) and termina­tion reports may be re-used within Term(b2, z). That is particularly important for implementation of iteration and tail recursion, as in Example 2. To achieve the isolation, we take care that upon the start of Term(b2, z), compo­nents receiving within it no longer want to receive within Term(b1, z). 
Example 2 In Table 13, we implement a service consisting of two consecutive parts. It might happen that the .rst part does not terminate, but a premature start of the second part is nevertheless prevented. 
Informatica 27 (2003) 57–73 63 


3.9 	Implementation of parallel composition 
For a b speci.ed as "b1|[S]|b2", we assume that all actions speci.ed in b1 or b2, including ., are actually executable within b, i.e. that they are all relevant. 
Protocol T(b, z) (Table 14) consists basically of proto­cols Term(b1, z) and Term(b2, z) running in parallel and locally synchronized on service primitives from S. 
If there are any distributed con.icts in b1 and/or b2, for­mally AD(b), Term(b1, z) and/or Term(b2, z) are typ­ically imprecise implementations of b1 and b2, unable to synchronize properly on S. So if S is non-empty, AD(b) is forbidden. 
If S is empty, b1 and b2 are nevertheless synchronized on their successful termination (if any). If termination of b is subject to a distributed con.ict within b1 and/or b2, for­mally T D(b), negotiation of more than one component is required within Term(b1, z) and/or Term(b2, z). That is unacceptable, for such termination is a decisive termination (see below). So T D(b) is forbidden. 
For independent concurrent execution of Term(b1, z) and Term(b2, z), it should be suf.cient to take care that their protocol message spaces are disjoint [10]. Unfortu­nately, it turns out that on a shared channel, unprompt re­ception in one of the protocols might hinder reception in the other. In the case of a non-empty S, that might even lead to a deadlock [15]. 
Kant and Higashino suggested that each c could solve the problem by prompt reception of messages into a pool, for further consumption by Termc(b1, z) or Termc(b2, z). So in Table 14, we introduce for each part Termc(bn, z) 
'
for each channel from a c to c that is shared (formally S Hc,,c(b)), a FIFO buffer for incoming messages. Such a buffer is, unlike Termc(bn, z), always ready to receive from the channel on gate rc c, , thereby removing the pos­sibility of blocking. Termc(bn, z) can subsequently claim the received messages from the buffer on a hidden gate bc, . As demonstrated in the following example, such buffers might be necessary even if S is empty. On the other hand, buffers are often redundant, but that is hard to establish. 
Example 3 In the .rst part of Table 15, there is a parallel composition implemented properly. 
In the second part, the reception buffers are omitted, and there is a scenario "a.; s.!1; d.; s.!2" leading to a dead­
ß ß 
w = spec ((a.; Proc)[](b.; .ß ))»(b. ; .. ) where Proc is (cß ; c.; Proc) endspec 
. 	.
T.(w, 1) . spec (a.; sß !11; Proc)[](b.; sß !12; .) 
. .
where Proc is (rß !11; c.; sß !11; Proc) endspec 
ß ßß
Tß(w, 1) . spec ((r.!11; Proc)[](r.!12; .))»s. !1; . where Proc is (cß ; s. ß !11; r. ß !11; Proc) endspec 
T. (w, 1) . spec r ß . !1; b. ; . endspec 
Table 13: An example combining .nite and in.nite alter­natives 

(7) T ' c(b, z) := (Parc,1|[Pc(S)]|Parc,2) 

where Parc,n := hide {bc, |SHc,,c(b)} in ren {(bc, /rcc , )|SHc,,c(b)} in Termc(bn, z) endren |[{bc, |S Hc,,c(b)}]| |||SH (b)FIFO(rcc , , bc, , z ·C I +(bn)) endhide 
c,,c 

Table 14: Mapping T' for parallel composition 
w = spec (((a.; ..)|||(bß ; .ß )) »(cß ; .ß))|[bß ]|(d.; bß; .ß ) endspec 
. .

T.(w, .) . spec (a.; sß !1; .)|||(d.; sß !2; .) endspec Tß(w, .) . spec hide b. in (bß; b.!1; cß; .)|[b.]|FIFO(r. ß , b., 1) endhide |[bß ]|hide b. in (b.!2; bß ; .)|[b.]|FIFO(r. ß , b., 2) endhide endspec . .
T.(w, .) . spec (a.; sß !1; .)|||(d.; sß !2; .) endspec 
Tß(w, .) . spec (bß; r. ß !1; cß ; .)|[bß]|(r. ß !2; bß ; .) endspec 
w = spec (((a.; ..)|||(bß ; .ß )) »(cß ; .ß))|||(d.; eß; .ß ) endspec 

. .

T.(w, .) . spec (a.; sß !1; .)|||(d.; sß !2; .) endspec 
Tß(w, .) . spec (bß; r. ß !1; cß ; .)|||(r. ß !2; eß ; .) endspec 

Table 15: An example of parallel composition requiring buffered reception 
w = spec (..[>(a.; bß ; ..))|[a.]|(..[](i.; a.; ..)) 3.10 Implementation of choice 
endspec 
. .

T.(w, 1) . spec ((.[> (a.; sß !11; rß !11; .)) For a b speci.ed as "b1[]b2", we assume that there are ser­|[a.]|(.[](i; a.; .))) vice actions (at least a .) in both alternatives, so that both 
. 

»sß !1; . endspec are relevant. The operator introduces distributed con.icts, Tß (w, 1) . spec ((r. ß !11; bß ; s. ß !11; stop)[> .) formally DC (b), if b has more than one starting compo­|||(r. ß !1; .) endspec 
nent. Protocol T(b, z) combines protocols Term(b1, z) andTable 16: An example of decisive and synchronized termi­Term(b2, z). b2 is the higher-priority alternative, sonation Term(b2, z) upon its start always quickly disables Term(b1, z), even if Term(b1, z) has already started. On the other hand, when a component detects the start of 
lock, because message 2 is not the .rst in the channel. 

Term(b1, z), it tries to prevent starting of Term(b2, z), In the third part, we no longer require that the two con-but might be unsuccessful. current parts are synchronized on bß. We also rename the Until one of the alternatives is abandoned, protocols second bß into eß, to distinguish it from the .rst one. The Term(b1, z) and Term(b2, z) run in parallel, so we re-above scenario no longer leads to a deadlock, but its desti-quire that their protocol message sets are disjoint. nation state erroneously requires that bß is executed before 
Within Term(b1, z), any starting action must be 
eß. Again, reception buffers would help. 
promptly reported to any starting component c of b2, for­mally SRc(b1), to inform it that execution of b2 should not start unless it already has. Analogously, we re-

For a b speci.ed as "b1|[S]|b2", successful termination quire S Rc(b2) for any starting component c of b1. If of T(b, z) requires successful termination of Term(b1, z) 
DC (b), any component might already be executing b1 and Term(b2, z). If such termination is decisive for one 
when Term(b2, z) starts, so we require S Rc(b2) also for or both of the component protocols, i.e. represents a . in 
the non-starting participants of b1, to make them quickly a decisive position within b1 or b2, formally DT (b), its 
abandon execution of b1. Note that the executor of an ac­implementation is problematic [14, 15]. It has been sug­
tion is informed of the action by the action itself. gested that such a . should be put under control of a sin-
If not earlier, a participant c abandons Termc(b2, z)gle server component, its pre-assigned executor, responsi­
upon successful termination of Termc(b1, z), if any. At ble both for its decisive role and for its synchronization role 
that moment, it must already be obvious that Term(b2, z)[14]. If successful termination of T(b, z) is to be a matter 
will never start, i.e. every starting component of b2 of a single component, the latter must be the only member 
must have already executed an action within Term(b1, z), of T C (b), and consequently the only member of E C (b), 
thereby refusing to be an initiator of Term(b2, z). In T C +(b1), T C +(b2), E C (b1) and E C (b2). '
other words, such a starting component c must guard the termination at c, formally GT + (b1). 
c,c, 

If not earlier, a participant c abandons Termc(b1, z) Example 4 An example of decisive and synchronized ter-upon successful termination of Termc(b2, z), if any. At mination is given in Table 16. Termination of b has been put that moment, c must already have detected the start of 
under exclusive control of component ., while component Term(b2, z), and that is true if and only if c is a partic­ß receives only a report of it. ipating component of b2. 
(8) T ' c(b, z) := if ¬DC (b) then (Termc(b1, z)[]Termc(b2, z)) 
cc 	cn
else ren .n=1,2 ({(u /uc )|(u . ASc(bn))} + {(rc, /ac, )|C H + (bn)}) in hide t in 
n c,,c ((Constc,1|[StGtc,2 + RecGtc,2 + {t}]|Constc,2) |[StGtc,1 + RecGtc,1 + StGtc,2 + RecGtc,2]|Constc,3) |[RecGtc,1 + {ac2 , |C H + (b1)}]|Constc,4
c,,c 
endhide endren 

where Constc,1 := (((Taskc,1 »	t; stop)[> (OneStRecc,2 »(AllStRecc,2|||AllRecc,1)))[> .) c 1 c
where Taskc,1 := ren {(u1/uc)|(u c . ASc(b1))} + {(ac, /rc, )|C H + (b1)} in Parc,1 endren 
c,,c where Parc,1 := see Table 14 Constc,2 := (Taskc,2[](t; .)) c 2 c
where Taskc,2 := ren {(u2/uc)|(u c . ASc(b2))} + {(ac, /rc, )|C H + (b2)}
c,,c 

in Termc(b2, z) endren 
Constc,3 := (((OneStRecc,2 »(AllStRecc,2|||AllRecc,1))[] 
(OneStRecc,1 »(AllStRecc,1 

[> (OneRecc,2 »(AllStRecc,2|||AllRecc,1))))) [> .) Constc,4 := ((|||+ (Loop(ac1 , ?z·C I +(b1))[> Loop(ac2 , ?z·C I +(b2))))[> .)
C H(b1)
c,,c 
c n

StGtc,n := {u |(u c . SSc(bn))}
n

RecGtc,n := {ac, |C H + (bn)}
c,,c 

OneRecc,n := ([]g.RecGtc,n (g?z·C I +(bn); .)) OneStRecc,n := (([]g.StGtc,n (g; .))[]OneRecc,n) AllRecc,n := (stop|||(|||g.RecGtc,n Loop(g?z·C I +(bn)))) AllStRecc,n := ((|||g.StGtc,n Loop(g))|||AllRecc,n) endif 
Table 17: Mapping T' for choice 
A participant c combines Termc(b1, z) and Termc(b2, z) as speci.ed in Table 17. If ¬DC (b), Term(b1, z) is known to be the selected alternative as soon as it starts, so every c is allowed to execute Termc(b1, z) and Termc(b2, z) as alternatives. 
If DC (b), Termc(b1, z) and Termc(b2, z) must be combined in such a complicated way that no LOTOS op­erator can express it directly. So we resort to the so called constraint-oriented speci.cation style [28]. This is the style in which two or more parallel processes synchronize on the actions they collectively control, and each process imposes its own constraints on the execution of the actions, so that they are enabled only when so allowed by all the processes referring to them. 
A T' c(b, z) consists of four constraints. Constc,1 and Constc,2 are respectively responsible for execution of Termc(b1, z) and Termc(b2, z), while Constc,3 and Constc,4 serve for their additional co-ordination. 
In the .rst place, we must be aware that in the case of DC (b), protocols Term(b1, z) and Term(b2, z) are actually executed in parallel for some time, so every shared incoming channel in principle requires an in­put buffer for Termc(b1, z) and an input buffer for 
'
Termc(b2, z) (see Section 3.9). But as no c ever trans­mits to c within Termc, (b1, z) after it has transmitted to c within Termc, (b2, z), input buffers for prompt re­ception are necessary only for Termc(b1, z). So we en­hance Termc(b1, z) into Parc,1, as described in Table 14, though the buffers are usually redundant. 
Internally to T' c(b, z), we rename every service prim-
c 	c
itive uin Termc(b1, z) (i.e. 	in Parc,1) into u1. Like-
c
wise, we internally rename every service primitive u
c
in Termc(b2, z) into u2. Besides, we internally to T' c(b, z) split every reception gate rc c, into gates a1 c, and a2 c, , where messages for Termc(b1, z) are, according to their contents, routed to the .rst gate, and messages for Termc(b2, z) to the second gate. The renamings are guided by service attributes ASc(bn) (lists all the service actions of bn at c) and C H + (bn) (true if the channel from 
c,,c 
' 
c to c is employed within Term(bn, z)). 
Applying all the above renamings to Parc,1 and Termc(b2, z), we obtain processes Taskc,1 and Taskc,2, respectively, that have disjoint sets of service primitives and reception gates. Every action within T' c(b, z) is an ac­tion of Taskc,1 or an action of Taskc,2, except that there is also an action on a hidden gate t serving for synchroniza­tion of Constc,1 and Constc,2 upon successful termina­tion of Taskc,1. 
The critical actions of Taskc,1 are its starting actions. They must in.uence execution of Taskc,2, so they are sub­ject to synchronization between Constc,1 and Constc,3. A starting action of Taskc,1 is a starting service action of b1 at c, i.e. a member of S Sc(b1), or a reception. If it is a member of S Sc(b1), it might also be an i or a ., i.e. not suitable for synchronization, so we in principle require that every member of SSc(b1) is a service primitive. If c is not a starting component of b2, Constc,3 is redundant, hence the requirement is not necessary. 
The critical actions of Taskc,2 are its starting actions. They must in principle in.uence execution of Taskc,1, so they are subject to synchronization between Constc,1 and Constc,2. A starting action of Taskc,2 is a member of S Sc(b2) or a reception. If disruption of Taskc,1 is nec­essary, i.e. if P Cc(b1), we require that every member of 

w = spec ((a.; .)|||(bß ; .))[]((c. ; .)|||(bß ; .)) endspec 
w1 = spec ((a.; (.ß |||.. ))|||(bß ; .. ))[]((c. ; (..|||.ß ))|||(bß ; (..|||.. ))) endspec 
w2 = spec ((a.; (.ß |||.. ))|||(bß ; i. ; (..|||.ß )))[]((c. ; (..|||.ß ))|||(bß ; (..|||.. ))) endspec 
w3 = spec ((a.; (.ß |||.. ))|||(bß ; (..|||.ß ; ((i.; .. )|||.ß))|||(bß ; ((i.

; i. )))[]((c. 
; .ß )|||.. ))) endspec 
. in hide t in 
. .

(hide b. in ((a.; ((sß !1; .)|||(s. !1; .)))|||(b. !1; .))|[b. ]|FIFO(a. , b. , 1) endhide»t; stop) ß ?2; .)[](a . ?1))))[> .) 
1 1
2
2 
2 
2

2 
. 
. /a. , rß /aß , r 
2
1
. . 
. /a
T.(w3, .) . spec ren r 
((( 
. ?2)|||Loop(a [](t; .)) 
[> (((a 

. ?2; .)) »(Loop(aß ?2)|||Loop(a 
. .

((a. !2; s. !2; .)|||(aß !2; sß !2; .)) . ?1)[>Loop(a. ?2))[> .)
2 2 1 
2 
ß , a. , t]|( . ]|((Loop(a 
2 2 
2 
|[a endhide endren endspec 
|[a 1 
. , a 
1
1 

/bß . , bß/bß . in hide t in 
1 

(hide b., b. in ((b.!1; .)|||(bß ; s. ß !1; b. !1; .)) |[b., b. ]|(FIFO(a., b., 1)|||FIFO(a. , b. , 1)) endhide»t; stop) 
ß 	. ?1))))[> .)
2 
2 1 
1
2
1 2 
1
Tß(w3, .) . spec ren bß 
(((( 
ß
1
ß 
. /a ß
2

ß 
. /a
, r./a., r , r./a., r 

ß 
.?1)|||Loop(a [](t; .))) 
[> (((b; .)[](a 
2 

. ?2; .)) »(Loop(b)|||Loop(a. ?2)|||Loop(a ((a. !2; .)|||(bß; ((s ß .!2; .)|||(s ß . !2; .))»a.!2; .)) . ]|(((((bß
2 
2
ß(((b1
2 2 
22
. , t]|( , a., a. , b
1 
2 

1 
, a 
ß 
ß|[b2
1
ß ß
1
1
2
)|||Loop(a. ?2)|||Loop(a.?1)|||Loop(a. ?1)))[]|[b; .)[](a 

1 |||?2))(Loop(?1)[Loop(?2)))[> .)>a a. . . 
2 

1 
1 1 
?1; .)[](?1; .)) »a. . 2 
1 

1 
. ?2; .)) »(Loop(b
2 

)|||Loop(a.?1)|||Loop(a. ?1)) 
1 

. ?2; (Loop(bß)|||Loop(a. ?2)|||Loop(a.?1)|||Loop(a. ?1)))))) 
, a
222
; .)[](a 
[>(a 

ß((Loop(b1
2 
[> .)) 
2
., a. , a., a 
2
211 
. ]|(((Loop(a 
1 
. 
|[a endhide endren endspec 
2 

.	?1)[>Loop(a /aß in hide t in 
.. 
./a 
11
. 
./a 
2 r,.
T. (w3, .) . spec ren r 
/a
., r ß, rß ß 
1
1 1 
2 
1 

(hide b., bß in ((b.!1; .)|||(bß!1; ((s. . !1; .)|||(s . !1; .)))) 
2 
ß 

|[b., bß]|(FIFO(a., b., 1)|||FIFO(aß, bß , 1)) endhide»t; stop) ß ?2; .))»(Loop(c. ß?1))))[> .) 
(((( [> (((c. 
.?1)|||Loop(a [](t; .))) 
; .)[](a 
.. . ||||||((c; ((!2; .)(!2; .)) !2; .)(!2; .))»s s a a. . ß 2 
2
2 
1 2
2 

)|||Loop(aß ?2)|||Loop(a 
ß ß ?2; .))»(Loop(c. ß ?1; .)) » 
|[c. |[a 
1 a,. 
2|] (t,ß 
1
. 
, a 
1
1
)|||Loop(aß?2)|||Loop(a.?1)|||Loop(aß ?1)))[]; .)[](a
ß , c , a 
.|](((((cß 1
(((a.?1; .)[](a 
1
((Loop(a 
2
[> (a 
[> .)) 
1
1
2 
1 

.?1)|||Loop(aß ?1)) ß?2; (Loop(c. )|||Loop(aß?2)|||Loop(a.?1)|||Loop(aß ?1)))))) 
211
2
1
2
1
2 

., aß, a., aß]|(((Loop(a.?1)[>Loop(a.?2))|||(Loop(aß ?1)[>Loop(aß?2)))[> .)
|[a endhide endren endspec 

Table 18: An example of distributed choice 
2 
(9) T ' c(b, z) := if ¬DC (b) then (Termc(b1, z)[> Termc(b2, z)) 
c 	cn
else ren .n=1,2 ({(u /uc )|(u c . ASc(bn))} + {(rc, /ac, )|C H + 	(bn)}) in hide t in 
n c,,c ((Constc,1|[StGtc,2 + RecGtc,2 + {t}]|Constc,2) |[StGtc,2 + RecGtc,2 + {p c }]|Constc,3) 
c, |C H + 

1
|[RecGtc,1 + {a endhide endren (b1)}]|Constc,4

c,,c 

where Constc,3 := ((AllStRecc,2[](p 
c 

1
; OneRecc,2 »AllStRecc,2))[> .) 

the rest of de.nitions as in Table 17 endif 
Table 19: Mapping T' for disabling 
S Sc(b2) is a service primitive. 	ogous to OneStRecc,n and AllStRecc,n, respectively, except that they refer only to receptions. 
The gates on which the starting service primitives and receptions within a Taskc,n occur are listed in StGtc,n Constc,1 prescribes the following: 1) Basically, execute and RecGtc,n, respectively. OneStRecc,n speci.es a Taskc,1 and indicate its successful termination by a t. 2) process ready to synchronize on one action of Taskc,n If Taskc,2 starts in the meantime (that will always be be-on gates from StGtc,n and RecGtc,n. AllStRecc,n fore t), stop the basic activity, but remain ready for recep­speci.es a processes ready to synchronize on all such ac-tion of protocol messages sent to Taskc,1. 3) Always be tions. Processes OneRecc,n and AllRecc,n are anal-ready to terminate, though Constc,2 will ensure that that 
w = spec ((a.; .)|||(bß ; .))[>((c.; .)|||(bß; .)) endspec 
ß .ß 
w1 = spec hide p. , p in (((a.; ..)|||(bß ; .ß)) »((p ; ..)|||(p ; .ß ))»(..|||.ß ))[>((c.; .ß )|||(bß ; ..)) endhide endspec 
2 
ß ?2))))[> .)) 
T.(w1, .) . spec hide p. , t in ren r. ß /a 
1
. 
ß /aß , r 

ß in . .
(hide bß in (a.; ((sß !1; .)|||(bß !1; .)) »p .; ((sß !1; .)|||(bß!1; .))) |[bß]|FIFO(aß , bß , 1) endhide»t; stop) ß ?2; .))»(Loop(c. ß?1))))[> .)
1
2 
1 
2 
2 
(((( [>(((c. )|||Loop(a

ß ?2)|||Loop(a 
; aß ?2; (Loop(c.

2 
; .)[](a 
|[c. 
. 
ß, t]|( 
.
2 
2
.

((c.; sß !2; .)|||(aß !2; .)) ß , t]|(((Loop(c. ß ?2))[](p ß?1)[>Loop(a 
2 
2 
1 
[](t; .)))
, a 
.

)|||Loop(a 
ß ß ., bß 
2 1 

)|||Loop(a ß?2))[> .) endren endhide endspec 
, c , a 
ß ]|((Loop(a , t in ren bß 
2
|[p |[a Tß(w1, .) . spec hide pß 
1 
ß, a ß 
1 

. in ß ßß
(hide b. in (bß ; ((s.!1; .)|||(b.!1; .)) »p ; ((s.!1; .)|||(b.!1; .))) |[b.]|FIFO(a., b., 1) endhide»t; stop) 
2

[>(((bß .?2; .)) »(Loop(bß .?1))))[> .) 
2 2
1 
1
2 

2
ß 
./a
/b/b/a, r , r

ß
12
(((( )|||Loop(a 

ß?2; (Loop(b; a.2
2 
.?2)|||Loop(a; .)[](a 
ß 

., t]|( ((a.!2; .)|||(bß ; s. ß !2; .)) 
2 
2
2 
2 
2 ßb?2))[](p, .
2
|[b
ß 
[](t; .)))
, a
2
ß
2
)|||Loop(a.?2))))[> .))
, a

., t]|(((Loop(bß )|||Loop(a ., a.]|((Loop(a.?1)[> Loop(a.?2))[> .) endren endhide endspec 
2 

Table 20: An example of distributed disabling 
21
2
|[p |[a 
1 
will happen only after successful termination of Taskc,1 or Taskc,2. 
Constc,2 prescribes the following: Execute Taskc,2 or terminate upon a t indicating that Taskc,1 has successfully terminated. 
Constc,3 in addition prescribes that in the case that the .rst action belongs to Taskc,1, Taskc,2 may start only upon a reception, i.e. upon detecting that Term(b2, z) has already started at a remote site. 
With the described measures for prompt start report­ing and for prevention of premature local termination, T' c(b, z) will progress towards completion of Taskc,1 or Taskc,2 as appropriate. 
There is, however, still a problem to solve. Taskc,2 must not terminate while c may still expect messages sent to Taskc,1. So we require that Taskc,2 (i.e. Termc(b2, z)) never successfully terminates without receiving on each of the channels on which Termc(b1, z) receives. Upon a re­ception within Termc(b2, z), c knows that on the chan­nel, there will be no more messages for Termc(b1, z). For some channels, the requirement might be redundant. 
It is convenient if c indeed promptly becomes unwilling to receive on gates in RecGtc,1, to improve the possibility of re-use of protocol messages belonging to Termc(b1, z). Therefore we introduce Constc,4. An analogous con­straint for protocol messages belonging to Termc(b2, z) would also be desirable, but we have found its automatic speci.cation too dif.cult. 
Example 5 An example of distributed choice is given in Table 18. The original service speci.cation w is gradu­ally transformed into a well-formed speci.cation, follow­ing suggestions from Section 4.2. w1 secures prompt re­porting of each individual starting service action. w2 in addition secures that no component terminates the .rst al­ternative until it is selected by components ß and ., the starting components of the second alternative. w3 in addi­tion secures that every channel employed for the .rst alter­native is also employed for the second one. 
In each individual component speci.cation, the .rst and the second alternative are highlighted by a box. When di­vergence occurs, components execute the .rst alternative, but gradually switch to the other. We see that every protocol message of the .rst alternative is a 1, and every message of the second one is a 2. All the speci.ed FIFO buffers are redundant. 


3.11 Implementation of disabling 
For a b speci.ed as "b1[> b2", we assume that there are service actions (at least a .) in both parts, so that both are relevant. The operator does not introduce distributed con­.icts, formally ¬DC (b), if there is a c which is the only participating component of b1 and also the only starting component of b2. 
Protocols Term(b1, z) and Term(b2, z) are combined as for "b1[]b2", except that Term(b2, z) is allowed to start as long as there is a starting component c of b2 which has not yet detected that b1 is successfully terminating and con­.rmed this knowledge by executing a special-purpose ser­vice primitive pc in b1. 
A participant c combines Termc(b1, z) and Termc(b2, z) as speci.ed in Table 19. If ¬DC (b), activation of Term(b2, z) is a local matter of the starting component of b2. For any other c, Termc(b1, z) is equivalent to stop, i.e. the component just waits for an eventual start of Termc(b2, z). 
If DC (b), we require that b1 consists of a regular part b3 followed by a dummy part b4 indicating its successful ter­mination (if ¬T M (b1), b4 is never activated, and as such not speci.ed), i.e. we pretend that the service we are imple­menting is actually "b3[> b2". More precisely, we require 
b4 = ((|||SCc(b2)(pc; .c))»(|||.c))
T C c +(b1) 
where p primitives are supposed to be hidden on a higher service level and not among the visible primitives of b3. Note that we also prescribe the executor of each individ­ual .. Since DC (b) and T M (b1) imply that b in no way synchronizes with concurrent service parts, any pc may be regarded entirely as an internal action of T' c(b, z). 
For such a b1, protocol Term(b1, z) consists of two phases. The .rst phase is Term(b3, z) followed by re­porting of successful termination to all the starting com­ponents of b4, i.e. exactly to the starting components of b2. In other words, the components are, as required, promptly informed when starting of Term(b2, z) becomes unde­sirable. If the .rst phase successfully terminates before Term(b2, z) starts, T(b, z) starts executing the usual dis­tributed implementation of a well-formed "b4[]b2". If the start of Term(b2, z) is suf.ciently delayed, the executed alternative is b4, i.e. b1 is not disrupted by b2. In any case, no participant abandons Term(b2, z) until every starting component c of b2 has executed a pc, i.e. refused to be an initiator of Term(b2, z). 
Comparing T' c(b1[> b2, z) with T' c(b1[]b2, z), we see that, instead of waiting for the starting actions of Termc(b1, z), Constc,3 now waits for the only pc in Termc(b1, z), if any. Consequently, instead of synchro­nizing on the gates in StGtc,1 and RecGtc,1, Constc,1 and Constc,3 have to synchronize just on p1 c , hence Constc,3 is much easier to specify. 
Example 6 An example of distributed disabling is given in Table 20. To obtain a well-formed service speci.cation, we furnish the .rst part with the required hidden p actions, and make sure that the starting actions of the second part are promptly reported and that both protocol channels are used for the part. 


4 	Computation and tuning of service attributes 

4.1 Attribute evaluation rules 
The attributes in Table 21 provide information on service actions and their executors. S Sc and ASc respectively list for an a, b or p its starting service actions and all its service actions at c. S Cc and P Cc respectively indicate for an a or b that c is its starting component or its participating component. 
The attributes in Table 22 provide information on suc­cessful terminations. T M , I T and DT respectively indi­cate for a b or p that it might successfully terminate, that it might terminate initially, or that the termination might be decisive. 
The attributes in Table 23 provide information on dis­tributed con.icts. DC indicates for a b that distributed con.icts are introduced by its top-level composition opera­tor. AD and T D respectively indicate for a b or p whether 
M. Kapus-Kolar 
No. SSc No. SSc 
(2) 	SSc(p) = SSc(b) (4) SSc(b) = {.|P Cc(b)}
(3) 	SSc(b) = Ø (6) SSc(b) = SSc(a) 
(12) 	SSc(b) = SSc(p) (13) SSc(a) = {a|P Cc(a)}
(7) 	
SSc(b) = ((SSc(b1)\S) . (SSc(b2)\S). 

(SSc(b1) . SSc(b2) . S)) (8,9) SSc(b) = (SSc(b1) . S Sc(b2)) 

(5) 	
SSc(b) = ((SSc(b1) \ {.}) . {i|(. . SSc(b1))}) 

(10) 	
SSc(b) = ((SSc(b1) \ S) . {i|((SSc(b1) . S) =.Ø)}) 

(11) 	
SSc(b) = ((SSc(b1) \ {s|.(s ' /s) . R}). 


{s ' |.s . SSc(b1) : ((s ' /s) . R)}) No. ASc No. ASc 
(2) 	ASc(p) = ASc(b) (4) ASc(b) = SSc(b) 
(3) 	
ASc(b) = Ø (12) ASc(b) = ASc(p) 

(5) 	
ASc(b) = ((ASc(b1)\{.}).{i} . ASc(b2)) 

(6) 
ASc(b) = (SSc(a) . ASc(b2)) (7–9) ASc(b) = (ASc(b1) . ASc(b2)) 

(10) 	
ASc(b) = ((ASc(b1) \ S) . {i|((ASc(b1) . S) =.Ø)}) 

(11) 	
ASc(b) = ((ASc(b1) \ {s|.(s ' /s) . R}). 


{s ' |.s . ASc(b1) : ((s ' /s) . R)}) (3–12) (SCc(b) = (SSc .
(b) = Ø)). 
(P Cc(b) = (ASc(b) .

= Ø)) 
(4) 	
.c : (P C (b) = {c}) 

(13) 	
(.c : (P C (a) = {c})) . ((.u : (a = u c)) . P Cc(a)) 


Table 21: Service actions and their executors 
No. DT No. DT 
(2) 
DT (p) = DT (b) (10,11) DT (b) = DT (b1) 
(3,4) DT (b) = f alse (12) DT (b) = DT (p) 
(5,6) DT (b) = DT (b2) (7) DT (b) = (DT (b1) . DT (b2)) 


(8) 	
DT (b) = (DT (b1) . DT (b2) . I T (b)) 

(9) 	
DT (b) = (T M (b1) . I T (b2) . DT (b2)) 


(3–12) T M (b) = .c : (. . ASc(b)) (3–12) I T (b) = .c : (. . SSc(b)) 
Table 22: Successful terminations 
No. AD No. AD 
(2) 	AD(p) = AD(b) (3,4) AD(b) = f alse 
(6) 	
AD(b) = AD(b2) (5,7) AD(b) = (AD(b1) . AD(b2)) 

(12) 
AD(b) = AD(p) (10,11) AD(b) = AD(b1) (8,9) AD(b) = (AD(b1) . AD(b2) . DC (b)) 


No. T D No. T D 
(2) 
T D(p) = T D(b) (10,11) T D(b) = T D(b1) 
(3,4) T D(b) = f alse (12) T D(b) = T D(p) 
(5,6) T D(b) = T D(b2) (7) T D(b) = (T D(b1) . T D(b2)) 


(8) 	
T D(b) = (T D(b1) . T D(b2) . (DC (b) . I T (b))) 

(9) 	
T D(b) = (T D(b2) . (DC (b) . (T M (b1) . I T (b2)))) 


(8) 	
DC (b) := (|S C (b)|> 1) 

(9) 	
DC (b) := (|P C (b1) . SC (b2)|> 1) 


Table 23: Distributed con.icts 
there are any distributed con.icts in it and whether there are distributed con.icts involving its successful termination. 
The attribute SRc in Table 24 indicates for a b or p that its start must be promptly reported to c. 
The attribute E Cc in Table 25 indicates for a b or p that c is its ending component for mapping T. E C + is the ana­
c 
logue for mapping Term. 
No. SRc No. SRc 
(1) 
SRc(b) = f alse (5,7,9–11) SRc(b1) = SRc(b) 

(2) 
SRc(b) = SRc(p) (5,6) SRc(b2) = f alse 

(7) 
SRc(b2) = S Rc(b) (12) SRc(p) = (SRc(p) . S Rc(b)) 


(8) 
SRc(b1) = (SRc(b) . SCc(b2)) 

(8) 
SRc(b2) = (SRc(b) . SCc(b1) . (DC (b) . P Cc(b1))) 

(9) 
SRc(b2) = (SRc(b) . P Cc(b1)) 


Table 24: Start reporting 
No. ECc No. ECc 
(2) 
ECc(p) = EC c +(b) (5,6) ECc(b) = EC c +(b2) 

(3) 
ECc(b) = f alse (10,11) ECc(b) = EC c +(b1) 


(4) ECc(b) = P Cc(b) (12) ECc(b) = ECc(p) 
(7–9) ECc(b) = (EC c +(b1) . E C c +(b2)) 
(3–12) EC c +(b) = ((ECc(b).. .c ' : RTc, (b)) . RTc(b)) 

Table 25: Ending components 
No. T C c + 	No. T C c + 
(1) 
T C c +(b) = T M (b) (2) T C c +(b) = T C c +(p) 

(5) 
T C c +(b1) = (ECc(b1) . P Cc(b2) . T Cc(b)) (5–9) T C c +(b2) = (T Cc(b) . P Cc(b) . T M (b2)) (7–11) T C c +(b1) = (T Cc(b) . P Cc(b) . T M (b1)) 

(12) 
T C c +(p) = (T C c +(p) . T Cc(b)) 


No. T Cc 
(3–6,10,11) T Cc(b) = T C c +(b) 
(7) 	T Cc(b) = (T C c +(b) . (ECc(b) . ¬P Cc(b). (¬DT (b).. .c ' : S Hc,,c(b)))) 
(8,9) 	T Cc(b) = (T C c +(b). (((.c ' . S C (b2) : GT + (b1)). 
c,c, 
(¬DC (b). ((E Cc(b) . ¬T M (b1)). 
. .c ' : (C H + (b1) . ¬C T + (b2)))). 
c,,c c,,c 
(¬T M (b2) . P Cc(b2))) .¬P Cc(b))) 
(12) T Cc(b) = (T C c +(b) . (T C c +(p) . ¬P Cc(b))) 
(3–12) RTc(b) = (T C c +(b) . ¬T Cc(b)) 
Table 26: Termination types 
The attributes in Table 26 provide information on termi­nation types. T Cc and T C + respectively indicate for a b
c 
or p that c is its terminating component for mapping T or Term. RTc indicates for a b that c detects its termination upon receiving a special report on it. 
The attributes in Table 27 provide information on utiliza­tion of protocol channels. C Hc,c, and C H + respectively 
c,c, 
indicate for a b or p that mapping T or Term introduces 
'
protocol messages on the channel from c to c . C Tc,c, and C T + respectively indicate that the channel is used in ev­
c,c, 
ery successfully terminating run. For a b consisting of two competing parts, S Hc,c, indicates if the channel is shared. The attributes GTc,c, and GT + in Table 28 respectively 
c,c, 
indicate for a b or p that in mapping T or Term, its success­
'
ful termination at c is guarded by c . 
By the rules in Table 29, we choose for a b such identi­.ers C I and C I + that all protocol messages introduced by mapping T or Term, respectively, are dynamically unique. 
Informatica 27 (2003) 57–73 69 
No. C Hc,c, No. C Hc,c, 
(2) C Hc,c, (p) = C H + (b) (10,11) C Hc,c, (b) = C H + (b1)
c,c, 	c,c, 
(3,4) C Hc,c, (b) = f alse (12) C Hc,c, (b) = C Hc,c, (p) 
(5) C Hc,c, (b) = (C H + (b1) . C H + (b2). 
c,c, c,c, 
((c .' ) . E C c + 
= c (b1) . SCc, (b2))) 
(6) C Hc,c, (b) = (C H + (b2). 
c,c, 
((c .' ) . P Cc(a) . SCc, (b2)))
= c (7–9) C Hc,c, (b) = (C H + (b1) . C H + (b2))
c,c, c,c, 
No. C Tc,c, No. C Tc,c, 
(2) C Tc,c, (p) = C T + (b) (10,11) C Tc,c, (b) = C T + (b1)
c,c, 	c,c, 
(3) 
C Tc,c, (b) = true (12) C Tc,c, (b) = C Tc,c, (p) 

(4) 
C Tc,c, (b) = f alse 

(5) 
C Tc,c, (b) = (C T + (b1) . C T + (b2). 


c,c, c,c, 
((c .' ) . EC c +(b1) . SCc, (b2)))
= c 
(6) C Tc,c, (b) = (C T + (b2). 
c,c, 
((c .' ) . P Cc 
= c (a) . SCc, (b2))) 
(7) C Tc,c, (b) = (C T + (b1) . C T + (b2))
c,c, c,c, 
(8,9) C Tc,c, (b) = (C T + (b1) . C T + (b2))
c,c, c,c, 
(3–12) C H + (b) = (C Hc,c, (b) . (E Cc(b) . RTc, (b)))
c,c, 
(3–12) C T + (b) = (C Tc,c, (b) . (ECc(b) . RTc, (b)))
c,c, 
(7–9) SHc,c, (b) = (C H + (b1) . C H + (b2))
c,c, c,c, 
Table 27: Channel utilization 
No. GTc,c, No. GTc,c, 
(2) GTc,c, (p) = GT + (b) (10,11) GTc,c, (b) = GT + (b1)
c,c, 	c,c, 
(3) 	GTc,c, (b) = true (12) GTc,c, (b) = GTc,c, (p) 
(4) 	
GTc,c, (b) = (¬T Cc(b) . ((c = c ' ) . P Cc(b))) 

(5) 	
GTc,c, (b) = (GT + (b1) . GT + (b2). 

c,c, c,c, (P Cc(b2). .c '' : (EC c+ ,, (b1) . GT c+ ,,,c, (b1)))) 

(6) 	
GTc,c, (b) = ((P Cc, (a) . ((c = c ' ) . P Cc(b2))). GT + (b2))


c,c, 
(7) 	GTc,c, (b) = (GT + (b1) . GT + (b2))
c,c, c,c, 
(8,9) GTc,c, (b) = (GT + (b1) . GT + (b2))
c,c, c,c, 
(3–12) GT + (b) = (¬T C +(b) . (T Cc(b) . GTc,c, (b)). 
c,c, c 
(¬T Cc(b). .c '' : (ECc,, (b) . GTc,,,c, (b)))) 
Table 28: Termination guarding 
No. C I + No. C I + 
(1,2) C I +(b) = . (5,6) C I +(b2) = C I (b) 
(5,10,11) C I +(b1) = C I (b) 
(7–9) if .c, c ' : SHc,c, (b) 

then C I +(b1) = C I (b)·1 , C I +(b2) = C I (b)·2 else C I +(b1) = C I +(b2) = C I (b) endif 
No. C I 
(3–6,10,11) C I (b) = C I +(b) 
(7–9) if (((C I +(b1) .= C I (b)) . (C I +(b2) .

= C I (b))). 
. .c, c ' : (T C c +(b) . RTc, (b) . C Hc,c, (b))) then C I (b) = C I +(b) else C I (b) = C I +(b)·1 endif 
(12) 	if. .c, c ' : (T C c +(b) . RTc, (b) . C Hc,c, (b)) then C I (b) = C I +(b) else C I (b) = C I +(b)·1 endif 
Table 29: Context identi.ers Attribute evaluation rules for a service speci.cation con­

stitute a system of equations which might have more than one solution for the attributes of the explicitly de.ned pro­cesses. One should always maximize their attribute T C + , while other attributes must be minimized. 


4.2 	Additional restrictions and their satisfaction 
Table 30 summarizes the additional restrictions introduced so far for a well-formed service speci.cation. 
The .rst three restrictions state that no irrelevant service part may be speci.ed. The restriction for parallel compo­sition is actually more rigorous than its approximation in Table 30 (see Section 3.9). 
The next two restrictions refer to the ending components of a b. Usually they can be satis.ed simply by proper choice of executors for individual . in b, but not always. It might be that a "b1[]b2 " or a "b1[> b2 " is terminating, but no c quali.es for its ending component, because a GT + (b1) or P Cc(b2) or a C T + (b2) is not true as re­
c,c, 	c,,c 
quired. GT + (b1) can be satis.ed by securing that in the 
c,c, 
terminating runs of b1, the last (possibly dummy) action at c always comes after a (possibly dummy) action at c '. For P Cc(b2), it suf.ces to insert into b2 a dummy action at c. For C T + (b2), it helps to introduce into every terminating 
c,,c 
'
run of b2 an action at c pre.xed by an action at c . 
The next two restrictions require that there are hidden p primitives at certain places in the service speci.cation. If p primitives are already used for other purposes, any other reserved service primitive type will do. 
The next restriction states that a b with distributed con­.icts must not synchronize with a concurrent service part, in order to avoid deadlock resulting from imprecise imple­mentation of b. However, if the concurrent service part is suf.ciently .exible (like, for example, a skilled user of an imprecisely implemented service), there will be no dead­lock and the restriction may be ignored. 
The next two restrictions secure prompt start report­ing. An ordinary action a is always speci.ed in a context "a; b2". A report recipient c must be the executor of a or a starting component of b2, so that the message will be gen­erated to implement the action-pre.x operator. If a c is a missing starting component of b2, that can be solved by in­troducing into b2 a dummy starting service action at c. For reporting of a ., there is no such b2 following, so we have only the .rst option. 
In a general case, execution of a disruptive b might start by concurrent execution and reporting of several starting actions. To avoid as much as possible such multiple report­ing of the start of b, it is advisable to rewrite the speci.ca­tion of b into the action-pre.x form (as required in [10] for b2 in a "b1[> b2"), i.e. make sure that AP (b) (de.ned in Table 31). 
The last two restrictions state that a service action in a particular position must not be an i or a .. If it is an i, change it into a service primitive and hide it on a higher level. If it is a ., pre.x it with a subsequently hidden ser­
(5) 	T M (b1) 
(7) 	((.c.CASc(b1)) . (S + {.})) 
= ((.c.CASc(b2)) . (S + {.})) (8,9) (|P C (b1)|> 0) . (|P C (b2)|> 0) 
(7) DT (b) . (|EC (b)| = 1) (3–12) ECc(b) . T Cc(b) 
(1) 	. .c : (p c . ASc(b)) 
(9) 	DC (b) . .b3 : 
((b1 = (b3 if T M (b1) then »(|||SCc(b2)(p c; .c)) »(|||+ .c)
T Cc (b1) 
endif) 
.. .c : (p c . ASc(b3))) 

(7) ((S =.Ø) . ¬AD(b)) . ¬T D(b) 
(4) 	
S Rc(b) . P Cc(b) 

(6) 	
S Rc(b) . (P Cc(a) . SCc(b2)) 


(8) DC (b) . (SCc(b2) . (({i, .} . SSc(b1)) = Ø)) (8,9) DC (b) . (P Cc(b1) . (({i, .} . SSc(b2)) = Ø)) 
Table 30: Restrictions 
No. AP No. AP 
(2) AP (p) = AP (b) (3,4,6) AP (b) = true 
(7,9) AP (b) = f alse (8) AP (b) = (AP (b1) . AP (b2)) 

(12) AP (b) = AP (p) (5,10,11) AP (b) = AP (b1) 
Table 31: Action-pre.x form 
vice primitive. For both cases, DC (b) implies that b runs in such a context that the transformation is irrelevant. 


5 Discussion and conclusions 
5.1 	Correctness 
A formal proof of the protocol derivation method is given in [18], and brie.y outlined below. 
For every service part b, the only property that really matters is correctness of its T' and Term implementa­tions for the context in which it is embedded, where a T' implementation consists of the members of P C (b), while a Term implementation might also involve some other server components. However, when proving the property, we also assume over twenty auxiliary properties of the im­plementations. 
All the properties are proven by induction on the ser­vice structure. Most of them are synthesized properties. We prove them for the T' implementations of stop and .. For every composite b (i.e. for every service composition operator), we prove that if Term implementations of the constituent service parts possess the properties, the T' im­plementation of b possesses their analogues. In addition we prove that if the T' implementation of a b possesses the properties, its Term implementations possess their ana­logues. For the few inherited properties, the proof goes in the reverse direction. By proving the main property for the main service process, we prove that the entire service is properly implemented. 

5.2 	Message complexity 
The operators potentially introducing protocol messages are the operators of sequence, choice and disabling. It is often possible to reduce the number of such operators by restructuring the service speci.cation, i.e. by making its inherent parallelism more explicit. If such restyling of the service (and consequently of the protocol) is not unac­ceptable for readability reasons, it can greatly reduce the message complexity, and can even be automated [25]. One should also strive for optimal insertion of dummy service actions and optimal assignment of hidden service actions to server components. 
Anyway, some of the messages introduced by our proto­col derivation mapping are redundant. 
– 	
In some cases, it would be possible to omit a message based on the observation that for the service part b1 to which it belongs, it sequences two service actions which are already sequenced for a concurrent service part b2 synchronized on them [13]. 

– 	
It would be possible to further optimize terminations of implementations of individual service parts, and their reporting in individual runs [14, 24]. 

– 	
When implementing a "b1[]b2", one could make better use of the fact that only the initial parts of b1 and b2 are concurrent. 

– 	
When implementing a "b1[> b2", one could make bet­ter use of the fact that only the initial part of b2 is concurrent to b1. 


With more extensive re-use of messages, their encodings could be shorter, but messages would no longer directly identify the service part to which they belong, leading to more complicated protocol speci.cations. 

5.3 	Comparison with similar methods 
The popular formal technique for specifying self-stabilizing protocols have long been .nite state machines (FSMs) [6, 27, 22]. With their explicit representation of states, they are very convenient for the purpose. Namely, when a process proceeds along a selected path in the tran­sition graph representing its FSM, the fact that it ignores messages belonging to the abandoned paths can be spec­i.ed simply by furnishing each state on the selected path with loops representing reception of such messages. In a process-algebraic language like LOTOS, there is no ex­plicit notion of states, so speci.cation of self-stabilization is a tricky task. 
There are two basic approaches to deriving self-stabilizing protocols. In the older approach [6, 27], a pro­tocol is .rst derived for the ideal case with no divergences and subsequently furnished with the reception-ignoring loops. The derivation algorithm in [22], like ours, handles the ideal and the non-ideal cases in an integrated manner, 
Informatica 27 (2003) 57–73 71 
and is consequently much less complex. Moreover, the al­gorithm derives protocols in a compositional way, support­ing implementation of sequence, choice and iteration. For those operators, the structure of services is quite well re­.ected in the derived protocols. Unfortunately, FSMs are less suited for explicit speci.cation of more complex op­erators, particularly for such introducing concurrency. We have solved the problem by switching to the more expres­sive LOTOS. 
We know no comparable LOTOS-based protocol deriva­tion transformation. Some hidden divergence is allowed in [1], but it is resolved with the help of global controllers. 

5.4 	Handling of data 
We intend to extend our method to service actions associ­ated with data [5, 11], to approach the ideal that the service speci.cation language should be the same as the protocol speci.cation language. The strategy for .exible integrated handling of messages implementing proper ordering of ac­tions and those carrying data is simple [11]: 1) In the ser­vice, identify the points where inter-component exchange of data would be desirable. 2) At each point, introduce a (possibly dummy) action of the data sender followed by a (possibly dummy) action of the data recipient, so that there will be an action-ordering message between the two com­ponents. 3) Let the message carry the data. In our case, data could also be carried in a message reporting termination of a b to a c with RTc(b). 
Data exchange is also desirable as a powerful means for compositional service speci.cation. Whenever the more speci.c operators (e.g. sequential composition, choice and disabling) do not suf.ce for describing a particular kind of composition of a set of service parts, one can still run the parts in parallel and let them exchange and process infor­mation on their respective states. 

5.5 	Handling of quantitative temporal constraints 
Once being able to handle service actions with data, one can easily implement quantitative temporal constraints [12, 23]. Such a constraint speci.es the allowed time gap be­tween two service actions. So the time when the .rst action is executed is just another piece of data generated by the .rst action and needed for timely execution of the second one. Temporal constraints can also be employed for pre­venting distributed con.icts and for further optimization of protocol traf.c [23]. 

5.6 	The problem of co-ordinated self-stabilization 
The most dif.cult challenge for future research seems to be implementation of self-stabilization after divergence in synchronized service parts. The problem is important be­cause synchronized processes are the core of the constraint­oriented speci.cation style, that is indispensable for ex­pressing more exotic forms of service composition. To solve it in a general case, one would need a protocol in­corporating negotiation of implementations of concurrent service parts, so an enhancement along the lines of [29] could help. 

5.7 Conclusions 
Automatic implementation of self-stabilization after diver­gence is an important achievement in LOTOS-based pro­tocol derivation, because many realistic services contain distributed con.icts (e.g. a connection establishment ser­vice with both parties as possible initiators). In the era of service integration, the problem is even more acute, be­cause one often wishes to combine services which are not exactly compatible. Take for example feature interactions in telecommunications, which can be nicely detected and managed based on speci.cations in LOTOS [4]. With the possibility of compositional derivation of self-stabilizing protocols, it suf.ces to specify dynamic management of such interactions on the service level. 
In our future work, we will focus on protocol derivation in E-LOTOS [8], the enhanced successor of LOTOS, be­cause it supports speci.cation of real-time aspects. 



References 
[1] Bista BB, Takahashi K, Shiratori N: A compositional approach for constructing communication services and protocols. IEICE Transactions on Fundamentals E82-A(11):2546–2557 (1999) 
[2] Bolognesi T, Brinksma E: Introduction to the ISO speci.cation language LOTOS. Computer Networks and ISDN Systems 14(1):25–59 (1987) 
[3] Brinksma E, Langerak R: Functionality decomposi­tion by compositional correctness preserving trans­formation. South African Computer Journal 13:2–13 (1995) 
[4] Dietrich F, Hubaux J-P: Formal methods for commu­nication services: meeting the industry expectations. Computer Networks 38(1):99–120 (2002) 
[5] Gotzhein R, Bochmann Gv: Deriving protocol spec­i.cations from service speci.cations including pa­rameters. ACM Transactions on Computer Systems 8(4):255–283 (1990) 
[6] Gouda 	MG, Yu YT: Synthesis of communicat­ing .nite-state machines with guaranteed progress. IEEE Trans. on Communications COM-32(7):779– 788 (1984) 
[7] ISO/IEC: Information Processing Systems 	– Open Systems Interconnection – LOTOS – A Formal De­scription Technique Based on the Temporal Ordering of Observational Behaviour. IS 8807, 1989 
M. Kapus-Kolar 
[8] ISO/IEC: Information Technology -Enhancements to LOTOS (E-LOTOS). IS 15473, 2001 
[9] Kahlouche H, Girardot JJ: A stepwise re.nement based approach for synthesizing protocol speci.ca­tions in an interpreted Petri net model. Proceedings of IEEE INFOCOM’96, pp 1165–1173, 1996 
[10] Kant C, Higashino T, Bochmann Gv: Deriving pro­tocol speci.cations from service speci.cations writ­ten in LOTOS. Distributed Computing 10(1):29-47 (1996) 
[11] Kapus-Kolar 	M: Deriving protocol speci.cations from service speci.cations including parameters. Mi­croprocessing and Microprogramming 32:731–738 (1991) 
[12] Kapus-Kolar 	M: Deriving protocol speci.cations from service speci.cations with heterogeneous tim­ing requirements. Proceedings SERTS’91. IEE, Lon­don 1991, pp 266–270 
[13] Kapus-Kolar M: On context-sensitive service-based protocol derivation. Proceedings of MELECON’96. IEEE Computer Society Press 1996, pp 955–958 
[14] Kapus-Kolar 	M: More ef.cient functionality de­composition in LOTOS. Informatica (Ljubljana) 23(2):259–273 (1999) 
[15] Kapus-Kolar M: Comments 	on deriving protocol speci.cations from service speci.cations written in LOTOS. Distributed Computing 12(4):175–177 (1999) 
[16] Kapus-Kolar 	M: Service-based synthesis of two-party protocols. Elektrotehniški vestnik 67(3):153– 161 (2000) 
[17] Kapus-Kolar M: Global con.ict resolution in 	au­tomated service-based protocol synthesis. South African Computer Journal 27:34–48 (2001) 
[18] Kapus-Kolar M: Deriving self-stabilizing protocols for services speci.ed in LOTOS. Technical Report #8476, Jožef Stefan Institute, Ljubljana, 2003 
[19] Khendek F, Bochmann Gv, Kant C: New results on deriving protocol speci.cations from service speci­.cations. Proceedings of ACM SIGCOMM’89, pp 136–145, 1989 
[20] Langerak 	R: Decomposition of functionality: A correctness-preserving LOTOS transformation. Pro­tocol Speci.cation, Testing and Veri.cation X. North-Holland, Amsterdam 1990, pp 203–218 
[21] Naik K, Cheng Z, Wei DSL: Distributed implementa­tion of the disabling operator in LOTOS. Information and Software Technology 41(3):123–130 (1999) 

[22] Nakamura M, Kakuda Y, Kikuno T: On constructing communication protocols from component -based service speci.cations. Computer Communications 19(14):1200–1215 (1996) 
[23] Nakata A, Higashino T, Taniguchi K: Protocol syn­thesis from timed and structured speci.cations. Pro­ceedings of ICNP’95. IEEE Computer Society Press 1995, pp 74–81 
[24] Nakata A, Higashino T, Taniguchi K: Protocol syn­thesis from context-free processes using event struc­tures. Proceedings RTCSA’98. IEEE Computer Soci­ety Press 1998, pp 173–180 
[25] Pavón Gomez S, Hulström M, Quemada J, de Frutos D, Ortega Mallen Y: Inverse expansion. Formal De­scription Techniques IV. North-Holland, Amsterdam 1992, pp 297-312 
[26] Saleh K: Synthesis of communication protocols: An annotated bibliography. Computer Communication Review 26(5):40–59 (1996) 
[27] Saleh K, Probert RL: An 	extended service-based method for the synthesis of protocols. Proceedings of the Sixth Bilkent Intern. Symp. on Computer and Information Sciences. Elsevier, Amsterdam 1991, pp 547–557 
[28] Vissers CA, Scollo G, Sinderen Mv: 	Speci.cation styles in distributed systems design and veri.cation. Theoretical Computer Science 89:179–206 (1991) 
[29] Yasumoto K, Higashino T, Taniguchi K: A compiler to implement LOTOS speci.cations in distributed environments. Computer Networks 36(2–3):291–310 (2001)