E-LOTOS-Based Compositional Service-Based Synthesis of Multi-Party Time-Sharing-Based Protocols Monika Kapus-Kolar Jožef Stefan Institute, Department of Communication Systems, Jamova 39, 1111 Ljubljana, Slovenia E-mail: monika. kapus-kolar@ ijs. si Abstract. In an earlier paper, we proposed a LOTOS/T+-based method for compositional service-based construction of multi-party time-sharing-based protocols. In the present paper, we generalize the method to services with data, real-time constraints, iteration, exception handling, multi-process synchronization and process suspension/resumption, and adapt it to work with the standard specification language E-LOTOS enhanced with weak sequencing. We also report a minor error in the earlier method and propose a more flexible event-reporting scheme. Key words: distributed service implementation, protocol synthesis, E-LOTOS Kompozicionalno snovanje večpartnerskih protokolov z delitvijo časa na osnovi opisov pričakovanih storitev v jeziku E-LOTOS Povzetek. V preteklosti smo predlagali metodo za kompozicionalno sintezo večpartnerskih protokolov z delitvijo časa na osnovi opisov pričakovanih storitev v jeziku LOTOS/T+. V pričujočem članku to metodo posplošimo na storitve s podatki, časovnimi omejitvami, ponavljanjem, obravnavanjem izjem, večprocesno sinhronizacijo in začasnimi prekinitvami procesov ter jo prilagodimo za delo s standardnim specifikacijskim jezikom E-LOTOS obogatenim s šibkim vrstenjem. Poročamo tudi o manjši napaki v originalni metodi in predlagamo bolj prilagodljivo shemo poročanja o dogodkih. Ključne besede: porazdeljena implementacija storitev, sinteza protokolov, E-LOTOS 1 Introduction For its users, a distributed server is a black box interacting with its environment through a set of service access points (SAPs). The behaviour of a server at its SAPs is the service it offers. The atomic instantaneous interactions constituting a service are its primitives (SPs). In a more detailed view, each SAP belongs to a particular place and is there supported by a particular protocol entity (PE). If necessary, the PEs communicate over a medium, i.e. execute a protocol implementing the service. We limit our discussion to protocols operating over reliable media. In [1], we proposed a method for compositional service-based construction of multi-party protocols. The method accepts and generates specifications written in LOTOS/T+ [2], a non-standard successor of LOTOS [3], a standard process-algebraic language for formal specification of concurrent and reactive systems. Unlike [2], another LOTOS/T+-based method, [1] does not address implementation of real-time service constraints, but can handle distributed conflicts. Unlike other protocol derivation methods based on LOTOS-like languages (see [1] for a list), the method of [1] generates protocols that resolve distributed conflicts between SPs through time sharing. If the transit delay of the underlying communication medium is short, this is often the optimal approach to conflict resolution [1]. In the present paper, we generalize the method of [1] to services with data, real-time constraints, iteration, exception handling, multi-process synchronization and process suspension/resumption, and adapt it to work with E-LOTOS [4, 5], a standard successor of LOTOS for specification of real-time systems. The only non-standard E-LOTOS feature we have not been able to avoid in the derived protocol specifications is weak sequencing [6]. We also report an error in [1] and propose a more flexible event-reporting scheme with plenty of space for protocol optimization. The paper is organized as follows. There is no motivation section, for a thorough discussion on the applicability of time-sharing-based protocols can be found in [1]. Sect. 2 more precisely defines the adopted specification language, the server model, the concept of a well-formed service specification and the protocol derivation problem. Sects. 3 and 4, respectively, describe the syntactic and the semantic aspects of the proposed protocol derivation method. Sect. 5 discusses the protocol derivation process. Sect. 6 concludes the paper by summarizing the proposed optimizations over [1] and [2]. 2 Formalization of the Protocol Derivation Problem 2.1 The Basic Kinds of E-LOTOS Processes An E-LOTOS process P executes a series of zero or more events. For each event, its relative execution time (RET) is measured relatively to the moment when it became logically enabled, while its absolute execution time (AET) is measured relatively to the start of the considered system. Let absolute time range over non-negative integers, with t denoting a time instant. "block" denotes time block, and "stop" inaction, "null" denotes immediate successful termination, i.e. a special urgent event 5. In its generalization "P := P", the event matches pattern P with the value of expression E (if its computation is successful), thereby updating the variables bound by the pattern. The simplest E is a constant K. Another generalization of "null" is "wait(P)", denoting a 5 with RET E. An "i" specifies an anonymous urgent internal process action i followed by a 5. A "GPi@P2[P]" specifies an interaction of the specified process at gate G, i.e. an observable action o, followed by successful termination. Patterns Pi and P2, respectively, denote the data associated with the action and its RET. E is an additional constraint on the data and the RET. In E-LOTOS, an o is by definition non-urgent, i.e. always has passing of time as a legal alternative. In LO-TOS/T+, an o becomes urgent as soon as it reaches its deadline. This is an important semantic difference between the two languages. Urgent issuing of a signal X carrying data E can be specified as exception raising "raise X(E)" or, if followed by a 5, by "signal X(E)". A "trap exception Xi(IPLi) is B\ endexn... exception Xn(IPLn) is Bn endexn exit P is Pn+1 endexit in Pn+2 endtrap" denotes process Pn+2 possibly followed by handling of a particular event trapped in it. Each Xi denotes a signal trapped as an exception and transferring control and data IPLi from Pn+2 to Bi, while "exit P is Pn+1 endexit" specifies that 5 in Pn+2 transfers control and data P to Pn+i- A shorthand for the case where only S is trapped and all the output data of Pn+2 is passed to Pn+i is "Pn+2; Pn+1". A "loop B endloop" basically denotes an infinite sequence "P; P;...", but if an exception "inner" occurs in a P, this is successful termination of the loop. A "P1QP2" denotes a process behaving as B\ or as P2, where the choice is made upon the first event. A "choice P[]B endch" denotes the choice between multiple processes P, with an instance of P for every value matching the pattern P. A "Pi [X > P2" denotes process B\ repeatedly suspended upon the start of P2. Whenever signal X occurs in P2, Pi is resumed and P2 reset to its initial state. A P of the form "Pi[X > P2" contains a family of implicit trapping operators, because whenever P2 executes its first event and becomes a^, P is reduced to "trap exception X is B\ [X > P2 in B'2 endtrap". "Pi [> P2" is a shorthand for the case with no X in P2. Note that the (n + l)-th instance of P2 is enabled when Pi is resumed after being suspended by the n-th instance of P2. A "par Gi#Ki,...,Gn#Knin [rx] Bi||...|| [rm] —» Pm endpar" denotes parallel composition of processes B\ to Pm. Each Bi is associated with a Ti listing the gates on which Bi synchronizes with its peers. If the gate G on which a synchronization occurs has its synchronization degree K defined in the list "Gi 1,..., Gn#ifn", the event is a synchronization of exactly K processes Bi with G in Ti, otherwise it is a synchronization of all such processes. The composite process successfully terminates when all its constituents do. A shorthand for processes B\ and P2 synchronized on gates Gi to Gn is "Pi | [Gi,..., Gn) |P2", with "Pi 11 |P2" and "P1HP2" shorthands for the minimal and the maximal synchronization, respectively. A "par P in iV|||P endpar" denotes independent parallel composition of multiple processes P. There is an instance of P for every value which matches the pattern P and is in the list N. A "rename gate Gi(IPLi) is G'xPi... gate Gm(/PPm) is G^Pm signal X1(IPL[) is X[Ex ... signal Xn(IPL'n) is XfnEn in P endren" denotes process P with some of its events renamed as specified. A "hide Gi : Ti,..., Gn : Tn in P endhide" denotes process P with all its actions on gates Gi to Gn of the respective types T\ to Tn changed into i. A "var Ui : Ti := Pi,..., Un : Tn := En in P endvar" denotes process P with some variables Vi, respectively of type Ti and initialized to Ei. A "case (Pi,..., Em) is Pi [E[] B1 |... |Pn[E'n] —» Pn endcase" denotes the first Bi in the list of processes Pi to Bn for which "(Pi,..., Em)" matches pattern Pi and satisfies constraint E[. A shorthand for a series of binary decisions is "if Pi then B\ elseif P2 then P2 ... elseif En then Pn else Pn+i endif". In the above constructs, many parts are just optional, with defaults defined in [4]. Parentheses may be used to direct parsing. We will typically refer to individual specification parts by their generic syntactic form, although in examples, we will also use shorthands or omit parts irrelevant for the discussion. For a process P, let Q(B) denote its visible gates. Two processes are considered equivalent if they have the same influence on every environment synchronized on their visible gates and trapping their signals and 5. 2.2 Weak Sequencing When successful termination or an exception of a B\ is trapped and handled by a the standard E-LOTOS semantics prescribes that B2 starts strictly after the termination of B\. In a real-time protocol, however, it might be crucial that a particular o in B2 is enabled as soon as B\ becomes able to proceed towards the particular kind of termination executing exclusively actions which o is allowed to overtake. In other words, weak sequencing might be necessary, and can indeed be introduced into E-LOTOS in a consistent and efficient way [6]. An accelerated o might resolve a choice. Example 1 Suppose that in "(a[]6); c", c is allowed to overtake a, but not b. Hence, c may occur as the first event of the process, but that resolves the choice in favour of a, for otherwise the illegal "c; 6" would be a possible run. Whenever we want weak sequencing for the trappings introduced with a particular process composition operator, we will decorate the operator with a C listing the pairs (G1, G2) such that actions on G2 are allowed to overtake actions on G\, e.g. "trap ... exception X(LPL)\C is B2 endexn...in B\ endtrap", "£?i;C| B2\ "loop C\B endloop", "Bx [X\C> B2". 2.3 Server Model We assume that a distributed server interacts with its users through a set of service gates S from a universe S, respectively of type Ts. Every action on a service gate is considered to be an SP, even if it is dummy and thus hidden from service users. The hidden SPs are urgent, i.e. executed as soon as possible, the others are not. Each S is located at a particular place. There are at least two places. Let p and p' denote two different places. At each place p, there is a process PEp, the protocol entity of the place. The remaining process of the server is the communication medium. Each PEp has three kinds of gates: 1) It controls the local service gates. 2) For every local S and remote p', there is a transmission gate s™ , of type (Ts, T's), where T's has the same structure as Ts, except that all items in it are boolean. 3) For every S at a remote p', there is a reception gate vvTs, of type Ts. For a local S, a PEp can transmit a type Ts message Msg to a PEp> by executing an "s^ (Msg, Sel)" where every item in Msg has a corresponding selector in Sel. Only the items whose selector is true are transferred to p', together with information on Ts. The medium delivers the message to p' after a transit delay not greater than a known dp,p negligibly short from the point of the expected service users, where (dp,p = 0) and (dp,p < dp,p + dp ,p ) for every p". Once received by p', the message waits in a local buffer, that is formally also a part of the medium, until claimed by PEp> on gate However, Msg is not delivered to PEp/ in its original form, as the medium replaces all its non-transferred parts with wildcards. Actions involving the medium are hidden from service users and as such executed as soon as possible. The medium issues no signals. Messages in input buffers can be claimed in any order. 2.4 Well-Formed Service Specifications To simplify protocol synthesis, we restrict our focus to well-formed service specifications (WFSS), i.e. to unambiguously parsable specifications in the language from Sect. 2.1 complying to the restrictions below. A WFSS is supposed to describe a non-parameterized non-blocking process Srv in which every event is a (possibly hidden) SP. Restriction 11) Every expression E in Srv must be such that its evaluation always successfully terminates. 2) Srv must be a non-parameterized "rename R in hide H in Srv' endhide endren" where R specifies the desired local renamings of SPs into SPs, H specifies the desired hidings of SPs, and Srv' refers exclusively to service gates. 3) No B in Srv' may be able to block without previously successfully terminating or raising an exception. 4) "rename..." is not allowed in Srv'. 5) Every "loop ..." in Srv' must be such that it never successfully terminates. 6) Every "case ... B\ ... Bn endcase" in Srv' must be such that it never fails to select a Bi. 7) Every event in Srv' must be a visible SP, hence Restriction 2 In Srv', 1) "signal...", "i" and "hide ..." are forbidden, 2) for every S or exception specified, there must be a trap, 3) in every "B1WB2", the starting events of Bi and B2 must be SPs, 4) in every "choice P[]B 1 endch", the starting events of B\ must be SPs, 5) in every "B\ [X > B2 ", the events of B\ and the starting events of B2 must be SPs, and 6) in every "par ... Bi...", every event of Bi must be an SP or a S, where 3) to 6) preclude implicit i [41. A process is aware of time if upon every action, it is aware of its AET. In E-LOTOS, timing constraints can directly refer only to RETs, therefore we need Restriction 3 Srv' must be a "Cl\\Mn" where 1) every Ts denotes a record with the first field of type time, 2) in Mn, there is no "@P" or "wait...", and 3) CI is just a constraint [7] securing that whenever Mn executes an SP, its first data item is its AET. Example 2 Suppose that Q(Mn) is {a,b} where Ta is a "(time, bool)" and Tb is a "(time, nat)". CI can be "var oldt : time := 0, ret : time, newt : time in loop (a(?newt,any : bool)@?ret[newt = (oldt + ret)] [] 6(?newt,any : nat)@?ret[newt = (oldt + ret)]); ?oldt newt endloop end var". Instead of an "alfalse; 6!1@!3" in Mn, one would write "a(?x; Ifalse); b(\(x + 3), !1)", thereby achieving that in the presence of CI, b is executed 3 time units after a. Restriction 4 Let in Mn every 1) "trap ..." be a "trap ... endexn in...", though "B\\B2" is also allowed, 2) "exception X(IPL)" be an "exception X(?Vi : Ti, ..., lVn : Tn)", and 3) "SP[E]" belong to a "var Vl : time in SP[E] endvar" and be an "S(Wi,W2,..., Wn)[(Vi = V2) A E']" of type Ts with V2 of type time and E' not referring toV1. 2.5 Protocol Derivation Problem We are looking for a mapping which would take a WFSS and generate such PEp that with the resulting protocol M(5ri;), the server would be equivalent to Srv. We want that maps a specification by mapping its parts, while noting that for an efficient protocol, the mapping has to be context-dependent. 3 Syntactic Aspects of Protocol Derivation For a place, it might be convenient to pretend that reports on SPs belonging to different gates of Mn are exchanged through different gates. Internally, such a p would use gates s^ and r^ instead of s^ and respectively. Let 1Z denote the universe of gates r^. Hiding and renaming of SPs without changing their location are a local matter, hence Mapping 1 For every p, Mp (rename R in hide H in Srv' endhide endren) is "rename R U Rp in hide H in Mp(aSW) endhide endren", where Rp renames gates s^, and rs into s^J and r^, respectively. Assuming that time progresses at all places with the same speed, time awareness is a local matter, hence Mapping 2 For every p, M p(Srv) is "C7P|[(/(MP( Mn)) n (p( B)\ ^ Mp(Bm) endpar", where for every i in {1,..., m}, there is such a set Ui(B) of pairs (S,p) with S in Ti, not at p and not mentioned in D, that for every p, T i,P(B) consists of gates sps with (S,p) in Ui(B) and of gates with (S,p) in Ui(B). Mapping 11 For every p, if a B in Mn is a "par P in N\\\B! endpar", MP(B) is "par P in 7V|||Mp(£i) endpar". Example 5 For "(a; b) \ [a] \ (a; c)" with a at a p and b and c at a p , a must be reported to p both in subprotocol Mia; b) and in subprotocol M(a; c), but if~M.p(a; b) and Mp(a; c) are synchronized on sj , and Mp/ (a; b) and Mp/ (a; c) on ra, there is only one protocol message. At every place, receptions must be allowed to overtake any non-SP action, for otherwise a message might be received with a non-zero local delay. In [1], we were not aware of that and so the method, unless corrected as in [8], generates incorrect protocols. Hence Mapping 12 For every p, if a B in Mn is a "Pi; B2", MP(B) is "(Mp(B1Y1Cp(B)\Mp(B2))"f where CP(B) lists all the pairs (Gi,G2) of Gi in (Q(M.p(Bi))\S) and G2 in (g(Mp(B2))nn). Mapping 13 For every p, if a B in Mn is a "loop Pi endloop", MP(B) is "loop CP(B)\MP(B1) endloop", where CP(B) lists all the pairs (Gi,G2) of G\ in (6(Mp(Bi))\5) and G2 in (0(Mp(£i)) n U). Mapping 14 For every p, if a B in Mn is a "trap exception Xi(IPLi) is Pi endexn... exception Xn(IPLn) is Bn endexn in Pn+i endtrap", MP(B) is "trap exception Xi(IPLi)\Ci,p(B) is Mp(Pi) endexn... exception Xn{lPLn)\Cn,P(B) is Mp(Bn) endexn in Mp(Pn+i) endtrap", where a CiiP(B) lists all the pairs (£1,62) of Gi in (C?(Mp(Pn+i)) \ S) and G2 in 0g(Mp(Bi))nn). Example 6 For "a@!0; (6@!2[]c@?x[x > 4])" with a, b and c at three different places p, p' andp", respectively, suppose that a report on a arrives to p and p" at times 1 and 5, respectively, and a report on b arrives to p" at 3. Ifp" implements ";" as strong sequencing, it enables Mpn(b ... []c ...) at 5, when it suddenly becomes ready not only for reception of the report on b, but also for an illegal c. If the sequencing at p" is adequately weakened, p" receives the report on b already at 3, in time to prevent c. In the distributed implementation of choice, there are cases where it is necessary that a place a priori abandons all but one of the alternatives, hence Mapping 15 For every p, if a B in Mn is a "Bi[]B2", MP(B) is "if Ei P(B) then Mp(Pi) elseif E2 P(B) then MP(B2) else Mp(Pi)[]Mp(P2) endif ". Mapping 16 For every p, if a B in Mn is a "choice P[]Bi endch", with P of a type T, MP(B) is "case E\ P(B) is P[E2,p(B)] Mp(£i)|any : T choice P[]Mp(Pi) endch endcase", with Pi,p(P) of type T. Example 7 For "(a[]6); c; d" with a, b and c at a p and d at a p , a and b need not be reported to p , hence Mp/ (a) and Mp/(6) can both be a "null", but then (Mp/(a)[]Mp/(6)) is "null[]null", i.e. a process unable to execute the required 5 [4]. Keeping only one of the equivalent alternatives yields a correct Mp/ (a[]6). Rule 3 For every p and B of the form "Pi []B2 ", "P2[]Pi ", "choice P[]Pi endch" or "B2[X\C > Pi" in Mp(Mn), every starting event of B\ must be an o, except in the last case where it may also be an X. No place may ever suspend transmission or reception of an SP report, for the recipient of the report might otherwise fail to detect the SP in time. Hence transmissions and receptions in an interrupted process must be allowed to overtake actions in the interrupting process. In the case of multiple consecutive instances of an interrupting process, receptions in each of them must be allowed to overtake non-SP actions in the preceding ones. In the distributed implementation of a "Pi [> P2", there are cases where it is necessary that a place a priori abandons execution of Pi. Hence Mapping 17 For every p, if a B in Mn is a "Pi [X > P2 ", MP(B) is "if EP(B) then Mp(P2) else rename Ri,P(B) in rename R2fP(B) in Mp(Pi) endren [X\(Ci,p(B) U C2,p(P)) > Mp(P2) endren endif", where R2jP renames every G in C?(Mp(Pi)) into a different G' not in £?(Mp(P2)), Ri,p(b) restores the original names of the gates, Ci,p(P) lists all the pairs (G1, G2) with G\ in ( 6); c; d" with a, b and c at a p and d at a p, it is appropriate that Mp/(6) is equivalent to "null". Within an "Mp/(a; stop)[> Mp/(b)", such an Mp/(b) would be unable to execute the required 5 [4]. Keeping just Mp/ (b) yields a correct Mp/ ((a; stop) [> b). 4 Semantic Aspects of Protocol Derivation Let I denote an instance of a P in Mn. An I of a P of the form "SP[E]" is an A. For an /, let M(7) denote the corresponding subprotocol of M(S,rv), i.e. the corresponding instance of M(P), with each Mp(/) denoting the corresponding instance of MP(B). In the particular case of an I of the form "loop P endloop" or "/i[X > P", P has an infinite series of instances, where in a corresponding "loop MP(B) endloop" or "Mp(/i)[X > Mp(P)", the instance of Mp(B) corresponding to the n-th instance of P is the n-th one, while in the case of an Mp(7i [X > P) reduced to Mp(P), the process corresponds to the first instance of P. Let s and sf denote two different SPs in Mn. For an 5, let Prt(s) list the participating A. An s is uniquely determined by Prt(s) and by the data it carries (including, thanks to CI, its AET). For an I, let Prt(s, I) list the A in Prt(s) which are subprocesses of I. With such detailed characterization of SPs, Srv is completely deterministic, so that the problem of its distributed implementation reduces to proper implementation of its individual runs p, prevention of non-determinism in individual Mp(Srv), and securing that time constraints of individual Mp(Srv) and the medium suffice for proper resolution of global conflicts. The more urgent the SPs of Srv' are, the smaller is the number of the possible runs, i.e. the easier it is to satisfy the rules below, i.e. the lesser is the need for inter-place communication. Example 9 Take "a@!0; 1" with aatap and b at a p. If a at time 0 is not urgent, its invocation is not mandatory, so that, to satisfy the empty p, p must refrain from executing b at time 1 before receiving a report on a. If a is urgent, the empty p is impossible, and hence the report not necessary. To prevent local non-determinism, we must prevent ambiguous transitions, hence Rule 4 For every p, ~M.p(Srv) is forbidden to have a state in which two or more outgoing transitions would represent receptions with identical gate and data. For a p, let Excp list, in the order of occurrence, the executed SPs. For an I, let Excp(I) be the projection of Excp onto the SPs s with a non-empty Prt(s, I). For a p, let Enbp list the I enabled during the run. For an I in an Enbp, let Atp(I) denote the time when it gets enabled in p. For an /, let Var (I) list the variables visible and not local to the process. For an I in an Enbp, let Inp(I) for every V in Var (I) provide its value upon enabling of I in p, if not undefined. For a p, let MP(I) denote Mp(/) started with the data in Inp(I). For each particular p, the expected actions ofM(Mn) are the following: For every s at a p at a t in Excp, it is expected that with A in Prt(s) execute s and promptly report it as specified, while for every p', it is expected that Mp,(A) with A in Prt(s) receive the incoming reports on s at t' with (t < t' < t + dp,p ), i.e. immediately upon arrival, in a manner maintaining communication closedness of individual M(A). For every p and p, we expect and will secure that Mp(Srv) proceeds as follows: 1) Whenever it enables an Mp(Z) with I in Enbp of the form "case ... endcase", "/1O/2" or "choice P[]B endch" with an If the alternative selected in I in p, Mp(/) is, at least virtually, executed as MP(I'). 2) Mp(Mn) executes exclusively the actions it is supposed to execute for p, taking care that its SPs are executed in the order specified in Excp. To be able to ignore the fact that for a p, an Mp(Srv) proceeding as expected might enable an Mp(/) with I not in Enbp, we introduce Rule 5 For every p and p, it must be impossible that Mp (Srv) proceeding as expected for p reaches a state in which it could allow Mp(Mn) to execute an s with an A in Prt(s) not in Enbp. Rule 6 For every p, p, I of the form "I\ [X > B" and the second or a later instance 12 of B in I, if 12 is not in Enbp, it must be impossible that ~M.p(Srv) proceeding as expected for p enables Mp(I2) and subsequently reaches a state in which it could allow Mp(Mn) to execute an s with a non-empty Prt(s, /1). Example 10 Take "a; 6; c" with a and b at a p and cat a p. It is appropriate thatp receives from p a report on b, while reporting of a is not necessary. As a is non-urgent, service users might decide not to invoke it. Executing the empty p, Mp/(a;6;c) operating as described enables Mp/(b) in spite of "b" not in Enbp, but correctly refrains from enabling Mp/ (c). For a p and a p, let Enbp list the I in Enbp with Mp(Z) enabled while Mp(Srv) proceeds as expected for P- Every expectedly enabled Mp(/) must be supplied with the expected input data, hence Rule 7 For every p, p, I in Enbp and V in Var (I), ifV is an input variable of~M.p(I), it must have a value K defined in Inp(I) and when 'M.(Srv) proceeding as expected for p enables Mp(I), the value of its input V must be K. For a p, let Actp list the A which are in Prt(s) of an s in Excp such that s is at p or that it is at a p' with E\ (A) true in Mp, (A) after 5. For an /, let Actp(I) list the A in Actp which are subprocesses of I. To be able to pretend that in every local decision, the place selects exactly the alternative intended for the particular p, we introduce Rule 8 For every p, p and I in Enbp of the form "case... endcase", MP(I) must be equivalent to MP(I') with I' the alternative in I selected in p. Rule 9 For every p, p, I in Enbp of the form "Z1U/2" or "choice P[]B endch", and two alternatives I' and I" of I, if M P(I) allows only M P(I'), I' must be the alternative of I selected in p, or Actpv(I") must be empty and MP(I') equivalent to M£(7"). Rule 10 For every p, p and I in Enbp of the form "Zi [X > B", if M£(/) omits Mp(ii), Actp(h) must be empty and Mp(B) unable to raise X. If an ~M.P(A) is supposed to perform an action, it must be timely enabled and while the action is still pending, not suspended permanently or too long, hence Rule 11 For every p, p, s at a t in Excp and A in Prt(s), if A is in Actp, it must be in Enbp and if s is at p, it must be impossible that 'M.p(Srv) proceeding as expected for p fails to enable MP(A) at t or earlier. Rule 12 For every p, p, I of the form "/1 [X > B ", consecutive instances /2 and /3 ofB in I, s at pat at in Excp(h) and sf in Excp(l2) executed before s, if Actp (12) is non-empty, it must be impossible that Mp(,SVv) proceeding as expected for p fails to enable Mp(/3) at t or earlier. Rule 13 For every p, p, I of the form "I\ [X > B ", consecutive instances /2 and /3 of B in I, s in Excp(h), sf at a t' in Excp(l2) with a non-empty (Prt(sf)P\ Actp(l2)), and A in Prt(s,Ii), if s is at p at t' with an Eiy(A) true in Mp(A) after s, or if it is at a p at at with (t -\-dp ,p > t') and Ei}P(A) true in ~MP, (A) after s, /3 must be in Enbp. Example 11 Take "B\[X > B2" with B\ an "(a;stop)", B2 a "(6; ((c; raise X) [] (d; e; stop)))" and a to d at a p and reported to a p , the executor of e. If first p executes a, b and d and reports them to p , the next event might be reception of the report on b. Upon the event, p suspends Mp/(i?i), but remains ready to receive the report on a. If its reception is the next event, it erroneously resolves the choice in Mp/(i?2) in favour of Mp/ (c; raise X), because the reception is legal only iJMp/ (B1) is actually resumed later on. Consequently, p fails to receive the report on d and execute e. Subprotocols synchronized on a transmission gate must properly co-operate on it, hence Rule 14 For every p, s on a gate S at a p in Excp, non-empty subset a of Prt(s) and destination p , if~M.p(A) with A in a are synchronized on gate sps, the value of EijPf (A) after s in Mp(A) must be the same for every A in a and if it is true, there must be a "V2,..., V„ " simultaneously satisfying E2,p' (A) after s in all Mp(A) with A in a. Places must not be too selective about the messages they want to receive, hence Rule 15 For every p, s at a pat at in Excp and A in Prt(s), if an EljPf (A) is true in M P(A) after s, ~MP, (A) must be ready to receive the report on s sent by MP(A) at any t' with (t < t' < t + dv'v ), setting no restrictions on those among the fields V2 to Vn which the medium might pass as a wildcard. The above rules secure that for every p, each Mp(Srv) can proceed as expected. It remains to secure that no unexpected SP occurs and that the expected SPs are executed in the expected global order. The first measure against unexpected SPs are Rules 5 to 7. If an ~M.P(A) is enabled or resumed unexpectedly early, that might also result in an unexpected SP, hence Rule 16 For every p and p, it must be impossible that ~M.p(Srv) proceeding as expected for p reaches a state in which it could allow M p(Mn) to execute an sat at less than the latest Atp(A) of A in Prt(s). Rule 17 For every p, p, I of the form "ii [X > B " and consecutive instances I2 and /3 of B in I, it must be impossible that 'M.p(Srv) proceeding as expected for p suspends Mp(ii) by MP(I2) and subsequently reaches a state in which it could allow Mp(Mn) to execute an s with a non-empty Prt(s,h) earlier than at Atp(l3). Example 12 Take "(a@!2; b)\[b]\b@\l" with urgent a at a p and b at a p. In its only run "a", "b" in "a@!2; 6" is enabled at 2. //Mp/(a!2) immediately terminates, Mp>(b) is enabled already at time 0 and can, without violating Rule 5, erroneously execute b in co-operation with Mp/ (6@! 1). Example 13 Take "((a@!2[]6@!5); stop)[X > (c@!0; d@!3; raise X)" with a at a p, b to d at a p , and d urgent. After c, d must also be reported to p, because otherwise M£(a@!2) might be, without violating Rule 6, resumed in time to execute a. Timely detection of remote decisions is also important for prevention of unexpected SPs, hence Rule 18 For every p, I in Enbp of the form "/1 [] /2" or "choice P[]B endch", and two different alternatives I' and I" of I, if Excp (I") is non-empty, with the first SP in it at a p at a t, then for every p , it must be impossible that Mp/ (Srv) proceeding as expected for p reaches a state in which it could allow Mpf(Mn) to execute an s with a non-empty Prt(s,I') at t or later. Rule 19 For every p, I in Enbp of the form "/1 [X> B" and consecutive instances I2 and /3 of B in I, if Excp(I2) is nonempty, with the first SP in it at a p at a t, then for every p', it must be impossible that Ts/lpr(Srv) proceeding as expected for p without executing an o in Mp/ (/2) reaches a state in which it could allow Mp/ (Mn) to execute an s at a t' with a non-empty Prt(s, /1) and (t' > t), unless /3 is in Enbp with (Atp(l3) < n Example 14 Intherun "c; a; b; e" o/"(c@!0; d@!3; stop)[> (a@!l; e!x@!2)" with a and urgent b at a p, c to e at a p , and dp,p equal to 1, a must be detected by p. However, reporting of a is not necessary, because it is sufficiently early if p' detects the disabling upon receiving a report on b, that is unavoidable because p must receive x. For a p, s and sf in Exec9, A in Prt(s) and A! in Prt(s'), let Grdp(A, A') be true if s' is executed after s and for a superprocess I\ of A and a superprocess /2 of A\ there is an I of the form 1) "trap... is /2 endexn... in I\ endtrap", 2) "/15/2", 3) "loop B endloop" or "/'[X > with h and I2 two different instances of B, or 4) "^[X > B" with I\ an instance of B. For a p and s and s' in Excp, let Grdp(s, s') be true, i.e. s guards s', if Grdp(A, A') is true for an A in Prt(s) and an A! in Prt(s'), or if Excp contains an s" with Grdp(s, s") and Grdp(s", sf). For a p, s and s' in Execp, A in Prt(s) and A! in Prt(sf), let Chnp(A, A') be true if Grdp(A, A') and A is in Actp with p the place of sf. For a p and an s and an sf in Excp, let Chnp(s, sf) be true, i.e. there is a causal chain implemented from s to s\ if Chnp(A, A') is true for an A in Prt(s) and an A! in Prt(s'), or if Excp contains an 5" with Chnp(s, s") and Chnp(ssf). Time constraints might not be sufficient for ordering a pair of SPs, hence Rule 20 For every p and s and sf in Excp with the same AET, Grdp(s, s) requires Chnp(s, s). Example 15 To implement for the run "a; 6; c" of "(a; b) | [b] | (6; c)" with a and c at a p and b at a p a chain from a to c, a must be reported to p and b must be reported to p. If a and b are urgent, the chain serves exclusively for ordering of SPs with the same AET, otherwise also for informing that the immediate guard has actually occurred. Example 16 Take "Bi|[6, e]|B2" with Bx an "((a@!0; 6@!1; stop)[X > (c@!l;e@!0; raise X))", B2 an "(e;b;d;e)", a to d at a p and e at a p. In the run "a; c; e; 6; d'\ proper sequencing of e and b at time 1 requires a chain. We are free to decide whether p should report etop in M(Bi), in ~M(B2) or in both. 5 The Protocol Derivation Process In [9], we prove that given a WFSS and satisfying all the above rules, one obtains a correct implementation of the specified service. However, unlike most of the earlier papers on protocol derivation, we propose no mechanical procedure for translating a WFSS into a protocol, i.e. for choosing the parameters of M. The reason is two-fold. As first, it is often the case that for a given service, a given partition of its SPs and a given communication medium, the given constraints, i.e. the restrictions on the service structure and the rules on the protocol parameters, cannot be satisfied simultaneously, particularly if there are many distributed conflicts and strong time constraints. The necessary compromises on the service, the partition and the medium require intervention of a designer. As second, the given constraints can typically be satisfied in many different ways, with no one indisputably better than the others. Hence it is advisable to have the constraints handled by a general-purpose constraint solver able to accept additional specific optimisation criteria. Besides in the quality of the derived protocol, one is typically interested also in the complexity of the derivation process. For that reason, we have carefully avoided constraints referring to the global state space of the distributed server, referring exclusively to properties of Srv, of individual sequences of selectively reported SPs, and of individual Mp(Srv) executing their local counterparts. Another measure for decreasing the complexity would be to intentionally reason in a highly compositional way, i.e. to take care not only that M(Srv) correctly implements Srv, but also that individual M (I) in isolation properly implement I. This is the usual approach in protocol derivation, but as such reasoning is less context-conscious, it might result in a less optimal protocol or even in an erroneous conclusion that no feasible protocol exists for the given setting. An important step towards an efficient protocol can be restructuring of Srv without changing its external behaviour, for example • changing the degree to which an inherent parallelism is made explicit, • changing the location of a hidden SP (e.g. to localize a causal relation or a conflict), • enhancing an SP with hidden parameters more accurately reflecting its identity (the information might be needed in a report on the SP), • making a process use a copy of a variable instead of its original, with the copy generated at a carefully chosen point (one can thereby control the point of sending the data to a place needing it), • introducing a dummy SP marking completion of a group of SPs at a particular place, so that completion of the group can be reported by reporting the dummy (facilitates the protocol optimization proposed in [10]), or • changing termination of a process into a dummy SP indicating that the process is ready for disabling, with an auxiliary process detecting the SP and performing the disabling (facilitates the protocol optimization proposed in [11], helpful particularly for processes comprising terminating and non-terminating alternatives or alternatives with different termination events). Ideally, the constraint solver would co-operate with an expert system optimizing the structure of Srv. 6 Concluding Remarks The proposed method generates protocols securing that any SP legal during a particular time interval is available to service users through the entire interval, while [2] and [1] strive only for occasional availability. The method accepts a much wider class of service processes. Another contribution is a flexible SP-reporting scheme with plenty of space for protocol optimization, particularly for message re-use and prevention of duplicate causal chains and unnecessary reports on urgent SPs and remote decisions. 7 References [1] M. Kapus-Kolar, "Compositional service-based construction of multi-party time-sharing-based protocols," IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, vol. E86-A, no. 9, pp. 2405-2412, 2003. [2] A. Nakata, T. Higashino, and K. Taniguchi, "Protocol synthesis from timed and structured specifications," Proc. ICNP'95, pp. 74-81, IEEE Computer Society, 1995. [3] T. Bolognesi and E. Brinksma, "Introduction to the ISO specification language LOTOS," Computer Networks and ISDN Systems, vol. 14, no. 1, pp. 25-59, 1987. [4] ISO/IEC, Enhancements to LOTOS (E-LOTOS), ISO/IEC 15437, ISO - Information Technology, 2001. [5] A. Verdejo, E-LOTOS: Tutorial and Semantics, M.S. thesis, Universidad Complutense de Madrid, 1999. [6] M. Kapus-Kolar, "Towards weak sequencing for E-LOTOS," Computer Standards & Interfaces, vol. 28, no. 1, pp. 59-73, 2005. [7] C. A. Vissers, G. Scollo, M. van Sinderen, and H. Brinksma, "Specification styles in distributed systems design and verification," Theoretical Computer Science, vol. 89, pp. 179-206, 1991. [8] M. Kapus-Kolar, A Correction to Compositional Service-Based Construction of Multi-Party Time-Sharing-Based Protocols, Jožef Stefan Institute tech. rept. #8896, 2003. [9] M. Kapus-Kolar, E-LOTOS-Based Compositional Service-Based Synthesis of Multi-Party Time-Sharing-Based Protocols, Jožef Stefan Institute tech. rept. #9200, 2006. [10] F. Khendek, G. von Bochmann, and C. Kant, "New results on deriving protocol specifications from service specifications," Proc. SIGCOMM'89, pp. 136-145, ACM, 1989. [11] M. Kapus-Kolar, "More efficient functionality decomposition in LOTOS," Informática, vol. 23, no. 3, pp. 259-273, 1999. Monika Kapus-Kolar received her B.Sc. degree in electrical engineering from the University of Maribor, Slovenia, and the M.Sc. and Ph.D. degrees in computer science from the University of Ljubljana, Slovenia. Since 1981 she has been with the Jožef Stefan Institute in Ljubljana. Her current research interests include formal specification techniques and methods for distributed systems development.