(PDF) A Users Manual

TAV (Tools for Automatic Veri cation) Users Manual Jens C. Godskesen Kim G. Larsen Michael Zeeberg Abstract This report gives a user introduction to the tools of Tav, a veri cation system for parallel and nondeterministic systems within the calculus of CCS. In particular Tav contains tools for deciding various notions of bisimularity between processes, and contains tools for model{checking with respect to a rather powerfull (recursive) modal logic. A distinctive feature of the tools of Tav | important from a development point of view | is, that they all o er explanations for the answers they give. 1 Contents 2 Contents 1 Introduction 3 2 Using The System 5 3 The Language for Processes 7 3.1 Predicates for analyzing a process : : : : : : : : : : : : : : : : : : : : 4 Arguing for Bisimularity 4.1 Strong Bisimularity 4.2 Weak Bisimularity 8 12 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5 Arguing against Bisimularity 5.1 Strong Hennessy{Milner Logic 5.2 Weak Hennessy{Milner Logic 12 14 16 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 Arguing for Modal Properties 6.1 Recursive Hennessy-Milner Logic 6.2 The Modal Property Checker 16 17 19 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 Examples 7.1 A Simple Protocol 7.2 The Dining Philosophers 7.3 Hymans Mutual Exclusion Algorithm 19 21 27 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 27 31 36 3 1 Introduction We think of program development as being logically divided into three phases: a speci cation phase, in which a collection of desired properties of the nal program is described; the implementation phase, in which the program or process with the desired properties is being developed; and nally, the veri cation phase, which consists of a formal justi cation of the correctness of the designed implementation with respect to the initial speci cation. For the development of parallel programs, it has become evident that the analyses involved in the veri cation phase is often tedious and delicate even for moderate size examples. Thus, it is rather clear that computer assistance is essential; not just to ensure the correctness of the veri cation, but even to make the analyses feasible. Furthermore, to be an aid in the implementation phase, it is important that the tools provided do more than just check and report the correctness (or lack of correctness). The tool must also provide explanations of the answers they give: a correct design has most likely been preceded by several incorrect attempts; knowing why these attempts where erroneous would obviously be of great help in the pursuit of a correct one. Furthermore, the explanations given should be concise in the sense that they contain no redundancies or irrelevant information. The Tav system 1 is based upon the framework of CCS (Calculus of Communicating Systems [Mil80]), and o ers a number of tools for analysing and arguing about properties of CCS{processes. In particular, there are tools for deciding (strong and weak) bisimularity [Mil80, Mil83, Par81] between processes, and tools for modelchecking, i.e. deciding whether a given process satis es a given modal property. What mostly distinguishes our system from other similar systems, such as the Concurrency Workbench (Edinburgh and Sussex University) [CPS88] and the AUTO system (INRIA, Sophia{Antipolis) [LMV88], is that the tools of Tav all o er explanations for the answers they give. The tools of Tav for bisimularity will try to construct a \minimum" (= concise) (strong or weak) bisimulation using the algorithm of [Lar86]. This is in contrast to the algorithm underlying [CPS88] and [LMV88], which tries to nd the \maximum" bisimulation using a generalized partitioning algorithm [KS, PT87]. In case the two given processes are not bisimular, the tools of Tau will return a distinguishing modal property using the Characterization Result of Milner and Hennessy in [HM85]. An earlier versions of this part of the Tav system was implemented by Michael Hillerstrom as part of his Masters Thesis [Hil87]. Tav provides tools for automatically checking whether a given CCS{process satis es 1 The Tav system has been implemented as part of the Tau{project [LS87], a project supported by the FTU{program under the Danish Research Council. 4 1. Introduction a given modal property. The language for describing modal properties is that of Hennessy{Milner Logic [HM85] extended with recursion [Lar88], which provides a rather powerful speci cation language in terms of expressibility. In particular the logic allows the speci cation of several safety and liveness properties. A proof in the proof system of [Lar88] is (automatically) returned in case the process satis es the given property. Otherwise, i.e. if the process does not satisfy the given property, a proof of satis ability of the dual property may be obtained. This manual is organized as follows: In section 2 we describe how to start (and terminate) the Tav system. Section 3 describes the syntax used for processes together with a number of basic predicates for exploring processes operational behaviour. Sections 4 and 5 present the tools for deciding and arguing about bisimularity together with a minimal theoretical introduction. Section 6 describes the tools in Tav for modelchecking. In section 7 a number of (larger) examples has been worked out using the various tools of Tav. 5 2 Using The System This section describes how to initiate the system Tav, written in C{Prolog [CM81]. Tav o ers the user an interactive veri cation tool running from inside the C{Prolog programming environment, giving immediate access to all C{Prolog facilities in addition to prede ned Tav{system predicates. To start the system you type shell% cprolog TAV which loads C{Prolog together with the Tav-system. Now you will see C Prolog version 1.4e.edai % Restoring file /usr/local/lib/cprolog/saved_states.d/Prolog1.4e | ?- and the system is ready to follow your directives. Asking the system questions is exactly as when C{Prolog is asked questions. After the prompt of C{Prolog (?), rst enter your question terminated with period, then type RETURN and the system will answer. The full supply of system predicates will be described in the following sections. If processes exceeding a certain size (approximately 20 states) are to be examined, it is necessary to allocate more space to C{Prolog. Currently, the C{Prolog implementation operates on six stacks, which individually can be assigned an amount of memory, speci ed in Kbyts. The stacks are: a heap (H), a global stack (G), a local stack (L), a trail (T), an atom area (A) and an auxiliary stack (X). Setting the size of the stacks is done by starting C{Prolog with the command shell% cprolog -H N1 -G N1 -L N3 -T N4 -A N5 -X N6 TAV All stacks are as mentioned optional and Ni is speci ed in Kbytes. In case of stack over ow the system abort the execution and leaves an error message informing you about which stack has been lled. Then, the whole system has to be closed down and restarted with a new stack con guration. To quit Tav | and the C{Prolog environment from which Tav is running | give the (standard Prolog) command: ?- halt. Tav has two modes: a process expression mode and a number mode. In the process expression mode (which is default), the analysis of processes operates directly on process expressions. However, such expressions may often be rather large, and to gain eciency Tav o ers you the possibility of assigning numbers to process expressions. To use numbers instead of syntactic expressions in succeeding analyses, turn on the numbermode by: 6 2. Using The System ?- numbmode. When using this mode, one has to be sure that the process under consideration actually has a number. Otherwise a numbering of the states of a process may be achieved by the command: ?- assignnumber(Proc). However, most predicates of the Tav system automatically assigns (unique) numbers to (states of) processes in case no number has previously been assigned. To return to process expression mode type: ?- nonumbmode. As Tav is an interactive system, you may nd it useful to run it from inside (a shell started in) Emacs, as this will allow you to scroll, cut and paste in the output from Tav during execution. The same advantages may be obtained, when running Tav inside Suntools on a Sun Workstation. 7 3 The Language for Processes The language used for expressing processes in the Tav system is essentially CCS as presented by Milner in [Mil80] with some minor modi cations. For each process construction of CCS a corresponding Prolog operator has been introduced. Of course, in this way it is not always possible to achieve standard notation | e.g. the standard CCS{notation for pre xing, \.", has a special meaning in Prolog. The notation used and the corresponding standard notation can be found in gure 1. Construction Inaction Pre xing Summation Parallel Restriction Renaming CCS TAV N IL a:p p q pjq pnS c p a=b + [ ] nil a;p p+q p/q pnS p-[a:=b] Figure 1: CSS{notation versus Tav{notation Complementary actions (used in the operational semantics of parallel processes in order to allow synchronization) are represented by two predicates in and out. In addition to these synchronizable actions, Tav includes actions which cannot be synchronized. The action set of processes is thus the set of (lower case) names: atom j in(atom) j out(atom) where atom denotes a standard Prolog atom. A special action is the atom tau, which represents the unobservable action in CCS. In the pre xing construct, a can be any action. Note, that for convenience restriction to is used in Tav rather than restriction from in standard CCS manner. Sets and operations on sets are implemented as lists and operations on lists. The members of S in restriction and the actions in renaming may only be atoms di erent from tau. However, the restriction and renaming extends to all in{ and out{pre xes of the actions involved. Parantheses must be used to resolve ambiguities. However, in order to avoid an excessive use of paratheses the following operator precedence has been introduced: Pre x > Restriction > Renaming > Summation > Parallel The :=: predicate enables (recursive) processes and abbreviations to be declared for later use. To bind the identi er id (which must be a Prolog atom) to the process expression expression, type 8 3. The Language for Processes ?- id :=: expression. All declarations are potentially recursive as the scope rules applied are dynamic. Also, no process identi er may be declared twice. The following lists some sample process expressions in Tav: a;nil in(a);(b;nil + out(c);nil) (in(a);nil / in(b);nil / out(a);nil) \ [b] and sample declarations of process identi ers: ?- p :=: in(a);(b;nil + out(c);p). ?- q :=: (in(a);nil / out(a);q) \ [b]. To get information about the number (and possible declaration) of a process, use the predicate procinfo with the process expression or number as argument (depending on whether or not Tavu is in numbmode). A complete listing of all declarations made, can be obtained by the predicate procinfo. If more extensive analyses are to be performed on a process, one may nd use of the predicate savestate, which given a lename saves all precomputed datastructures on that le for later use. To regain these datastructure without a new precomputation, use the predicate load with the lename as argument. 3.1 Predicates for analyzing a process Tav contains a number of predicates for exploring the operational behaviour of processes. All these predicates apply to numbers or process expressions depending on whether or not the numbermode is switched on. Also, termination is only guaranteed for nite state processes (i.e. static constructs should not be mixed with recursive declarations), and provided all recursive declarations are well{guarded (see [Mil80]). The predicate moves provides information about the immediate derivatives of a process according to the standard transition relation ?! of CCS. That is, q appears a in the listing of moves(p,a) just in case p?! q. moves(p,all), where all is a distinguished symbol, lists all derivatives of p under all actions. 3.1 9 Predicates for analyzing a process ?- moves(in(a);b;nil + out(c);nil, in(a)). -in(a)-> b;nil ?- moves(in(a);b;nil + out(c);nil, all). -in(a)-> b;nil -out(c)-> nil Similarly, the predicate obsmoves provides information of the immediate derivatives of processes under the observational transitional relation =), where p=)p means a a n p?!p for some n 0, and p=)p means p=)q ?!q =)p for a 6= . The output is formatted as for moves with the one di erence that -act-> is substituted with =act=>. Note also, that in the context of observational derivatives, tau plays the role of the (standard) empty string of observable actions . As for moves one can use the all option to obtain all observational derivatives. The predicate states returns the statespace of a process. Note, that in addition you get numbers assigned automatically to the states of the process. 0 0 0 0 0 ?- states(in(a);(b;nil + out(c);nil)). 1 = nil 2 = b;nil+out(c);nil 3 = in(a);(b;nil+out(c);nil) To obtain full behavioral information about a process, Tav includes two predicates transsys and obstranssys. transsys(p) simply prints out the transition system for p with respect to the standard operational semantics given by ?!. Similarly, obstranssys(p) prints out the transition system for p with respect to =). The output is as follows: 10 3. The Language for Processes ?- transsys( (in(a);nil / in(b);nil / out(a);nil)\[b] ). State Transitions 4 = (in(a);nil/in(b);nil/out(a);nil)\[b] tau -> 3, in(b) -> 1, 3 = (nil/in(b);nil/nil)\[b] in(b) -> 2, 2 = (nil/nil/nil)\[b] 1 = (in(a);nil/nil/out(a);nil)\[b] tau -> 2, The predicate findpath returns some path between two process in case any such exists. Similarly, the predicate taupath returns the shortest tau{path between two processes. ?- findpath( (in(a);nil / in(b);nil / out(a);nil)\[b], (nil / nil / nil)\[b] ). -tau-> (nil/in(b);nil/nil)\[b] -in(b)-> (nil/nil/nil)\[b] Finally, Tav provides predicates, deadlock and divergence, for testing processes for the properties of deadlock and divergence. These properties may alternatively 3.1 Predicates for analyzing a process 11 be tested by the model checker to be describe in later sections. However it is more ecient to apply deadlock and divergence, which are especially optimized to decide these properties. A process is deadlocked if it by a series of moves may enter a state with no derivatives. A process is capable of diverging, if it may reach a state from which an in nite tau computation can take place. For nite{state processes, this means that the state{space of the processes must contain a tau cycle. ?- p :=: in(a);in(a);p + b;nil. ?- q :=: out(a);out(a);q + b;nil. ?- deadlock( (p/q)\[b] ). -b-> (nil/q)\[b] -b-> (nil/nil)\[b] ?- diverge( (p/q)\[b] ). -tau-> (in(a);p/out(a);q)\[b] -tau-> (p/q)\[b] 12 4. Arguing for Bisimularity 4 Arguing for Bisimularity The notion of bisimularity | introduced by Park in [Par81] and later investigated by Milner [Mil83] | induces an abstracting equivalence on processes identifying processes with \similar" operational behaviour. Assume that the operational behaviour of processes is given by some transition relation ?!. Then, a bisimulation R is a set of pairs of processes, such that whenever ( ) 2 R, the following closure conditions hold: P; Q 1. Whenever P 2. Whenever Q a a ?! , then ?! P 0 Q a a ?! , then ?! Q 0 P Q P 0 with ( 0 with ( 0 0 ) 2 R for some , and 0 0 ) 2 R for some . P ;Q P ;Q Q P 0 0 Two processes and are said to be bisimular in case they are contained in some bisimulation. It may be shown that bisimularity is in fact an equivalence between processes, and moreover is itself a bisimulation. For a more thorough explanation we refer the reader to [Par81, Mil83, Lar87]. We may now apply the general notion of bisimularity to either the transition relation ?! from the standard operational semantics of CCS (corresponding to the system predicate moves) or to the derived observational transition relation =) (corresponding to the system predicate obsmoves). We shall refer to the resulting equivalences on CCS{processes as strong bisimularity and weak bisimularity. The Tav system includes predicates for constructing (\minimal") strong and weak bisimulations containing a given pair of CCS{processes. In case the processes are not bisimular, a distinguishing modal property will be generated. This case will be dealt with in details in the next section. The fundamental algorithm underlying this part of the Tav system will terminate provided the processes compared are both nite{state and only involves well{guarded recursive de nitions. More detailed descriptions may be found in [Lar86, Hil87, Lar] P Q 4.1 Strong Bisimularity Strong bisimularity is decided by the predicate processes as arguments. , which takes two CCS{ sbisim 4.1 Strong Bisimularity 13 ?- clock1 :=: sec;clock1. ?- clock2 :=: sec;sec;clock2. ?- sbisim(clock1,clock2). Constructing derivation table for clock1 Constructing derivation table for clock2 Searching for a strong bisimulation... Here is a listing of a strong bisimulation of the processes clock1 and clock2 0 clock1 clock2 LHS--> sec ==> 1 RHS--> sec ==> 1 1 clock1 sec;clock2 LHS--> sec ==> 0 RHS--> sec ==> 0 In the above example, two recursive clock{processes has been de ned: a simple clock, clock1, with only one state, and a more complicated clock, clock2, with two states. Clearly, the two processes behaves identical: they can perform the basic action sec ad in nity. This expectation is con rmed by the call of the predicate sbisim, which returns a (strong) bisimulation consisting of the two pairs, (clock1,clock2) and (clock1,sec;clock2) (numbered 0 respectively 1). Each pair of processes in the bisimulation is succeeded by information explaining how the closure conditions required of a bisimulation is ful lled for that particular pair. Here LHS (RHS) refers to the rst (second) process of the pair. For pair 0 then, LHS--> sec ==> 1 indicates, that clock1 can perform an sec{action (with respect to the transition relation ?!) which is matched by a sec{action of clock2 resulting in the pair 1. Similarly, RHS--> sec ==> 1 means, that clock2 can perform an sec{action being matched by clock1 with a resulting new pair 1. The information Constructing derivation ... listed immediately after the call sbisim(clock1,clock2) indicates that the operational behaviour of clock1 and clock2 are being precomputed and saved in internal datastructures (in particular the states of the processes are being represented by unique numbers). Later analyses of the processes will utilize these precomputed tables (and in doing so gaining in 14 4. Arguing for Bisimularity time{eciency). Thus, repeating the call following listing: sbisim(clock1,clock2) will give the ?- sbisim(clock1,clock2). Using existing derivation table for clock1 Using existing derivation table for clock2 Searching for a strong bisimulation... Here is a listing of a strong bisimulation of the processes clock1 and clock2 0 clock1 clock2 LHS--> sec ==> 1 RHS--> sec ==> 1 1 clock1 sec;clock2 LHS--> sec ==> 0 RHS--> sec ==> 0 4.2 Weak Bisimularity Weak bisimularity is decided by the predicate wbisim, which takes two CCS{processes as arguments. In the example below, medium represents a disposable medium: it can take in a message on a and deliver the message on b after which it will die. delay-medium consists of a \sequential" composition of two disposable media: the message delivered by the rst medium is accepted by the second. Thus, from an observational point of view, the two processes ought to be equivalent. This is con rmed by the answer to the call wbisim(medium,delay-medium), which returns a (weak) bisimulation consiting of 4 pairs. The listing ...extending it to an obdertable indicates that the observational behaviour of the two processes (corresponding to the transition relation =)) is being precomputed and saved for future analyses of the two processes. 4.2 Weak Bisimularity ?- medium :=: in(a);out(b);nil. ?- delay-medium :=: (medium-[b:=c] / medium-[a:=c])\[a,b]. ?- wbisim(medium,delay-medium). Constructing derivation table for medium ...extending it to an obdertable. Constructing derivation table for delay-medium ...extending it to an obdertable. Searching for a weak bisimulation... Here is a listing of a weak bisimulation of the processes medium and delay-medium 0 medium delay-medium LHS--> in a ==> 1 RHS--> in a ==> 1 1 out b;nil (out b;nil-[b:=c]/medium-[a:=c])\[a,b] LHS--> out b ==> 2 RHS--> epsilon ==> 3 2 nil (nil-[b:=c]/nil-[a:=c])\[a,b] 3 out b;nil (nil-[b:=c]/out b;nil-[a:=c])\[a,b] LHS--> out b ==> 2 RHS--> out b ==> 2 15 16 5. Arguing against Bisimularity 5 Arguing against Bisimularity Hennessy and Milner presented in [HM85] a simple modal logic | referred to in the following as Hennessy{Milner Logic or in abbreviated form HML | for expressing properties of processes. This logic provides an alternative characterization of bisimulation, in the sense that two processes are bisimular just in case they enjoy exactly the same properties expressible in the logic (strictly speaking this result is subject to a technical condition known as image{ niteness. However, this condition is satis ed by all nite{state processes). The negative form of this statement brings further clarity to its usefulness: two processes are non{bisimular just in case they are distinguished by some property of the logic. Hence, it follows, that we may use such a distinguishing property as an explanation in the case two processes are non{bisimular. 5.1 Strong Hennessy{Milner Logic The formulae of (strong) Hennessy{Milner Logic consists of simple modal expressions built up according to the following abstract syntax, where a2 Act: F ::= tt | ff F or G | | F and G | <a>F | [a]F A formula is intended to describe a collection of properties that a sought process should have. A process is said to satisfy a formula if it enjoys the corresponding properties. The formula tt is satis ed by all processes, whereas no process will satisfy ff. Satisfaction of conjunctive (F and G) and disjunctive (F or G) formulae is the standard. To satisfy the modal formula <a>F, a process p must possess some a a{transition, p ?! p , leading to a state, p , satisfying F. Dually, for a process p to a satisfy a modal formula [a]F, for any a{transition, p ?! p , p must satisfy F. The following examples show the kind of properties that may be expressed in HML: <a>tt is satis ed provided the process can perform a. Dually, [a]ff indicates that the process cannot perform a. <a>[b]tt requires ability to perfom a and reach a state which is deadlocked on b; and [a]<b>tt ensures that all a{transitions lead to states, where b is enabled. The system predicate sbisim produces a distinguishing property of strong HML, for processes not being strong bisimular. This is demonstrated in the classical example below: 0 0 0 0 5.2 17 Weak Hennessy{Milner Logic ?- sbisim( a;(b;nil + c;nil) , a;b;nil + a;c;nil). Constructing derivation table for a;(b;nil+c;nil) Constructing derivation table for a;b;nil+a;c;nil Searching for a strong bisimulation... The process: a;(b;nil + c;nil) enjoys some properties which the process a;b;nil + a;c;nil doesn't. One property is: <a>(<c>tt and <b>tt) In fact, the property produced by sbisim is always enjoyed by the rst process. Thus, reversing the order of the processes yields: ?- sbisim(a;b;nil + a;c;nil , | a;(b;nil + c;nil)). Using existing derivation table for a;b;nil+a;c;nil Using existing derivation table for a;(b;nil+c;nil) Searching for a strong bisimulation... The process: a;b;nil + a;c;nil enjoys some properties which the process a;(b;nil + c;nil) doesn't. One property is: <a>[c]ff 5.2 Weak Hennessy{Milner Logic Using the predicate wbisim, non{bisimular processes in the weak sense may similarly be distinguished by properties of the following weak version of HML: F ::= tt | ff F or G | | F and G | <<a>>F | [[a]]F 18 5. Arguing against Bisimularity The interpretation of formulae of weak HML is exactly as for strong HML, but with the modalities <<a>> and [[a]] referring to the observational transition relation =). ?- medium :=: in(a);out(b);medium. ?- delay-medium :=: (medium-[b:=c] / medium-[a:=c])\[a,b]. ?- wbisim(delay-medium,medium). Constructing derivation table for delay-medium ...extending it to an obdertable. Constructing derivation table for medium ...extending it to an obdertable. Searching for a weak bisimulation... The process: delay-medium enjoys some properties which the process medium doesn't. One property is: <<in(a)>><<in(a)>>tt In the above example, reusable versions of the medium from the previous section is considered. However, in this case a delayed medium is not weakly bisimular to an ordinary medium. The distinguishing property displayed shows that delay-medium is able to take in two messages on a, without delivering messages on b. Clearly, this is a property not enjoyed by medium. The tools for modelchecking to be presented in the next section, may now be used to give further explanation as to why delay-medium enjoyes the displayed property. 19 6 Arguing for Modal Properties In this section we argue for an extension of HML with recursion. We de ne the language for recursive properties and describe how it may be (automatically) checked, if a process enjoys one of these properties. 6.1 Recursive Hennessy-Milner Logic Considered as a speci cation language Hennessy{Milner Logic is too weak, since any formula only says something about the rst few actions (depending of the \modal depth" of the formula) of a process. However, most interesting processes have innite life time (i.e. they can act for ever), and obviously we would like to de ne properties characteristic of the full and possibly in nite behaviour of a process. In particular, we want to express properties which hold invariantly | i.e. at every moment throughout the life time of a process | or properties which may possibly hold | i.e. at some unspeci ed moment during the life time of the process. Consider the process system de ned by the two following process declarations: ?- p :=: a;p. ?- q :=: a;q + a;nil. Suppose we would like to specify the invariant property inva, saying that the process is always capable of performing an a action; and dually the property posa, which expresses the possibility of a deadlock on a during execution. It should be obvious that p enjoys inva but not posa, and similarly, that q enjoys posa but not inva. Unfortunately, neither inva nor posa is expressible in ordinary HML. To increase expressibility, we extend the logic with recursion. Intuitively a process p satis es inva if it has the property <a>tt and any state immediately succeeding p satis es inva. Similarly, a process p satis es posa if either p has the property [a]ff or at least one state immediately following p has the property posa. From this it is fairly easy to see that inva and posa must satisfy the following laws: inva posa = = <a>tt and [act]inva [a]ff or <act>posa where <act>F = Wa2Act <a>F and dually [act]F = Va2Act [a]F . Now, we want these equations to de ne the semantics of inva and posa. However, this immediately raises the questions of whether the equations have solutions at all, and if so, which solution to take. 6. Arguing for Modal Properties 20 Both equations are (semantically) of the general form: S = O(S ) (1) where S is the set of processes satisfying the recursive property, and O is a set operator derived from the right{hand side of the equation. Now, it can be argued that any such operator O de neable in HML is a monotonic operator on sets. Thus, it follows from standard xed point theory [Tar55] , that O has a minimal and a maximal xed point. In our particular case it turns out that inva should be interpreted with respect to a maximal solution and that posa should be interpreted with respect to a minimal solution. Doubtlessly, it is not always clear which solution to choose, but in general we have that safety properties requires the use of maximal solutions, whereas liveness properties should be interpreted by a minimal solution. In the Tav system, recursion is introduced by allowing identi ers (Prolog atoms) to occur in our logic. Recursive properties are then declared by binding identi ers to formulae expressions (possibly containing identi ers). The predicate => is used to indicate that the maximal solution is wanted, whereas <= indicates the minimal solution as the intended one. Thus, the properties inva and posa can be de ned in the Tav system as follows: ?- inva => "<a>tt and [act]inva". ?- posa <= "[a]ff or <act>posa". Note that the formula expression being bound must be surrounded by quotation marks (formulae expressions requires parsing, as the connectives of HML are not implemented as Prolog operators). To enable such properties to be expressed more conveniently, we extend HML with a number of standard operators from the world of Temporal Logic (e.g. [BAPM83]). This extension is a pure syntactic one | in fact for each of the new temporal operators there exist an equivalent recursive scheme: INV F and inv F are invariant properties. Informally INV F , denoted strong invariance, is satis ed by a process if any state of that process enjoys the property F . In particular we have that inva alternatively may be characterized as INV <a>tt. Weak invariance, inv F , is satis ed by a process if it has some computation (a maximal nite or in nite derivation sequence) on which all processes satis es F . A process satis es even F if F holds eventually; i.e. if for all computations of the process, F holds at some point. Similarly, a process satis es poss F , if there is some computation where F holds at some point. The property posa can then alternatively be de ned as poss [a]ff. 6.2 21 The Modal Property Checker Finally, a process satis es UNTIL and until | denoted as holds strong until and as holds weak until respectively | if for all computations holds until holds. However, for weak until is allowed to hold throughout a computation without ever being satis ed in contrast to strong until where it is required that eventually holds for all computations. The full language for modal properties is now: F G G F F G F G F G F G G F ::= X | tt F and G | F or G [a]F | <<a>>F INV F | inv F poss F | F UNTIL G | ff | <a>F | [[a]]F | even F | F until G | | | | where X is an identi er assumed to be previously declared (by the use of either => or <=), and a is any action or the symbol act. 6.2 The Modal Property Checker The implementation of the Modal Checker is based on the proof system presented in gures 2 and 3. This proof system originates from [Lar88]. From the rules in the proof system one may infer assertions of the form ? ` : , where ? is a set of assumptions, is a process and is a formula. Every rule in the proof system conforms to the following general scheme: ?1 ` 1: 1 ?n ` n : n ?` : where is the name of the rule and is a side condition which must be ful lled in order to apply the rule. Whenever the side condition is ful lled, one may infer from the assertions above the line the assertion below the line. Occassionally there are no assertions above the line, in which case the assertion below the line is trivially inferable and the rule degenerates to an axiom. The rule tt, is an axiom stating that for any set of assumptions ? and any process , ? ` : tt may directly be inferred. The rule <> says, that in order to infer ? ` : <a> you must establish ? ` : for some process which according to the side condition should be derivable from by an action . There are three rules for inferring ? ` : , when is a recursively speci ed property. If ( X the rule Min allows you to perform the inference from the p F p F N N p p F ::: p F R p F R p p F p 0 F p p a p X X F X 0 6. Arguing for Modal Properties 22 tt ? ` p: tt and ? ` p: F ? ` p: G ? ` p: F and G or ? ` p: F ? ` p: F or G <> ? ` p :F ? ` p: <a>F [] ? ` p1 : F : : : : : : ? ` p n : F ? ` p: [a]F Max1 ?; p: F Max2 ?; p: X ` p: FX ? ` p: X Min ? ` p: FX ? ` p: X ? ` p: G ? ` p: F orG 0 p a ?! 0 p f p1 ; : : : ; p ` : p F X X ) X F ( X F Figure 2: Proof System ng = fp 0 a j ?! g p p 0 6.2 23 The Modal Property Checker INV ?? ` p: F ?? ` q1 : INV F : : : ; ?? ` qn : INV F ? ` p: INV F inv ?? ` p: F ? ` p: inv F 8 a: p a 6?! ?? ` p: F ?? ` q: inv F ? ` p: inv F ? ` p: F ? ` p: even F even ? ` q1 : even F : : : ? ` qn: even F ? ` p: even F n > 0 ? ` p: F ? ` p: poss F poss ? ` q: poss F ? ` p: poss F ? ` p: G ? ` p: F UNTIL G UNTIL ? ` p: F ? ` q1 : F UNTIL G : : : ? ` qn : F UNTIL G ? ` p: F UNTIL G ?? ` p: G ? ` p: F until G until ?? ` p: F ?? ` q1 : F until G : : : ?? ` qn : F until G ? ` p: F until G a where 2 f 1 ?! g, and ?? means that ? ng = f j 9 has been augmented with the correctness assertion : occurring in the sequent of the conclusion (in accordance with the rule for maximal xed points). q q ;:::;q p 0 a: p p 0 p F Figure 3: Proof System 6. Arguing for Modal Properties 24 assertion ? ` : X . The rule Max2 is quite similar, allowing almost the same inference whenever ) X . However for maximal speci ed properties assertions are much easier to establish due to the rule Max1, which simply says that ` : may be inferred directly provided : is included in . The rules for the temporal operators in gure 3 are straightforward formalizations of the brief semantic description given previously. As each temporal operator may be represented by a recursive scheme (see [Lar88]), the rules are in fact derivable from the rules of gure 2. The proof system presented is sound and complete in the sence that an assertion ; ` : is derivable in the system if and only if belongs to the semantic interpretation of . This is what makes the system a correct basis for The Modal Checker. The Modal Checker has two modes, one which just decides if a process enjoys a property and one which both decides and moreover displays a proof with : as conclusion. Suppose we would like to ask the system if the process de nd above has the property INV <a>tt. This is carried out by the order: p F X F p F p F p F p F p F p F p ?- [] >- p : "INV <a>tt". Here [] indicates the empty set of assumptions, and >- the turnstyle ` Now, assume is a process which satis es , then the system o ers an explaination as to why this is the case. To get such an explanation one must shift to why-mode by using the predicate why. To return to the original mode (no{why mode), use the predicate nowhy. In why{mode the Modal Checker will display a proof (if any such exists). By a proof we understand a tree-like structure, where nodes are sequents, ? ` : , and all parents are inferable from their children by some rule of the proof systems. Thus all leaves must be axioms. Now, consider the proof for ; ` : , i.e. ; ` : is the root in that proof. Such a proof must exists due to the soundness and completeness of the proof system. Suppose ; ` : is inferable from its children, ?1 ` 1 : 1 ?n ` n : n by some rule . In that case The Modal Checker will display such a proof as: : p F p F p F p F p F R p F p F ;:::; 6.2 25 The Modal Property Checker >- P : F by R as >- P1 : F1 by R1 as Proof1 and and >- Pn : Fn by Rn as Proof n where Proof is the display for the proof for ? ` p : F . We leave out the assumption sets and just write ^ in case they are non{empty, often also R is left out, since the rule applied may be obvious by the structure of F . To improve readability processes are represented by numbers. To obtain the corresponding process expression use the predicate procinfo. The following shows a typical display produced by the Modal Checker (assuming in why{mode): i i i i ?- p :=: a;p. ?- [] >- p : "INV <a>tt". Constructing derivation table for p ...extending it to an obdertable. >- 1 : INV <a>tt as ^ >- 1 : <a>tt as ^ >- 1 : tt is immediate and ^ >- 1 : INV <a>tt is immediate by ^ From the session below it follows, that a;b;nil + a;c;nil has the property <a>[c]ff since it has an a{derivative to b;nil (state number 3), and clearly b;nil has the property [c]ff. 6. Arguing for Modal Properties 26 ?- [] >- a;b;nil + a;c;nil : "<a>[c]ff". Constructing derivation table for a;b;nil+a;c;nil ...extending it to an obdertable. >- 4 : <a>[c]ff as >- 3 : [c]ff is immediate ?- states(a;b;nil + a;c;nil). 1 2 3 4 = = = = c;nil nil b;nil a;b;nil+a;c;nil 27 7 Examples 7.1 A Simple Protocol In this section we analyse the simple protocol rst presented in [Par85]. The protocol consists of three components composed in parallel: a sender, a medium and a receiver. sender accepts an item from the external world by an a-action and passes it to the medium by an out(b)-action after which it waits for either an acknowlegde, in(d), or an error message, in(c), indicating that the item is lost. If the sender receives an acknowlegde it returns to its initial state, otherwise it tries to resend the item. After medium has received a message, in(b), it either looses its information which is signaled by the out(c)-action, or the information gets to the receiver by an out(e)-action. In both cases the medium returns to its initial state. The receiver receives an item by in(e), deliver it to the external environment by f, then it sends an acknowlegdement, out(d), and returns to its initial state. The protocol may now be described as sender :=: a;sender1. sender1 :=: out(b);(in(d);sender + in(c);sender1). medium :=: in(b);(out(c);medium + out(e);medium). receiver :=: in(e);f;out(d);receiver. protocol :=: (sender/medium/receiver) \ [a,f]. where we have restricted to the actions a and f. The expected behavior of this protocol is expressed by the CCS speci cation spec :=: a;f;spec. and we see that protocol has the same observational behavior as spec, by 28 7. Examples ?- wbisim(spec,protocol). Searching for a weak bisimulation... Here is a listing of a weak bisimulation of the processes spec and protocol 0 spec protocol LHS--> a ==> 1 RHS--> a ==> 1 1 f;spec (sender1/medium/receiver)\[a,f] LHS--> f ==> 2 RHS--> tau ==> 4 2 spec (in(d);sender+in(c);sender1/medium/out(d);receiver) \[a,f] LHS--> a ==> 1 RHS--> tau ==> 3 3 spec (sender/medium/receiver)\[a,f] LHS--> a ==> 1 RHS--> a ==> 1 4 f;spec (in(d);sender+in(c);sender1/ out(c);medium+out(e);medium/receiver)\[a,f] LHS--> f ==> 2 RHS--> tau ==> 5 RHS--> tau ==> 1 5 f;spec (in(d);sender+in(c);sender1/medium/ f;out(d);receiver)\[a,f] LHS--> f ==> 2 RHS--> f ==> 2 However, this does by no means imply that a given input alway will pass through 7.1 A Simple Protocol 29 the protocol, since weak bisimularity does not preserve divergence . Consider the following. A most natural request to such a protocol is that it invariantly holds, that no matter how the protocol receives an input on a it is guaranteed to be delivered on f. Moreover, it should always be true, that whenever an output on f has been delivered, the protocol will eventually be ready for a new input on a. In modal terms these two properties may be expressed as INV([a]even(<f>tt)) and INV([f]even(<a>tt)). Unfortunately, protocol just enjoy one of these two properties, namely the second. This can be seen from the following applications of the Modal Checker. ?- [] >- protocol : "INV([a](even(<f>tt)))". no ?- [] >- protocol : "INV([f](even(<a>tt)))". yes But why does protocol not have the property INV([a](even(<f>tt)))? The answer to that can be found by asking why the process enjoys the dual property poss(<a>(inv([f]ff))). ?- [] >- protocol : "poss(<a>(inv([f]ff)))". >- 6 : poss <a>(inv [f]ff) as >- 6 : <a>(inv [f]ff) as >- 5 : inv [f]ff as ^ >- 5 : [f]ff is immediate and ^ >- 4 : inv [f]ff as ^ >- 4 : [f]ff is immediate and ^ >- 5 : inv [f]ff is immediate by ^ Out of this proof it can be read that from some state, namely 5, there exist a computation on which f {actions are never allowed. By using moves we get that the only derivation from 5 is a tau transition to 4, from where the only derivation is a tau transition back to 5. Thus we may conclude that the reason why protocol does not posses the property INV([a](even(<f>tt))) is because it is capable of diverging. This is re ected more directly by the following 30 7. Examples ?- diverge(protocol). protocol -a-> (sender1/medium/receiver)\[a,f] -tau-> (in(d);sender+in(c);sender1/out(c);medium+out(e);medium/ receiver)\[a,f] -tau-> (sender1/medium/receiver)\[a,f] Thus, even though the observational behavior of protocol equals that of spec, we cannot be sure that an input ever comes through (without making certain fairness assumptions), in that the protocol may possibly diverge. 7.2 7.2 The Dining Philosophers 31 The Dining Philosophers This is a simpli ed version of the Dining Philosophers example from [Hoa78], where forks are assumed to be placed in the center of the table and thus available for any philosopher. We assume that some philosophers meet in an academy eating spaghetti and disgussing the latest results in their topic of research. To eat spaghetti each philosopher needs two forks. He can take any fork not used by another philosopher and after eating he must release both forks immidiately. In this example we shall consider only two philosophers. The parallel system, called academy, consists of four components, namely two philosophers phil1 and phil2 and two forks. Each component is de ned as: ?- fork :=: in(take);in(drop);fork. ?- phil1 :=: think1;phil1 + out(take);out(take);phil11. ?- phil11 :=: eat1;phil11 + out(drop);out(drop);phil1. ?- phil2 :=: think2;phil2 + out(take);out(take);phil22. ?- phil22 :=: eat2;phil22 + out(drop);out(drop);phil2. ?- academy :=: (phil1/phil2/fork/fork)\[eat1,eat2,think1,think2]. Thus a philosopher, say phil1, can think and thereby become a philosopher again or he can in turn take two forks and become phil11. From this state the philosopher will eat until full after which he drops the two forks returning to the initial state phil1. A fork is supposed to be rst taken and then droped again. Finally, the system academy is de ned as the parallel composition of two forks and the two philosophers where only eat and think actions are observable to the environment: Of course, the intended observational behaviour of academy is, that one of the philosophers may always either think or eat. Thus a speci cation could perfectly well be: ?- spec :=: eat1;spec + eat2;spec + think1;spec + think2;spec. So, let us now see whether the academy is weakly bisimular to spec. 32 7. Examples ?- wbisim(academy,spec). Constructing derivation table for academy ...extending it to an obdertable. Constructing derivation table for spec ...extending it to an obdertable. Searching for a weak bisimulation... The process: academy enjoys some properties which the process spec doesn't. One property is: <<tau>>[[eat1]]ff From this, we conclude that academy does not satisfy spec, since there exists a situation where phil1 cannot eat. To see why, we apply the model checker of Tav under the why{mode. ?- why. ?- [] >- academy : "<<tau>>[[eat1]]ff". Using existing obdertable for academy >- 15 : <<tau>>[[eat1]]ff as >- 9 : [[eat1]]ff is immediate ?- procinfo(15). academy :=: (phil1/phil2/fork/fork)\[eat1,eat2,think1,think2] ?- procinfo(9). (out(take);phil11/out(take);phil22/in(drop);fork/ in(drop);fork)\[eat1,eat2,think1,think2] 7.2 The Dining Philosophers 33 Thus , process number 15, has the property <<tau>>[[eat1]]ff since can reach process number 9 by performing an number of tau actions and moreover since that process cannot do an eat1 action. Actually process number 9 is deadlocked. academy academy ?- numbmode. ?- deadlock(15). 15 -tau-> 14 -tau-> 13 -tau-> 12 -tau-> 11 -tau-> 10 -tau-> 9 What has happend is that phil1 and phil2 has one fork each and since each both are waiting to lay hand on another the system is deadlocked. In order to get rid of this deadlock property we de ne a new academy, new-academy, by introducing a chair | actually this is just a binary semaphore | which a philosopher must posses before eating. 34 7. Examples ?- chair :=: in(sit);in(stand);chair. ?- new_phil1 :=: think1;new_phil1 + out(sit);out(take);out(take);new_phil11. ?- new_phil11 :=: eat1;new_phil11 + out(drop);out(drop);out(stand);new_phil1. ?- new_phil2 :=: think2;new_phil2 + out(sit);out(take);out(take);new_phil22. ?- new_phil22 :=: eat2;new_phil22 + out(drop);out(drop);out(stand);new_phil2. ?- new_academy :=: (new_phil1/new_phil2/fork/ fork/chair)\[eat1,eat2,think1,think2]. Thus now a philosopher must sit on the chair, in(sit), before taking the forks and after eating he must stand up, in(stand), when the forks are dropped. It now turns out that new-academy satis es spec since: 7.2 35 The Dining Philosophers ?- wbisim(new_academy,spec). Constructing derivation table for new_academy ...extending it to an obdertable. Using existing obdertable for spec Searching for a weak bisimulation... Here is a listing of a weak bisimulation of the processes new_academy and spec 0 new_academy spec LHS--> LHS--> LHS--> LHS--> RHS--> RHS--> RHS--> RHS--> think2 ==> think1 ==> tau ==> 7 tau ==> 1 think2 ==> think1 ==> eat2 ==> 3 eat1 ==> 9 ......... The complete weak bisimulation contains 15 states. 6 6 6 6 36 7. Examples 7.3 Hymans Mutual Exclusion Algorithm Hyman's algorithm [Hym66] was supposed to guarentee mutual exclusive execution of the critical section of concurrent processes. However, it turned out that the algorithm does not preserve mutual exclusion at all. We would like to analyse the algorithm using the tools of Tav. The following formulation of Hyman's algorithm is taken from [Wal88]. There are two processes, two variables, 1 and 2 , of type boolean with initial value false and a variable ranging over f1 2g with arbitrary initial value. The th process may be described as in the gure below, where is the index of the other process. b k b ; i j while true do begin h non critical section while k 6= i i; do begin while k := bj do skip; i end; h bi critical section i; := false end. The CCS representation of Hyman's algorithm, hyman2, also is taken from [Wal88]. Here the initial value of is 1. k 7.3 Hymans Mutual Exclusion Algorithm ?- bool1f :=: out(b1rf);bool1f + + in(b1wt);bool1t. ?- bool1t :=: out(b1rt);bool1t + + in(b1wt);bool1t. ?- bool2f :=: out(b2rf);bool2f + + in(b2wt);bool2t. ?- bool2t :=: out(b2rt);bool2t + + in(b2wt);bool2t. 37 in(b1wf);bool1f in(b1wf);bool1f in(b2wf);bool2f in(b2wf);bool2f ?- k1 :=: out(kr1);k1 + in(kw1);k1 + in(kw2);k2. ?- k2 :=: out(kr2);k2 + in(kw1);k1 + in(kw2);k2. ????- p1 :=: out(b1wt);p11. p11 :=: in(kr1);p13 + in(kr2);p12. p12 :=: in(b2rt);p12 + in(b2rf);out(kw1);p13. p13 :=: enter;exit;out(b1wf);p1. ????- p2 :=: out(b2wt);p21. p21 :=: in(kr2);p23 + in(kr1);p22. p22 :=: in(b1rt);p22 + in(b1rf);out(kw2);p23. p23 :=: enter;exit;out(b2wf);p2. ?- hyman2 :=: (p1/p2/k1/bool1f/bool2f)\[enter,exit]. The rst four declarations represents the boolean variables b1 and b2, k1 and k2 represents the variable k and p1 and p2 represents the two processes. Finally hyman2 is the paralles compostion of the boolean variables instantiated to false, the variable k instantiated to 1 and the two processes p1 and p2. Suppose that Hyman's algorithm is a genuine algorithm for mutual exclusion. Then necessarily it must be weakly bisimular to the following speci cation. spec :=: enter;exit;spec. saying that enter and exit actions must alternate, hence ensuring, that the two processes are never simultaneously in their critical regions. To examine whether hyman2 satis es spec we search for a weak bisimulation. 38 7. Examples ?- wbisim(hyman2,spec). Constructing derivation table for hyman2 ...extending it to an obdertable. Constructing derivation table for spec ...extending it to an obdertable. Searching for a weak bisimulation... The process: hyman2 enjoys some properties which the process spec doesn't. One property is: <<enter>><<exit>><<enter>><<exit>><<enter>><<enter>>tt From this, we conclude that hyman2 actually allows both processes to enter their critical regions (in disagreement with the mutual exclusion property) In would be interesting to test whether hyman2 satis es the even simpler property <<enter>><<enter>>tt saying that the two processes can both be in their critical section rst time they enter it. ?- why. ?- [] >- hyman2 : "<<enter>><<enter>>tt". Using existing obdertable for hyman2 >- 71 : <<enter>><<enter>>tt as >- 17 : <<enter>>tt as >- 9 : tt is immediate ?- procinfo(71). hyman2 :=: (p1/p2/k1/bool1f/bool2f)\[enter,exit] Moreover, we would like to nd a path for a computation where this property 7.3 Hymans Mutual Exclusion Algorithm 39 is satis ed. Thus, we alternatively could test why hyman2 enjoys the property <<tau>><enter><<tau>><enter>tt and then use the predicate taupath. ?- [] >- hyman2 : "<<tau>><enter><<tau>><enter>tt". Using existing obdertable for hyman2 >- 71 : <<tau>><enter><<tau>><enter>tt as >- 18 : <enter><<tau>><enter>tt as >- 17 : <<tau>><enter>tt as >- 10 : <enter>tt as >- 9 : tt is immediate ?- procinfo(18). (p13/out(kw2);p23/k1/bool1t/bool2t)\[enter,exit] ?- taupath(hyman2, (p13/out(kw2);p23/k1/bool1t/bool2t)\[enter,exit]). hyman2 -tau-> (p1/p21/k1/bool1f/bool2t)\[enter,exit] -tau-> (p1/p22/k1/bool1f/bool2t)\[enter,exit] -tau-> (p1/out(kw2);p23/k1/bool1f/bool2t)\[enter,exit] -tau-> (p11/out(kw2);p23/k1/bool1t/bool2t)\[enter,exit] -tau-> (p13/out(kw2);p23/k1/bool1t/bool2t)\[enter,exit] 40 7. Examples ?- procinfo(17). (exit;out(b1wf);p1/out(kw2);p23/k1/bool1t/bool2t)\[enter,exit] ?- procinfo(10). (exit;out(b1wf);p1/p23/k2/bool1t/bool2t)\[enter,exit] ?- numbmode. ?- taupath(17,10). 17 -tau-> 10 From this it follows that hyman2 after ve tau-actions reaches a state (process number 18) where p1 enters its critical section. The system is now in a state (process number 17) where it can do a single tau-action to process number 10. From that state it is possible for p2 to enter its critical section. References 41 References [BAPM83] M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Informatica, 20, 1983. [CM81] W.F. Clocksin and C.S. Mellish. Programming in PROLOG. Springer{ Verlag, 1981. [CPS88] R. Cleaveland, J. Parrow, and B. Ste en. The concurrency workbench. University of Edinburgh, Scotland, 1988. [Hil87] M. Hillerstrom. Veri cation of CCS{processes. PhD thesis, Aalborg University Center, Denmark, 1987. R 87{27. [HM85] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, pages 137{161, 1985. [Hoa78] C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8), 1978. [Hym66] H. Hyman. Comments on a problem in concurrent programming control. Communications of the ACM, 9(1), 1966. [KS] Kannellakis and Smolka. CCS expressions, nite state processes, and three problems of equivalence. To appear in Information and Computation. [Lar] K.G. Larsen. Arguing about membership of maximal xedpoints. furture paper. [Lar86] K.G. Larsen. Context{Dependent Bisimulation Between Processes. PhD thesis, University of Edinburgh, May eld Road, Edinburgh, Scotland, 1986. [Lar87] K.G. Larsen. A context dependent bisimulation between processes. Theoretical Computer Science, 1987. [Lar88] K.G. Larsen. Proof systems for Hennessy{Milner logic with recursion. Lecture Notes in Computer Science, 299, 1988. in Proc. of CAAP'88. [LMV88] V. Lecompte, E. Madelaine, and D. Vergamini. Auto: A ver cation system for parallel and communicating processes. INRIA, Sophia{Antipolis, 1988. 42 [LS87] [Mil80] [Mil83] [Par81] [Par85] [PT87] [Tar55] [Wal88] References K.G. Larsen and A. Skou. Tau: Theories for parallel systems, their automation and usage. Aalborg University, Denmark, March 1987. R. Milner. Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1980. R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25, 1983. D. Park. Concurrency and automata on in nite sequences. Lecture Notes in Computer Science, 104, 1981. in Proc. of 5th GI Conf. J. Parrow. Fairness Properties in Process Algebra. PhD thesis, Uppsala University, Sweden, 1985. Paige and Tarjan. Three partition re nement algorithms. SIAM Journal of Computing, 16(6), 1987. A. Tarski. A lattice{theoretical xpoint theorem and its applications. Paci c Journal of Math., 5, 1955. D. Walker. Analysing mutual exclusion algorithms using CCS. ECS{ LFCS 88{45, University of Edinburgh, 1988.