. . . 1:0. K. _ . .51: I i: it I' :3! X , $4! {$52 '1 6 ‘I .; 3. W ‘§ 4 rA :: SI - . . ' Win? m g faith». “.3. ‘ O lion...- ‘ ..‘ .. .. . . . . ‘ . v I .uuf 0 D-pvlas.l .‘0 . lvy Ovll\.o..‘o0‘1'r . lvn. ‘. v. 0 '31}. .. vol? Iv - ‘ ~ .2 .u‘.. ,‘A 33.. . . I u #5... .-L.1;vt.v,.u mdf§fi£fid§rf ... I." ill” ‘3 W“ l lllllll l H ll ll Mill Hill 3 1293 00881 2723 ll This is to certify that the thesis entitled TEMPORAL SPECIFICATIONS FOR DISTRIBUTED SYSTEMS presented by William Eugene McUmber has been accepted towards fulfillment of the requirements for M.S. Computer Science degree in 0-7639 MS U is an Affirmative Action/Equal Opportunity Institution LIBRARY Michigan State University PLACE IN RETURN BOX to remove this checkout from your record. 0 AVOID FINES return on or before date due. L_.._———————————-—/‘l l DATE DUE DATE DUE DATE DUE _ ’_— ii _ !_ —— ——_— __— #— f ’f !__ ‘ ___ —' i Si 3 L471} 7— 4—— !__—f 4‘ ! —_——— MSU Is An Affirmative Action/Equal Opportunity Institution czwmuuoanpnwn ___.——- Temporal Specification Systems for Distributed Systems By William E. Mc Umber A Thesis Submitted to Michigan State University in partial fulfillment of the requirements for the degree of Master of Science Department of Computer Science May, 1993 Betty H. C. Cheng, Advisor ABSTRACT Temporal Specification Systems for Distributed Systems By William E. Mc Umber This work explores specification techniques that have the capability of handling state- ments about occurrences in time. The work is oriented towards problems found in con- junction with distributed systems. Distributed system problems are characterized by many processes executing concurrently, often with important interoperating timing constraints, and often without the benefit of synchronization from a global clock. The usual approach, state based temporal systems, assume some form of clocking of the system and requires either a synchronous or interleaving state transition model. After giving a survey of current specification methods, this thesis presents two alternative specification systems based on modal-temporal logic. The first approach is based on an extension to the Larch specification language. The model proposed is based on points in time and avoids the use of clocks. The second approach uses two sets of modal operators, one for time and another for possibil- ity, as a means of specifying event sequences without state transitions in either linear or branching time. In this approach, use of the modal possibility operator replaces existential quantification found in state-based branching time formulations of temporal logic. The second approach disallows instants in time and is based on intervals. To my wife, Cheryl and our sons Weston and Robert. ACKNOWLEDGMENTS I am indebted to many people without whom I could not have completed this work. First and foremost, I am indebted to my advisor, Betty H. C. Cheng, whose direction has led me to this point. It is Dr. Cheng that convinced me of the importance of predicate logic for program specifications, and it was her suggestion to carefully study Larch that influenced much of my thinking about the nature of a specification language. In addition, her guidance and patience through many edits and her pointed questions were invaluable. I also wish to thank Phillip McKinley who introduced me to the formal aspects of distributed systems. From him I first understood the complexity inherent in problems dealing with mutual exclusion, liveness and distributed systems in general. I wish to thank the members of my committee, John Geske, Phillip McKinley, and Betty H. C. Cheng who provided many helpful comments. I wish to extend my thanks to George Stockman and Lora Mae Higbee who lead the way through a maze of procedures and requirements that ultimately permitted the completion of this Thesis. Finally, the personal and emotional support provided by my loving wife, Cheryl, and our sons, Wes and Robbie can not be measured. The many hours spent on this work was, in many ways, their time, and I am indebted to them for it. iv TABLE OF CONTENTS LIST OF FIGURES 1 Introduction 2 Modal Logic 2.1 Temporal Logic Systems ............................. 3 Survey of Temporal Specification Systems 3.1 Process Algebras -— CSP and CCS ....................... 3.2 LOTOS ...................................... 3.3 Temporal Characteristics of Process Algebras ................. 3.4 Data Network Specifications ........................... 3.5 Temporal Characteristics of Stream Networks ................. 3.6 Temporal Extensions to a Non-Procedural Language ............. 3.7 Specifying Temporal Properties Without Temporal Logic .......... 3.8 Comparison of Systems ............................. 4 The Extension of Larch for Temporal Specifications 4.1 Introduction .................................... 4.2 Properties of Time ................................ 4.2.1 Discrete versus Continuous ....................... 4.2.2 Points and Intervals ........................... 4.2.3 Events, Intervals and Properties .................... 4.3 Extension of Existing Language with Temporal Notation ........... 4.3.1 Larch Specifications ........................... 4.3.2 Temporal Notation for Larch ...................... 4.4 Dining Philosopher Example .......................... 5 Dual Modalities for Temporal Specifications 5.1 Introduction .................................... 5.2 Interval Model of Time .............................. 5.3 Temporal Logic Systems ............................. 5.4 Examples of Common Specifications ...................... vii 1 4 6 13 14 25 29 31 35 36 47 50 52 52 53 53 54 56 58 58 60 66 71 71 72 77 83 5.4.1 Property Becoming True ......................... 5.4.2 Fairness Conditions ........................... 5.4.3 Latching Conditions ........................... 5.4.4 The Leads-to Operator .......................... 5.4.5 Mutual Exclusion ............................. 5.5 Related Work ................................... 5.6 Conclusion 5.7 Future Work OOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOOO 6 Conclusions and Future Work BIBLIOGRAPHY A vi 84 84 84 86 86 88 89 91 94 98 3.1 3.2 3.3 3.4 3.5 3.6 3.7 3.8 3.9 3.10 3.11 3.12 3.13 3.14 3.15 4.1 4.2 4.3 4.4 4.5 4.6 4.7 4.8 5.1 5.2 5.3 LIST OF FIGURES CCS Description of Jobber’s Behavior ..................... Transisition Diagram for Jobber and Hammer ................. Language equivalent state machines with differing behavior ......... Algebraic description of type not ........................ An operator agent F ............................... Lucid network for calculating arithmetic means ................ Table of temporal Lucid operators ....................... Language form of the mean program ...................... Stream schedule agent .............................. Ina Jo Specification Template .......................... Ina Jo non-temporal example .......................... Ina Jo Syntax for Assertions ........................... Temporally based version of specification LIVE ................ Buchi automaton ................................. Buchi automaton specifying mutual exclusion ................. Example trait for a push down stack ...................... Event behavior from a container point of view ................. Axioms for behavior of instants ......................... Temporal (modal) constructs introduced into Larch .............. Trait specifying axioms for intervals ...................... Trait Specifying Axioms for hold Predicate ................... Simple trait for Dining Philosophers ...................... Refinement of Dining Philosophers to specify transitions ........... Possible structural relations for time intervals ................. Branching time. Letters represent possible states of the system at times 1 through 4. The sequence ABFQ is one possible execution path but so is ADLX. ...................................... Two dimensions for modal operators. The X axis represents the regular progression of time. The Y axis represents alternate execution sequences, each with temporal properties. ......................... vii 18 18 24 29 31 32 32 33 34 37 38 40 46 48 49 59 60 62 63 65 65 67 69 75 78 5.4 Proof that GDP and [II-1P cannot both be true. If GDP and CJ-uP are both true, then their conjunct must also be true. The proof shows this assumption leads to a contradiction. ............................. viii CHAPTER 1 Introduction Formal methods focus a software development effort on an accurate and precise specification of what a software system or component is to achieve. This type of specification is usually referred to as a formal specification and is expressed in a precise mathematical notation de- fined by a formal specification language. Specifications can be written in natural languages, semi-formal notations (analogous to pseudo-code for programs), and in formal languages. We define a formal language as one in which the syntax and semantics are pre-defined in an unambiguous way. Syntax is usually defined through a gramli Semantics are harder to define precisely but, at a minimum, the intention of language constructions can be described through logical formulas accompanied by a small amount of clarifying text. An example can be found in [1] where Larch, both described and used later, is formally defined. The intention of formality in a language is to provide the interpretation of any statement in the language by a set of defined rules. The advantage of a formal language as defined is that its assertions are unambiguous and have the potential of being manipulated by programs [2, 3, 4]. Many formal languages are already in use for software specification. A frequent basis for these languages is formal logic [2, 5, 6]. Software for distributed systems have the same problems of correct and accurate 1Grammars can be “ambiguous” in the sense that the same language construct may possibly be derived from two or more different sets of production rules. Since determination of ambiguity in grammars more complex than regular grammars (i.e.,context free and context sensitive grammars) is undecidable, we can never be sure, in the general case, that the formal language grammar, and hence the formal language, has unambiguous syntax. The intended meaning of “unambiguous” is that the rules for the formal language are defined as best as possible before use and that the semantics are unambiguous. behavior as do other forms of software, but it also has the added burden of inter-process timing relations. By their nature, distributed systems consist of many processes running in a computationally diverse environment. Often, the processes must interact in complex ways without interfering with each other. Two broad classes of inter-process problems, called liveness and mutual exclusion, have been widely studied [7, 8, 9, 10]. Both problems contain at their core the sub-problem of inter-process timing constraints. Temporal specification systems have been widely studied but often only in connection with real-time systems [11, 12, 13]. Unlike real-time systems where a global clock either exists or can be assumed, distributed systems normally have no global clock. Provision of a global clock is equivalent to solving distributed consensus problems which is known to be difficult and, in some situations, impossible [14, 15, 16]. Most real-time specification systems use state progressions as the means of marking the passage of time. Either an interleaved or sequential model of state transition is usually assumed. Since a distributed environment has no global clock and processors run at various speeds, neither model of state transition matches reality very well. The goal of this work is to investigate and formulate a formal specification methodology that has sufficient expressive power to specify time-based system behaviors. The specifica- tion system must be expressive enough so that it does not rely on state transitions alone to describe time. The specification language should be based on logic and algebraic in nature. The reason for basing the language and method on logic is that both modal logic and first order logic have been extensively studied and are well understood. We specifically address formal languages that are algebraically based for two reasons: 1. We consider algebraic languages to be better suited to automated tools and existing automatic rewrite systems than other approaches. 2. Algebraic languages are declarative in nature, and as such, are more likely to be implementation-detail independent. The intention is to specify the required behavior rather than how the behavior is obtained. It is likely that verification of actual software specifications, especially those involving timing constraints such as liveness, deadlock, and mutual exclusion, can only be practically addressed by automated systems. If this is true, the specification system will have to be embodied in automated tools in order to have significant impact. Finally, the specification system should be as intuitive as the constraints of the prob- lem allow. Initial problem descriptions always originate with humans. The success of the methodology will be determined by the degree to which the specifier is relieved of details while retaining enough precision to describe exactly what should happen. We meet these goals through several new developments. First, we introduce a temporal model into an existing algebraic specification language. The temporal model includes de- velopment of an HOLD predicate for describing invariant properties. We first encountered the idea of HOLD in Allen’s [17, 18, 19] work but we have extended the use and definition beyond the original concept. Second, we introduce a new method of specifying alternate future sequences by em- ploying dual modalities. Temporal specification systems frequently have difficulty with alternate future execution sequences, generally known as the branching time problem. The most common solution is to use quantification over modal operators to describe multiple future sequences, as in [20]. This approach has its difficulties, however [21, 22]. Our ap— proach avoids quantification over execution sequences, and consequently, the difficulties quantification introduces. The remainder of the thesis is organized as follows. Chapter 2 introduces modal and temporal logic, both of which are used throughout this work. Chapter 3 surveys a vari- ety of specification methods capable of describing timing constraints. Chapter 4 presents our extensions to an algebraic language with temporal logic. Chapter 5 introduces a new approach to temporal specification based on intervals. This approach uses the standard modal-temporal operators for time but introduces the use of another modal operator as a replacement for quantification for branching time descriptions. Finally, Chapter 6 contains concluding remarks and discusses future work. CHAPTER 2 Modal Logic Many commonly used temporal logic systems are based on modal logic. Complete descrip- tions of modal logic can be found in [23, 24, 25], but a brief introduction of fundamental concepts is provided in this section in order to provide a basis for temporal logic discussions later. Modal logic augments standard quantified first-order predicate logic by introducing op- erators for describing what is possible and necessary in addition to what is or is not. Just as quantifiers specify “all” or “some” in a formula, modal operators permit specification of ne- cessity and possibility. In English, there is a clear distinction between “Today is Saturday” and “It is possible that today is Saturday.” The former’s truth or falsity is determined by the value of “today”. The latter’s truth is determined by the values of “todays” throughout multiple contexts where the statement “Today is Saturday” can be made. Contrast the two statements when the value of “today” is not Saturday. In elementary logic, the statement “today is Saturday” is clearly false on Tuesday, while “it is possible that today is Saturday” is true. In logic terms, for a given predicate P, [possible] P can be true when P, in a particular setting, is false. The intuitive idea introduced above is one of a collection of possible worlds, including our present one. In each world, each logic sentence can be evaluated to true or false. Thus, a world is an instantiation of a set of variables and value assignments particular to this world. A sentence is said to be necessary if it is true in all worlds. A sentence is said to be possible if it is true in at least one world. The difference between the earlier statements “It is possible that today is Saturday” and the first order statement “It is not the case that for all days, no day is Saturday” lies in the object of quantification. In the former, modal logic requires quantification over all worlds, or possible settings of the statement “today is Saturday.” In the latter statement, quantification ranges over all days, but only within one setting, that is, one world. Given a sentence A, the notation DA is used to indicate A’s necessity. The notation 0A is used to indicate A’s possibility. Given an infinite collection of worlds, W, P abbreviates an infinite sequence P0, P1, P2, . . . of subsets of W. The pair A = (W, P) represents a model. Given a sentence A, and a world pfl E P in the model, the interpretation of i=3” A (2.1) is A is true at world pn in A. Several tautologies for world models can be written as follows: 1. [=3fl True. 2. -~ #3” False. 3. i=9” L'JA => for every p,- E A, i=3,- A 4. i=3" 0A = for some p,- 6 A, #9,. A Statement (1) means that the logic constant True is always true in all worlds. Likewise, Statement (2) means False is never true. Statement (3) defines necessary as requiring A to be true in all worlds in the subset P of worlds in the model. Statement (4) similarly defines possible as requiring A to be true in some world. Given the notation I: A means A is true in all models in all worlds, if A is a tautology, then I: A and CIA are true for all worlds. If we take D as a primitive then we can define O as 0A = fill-1A (2.2) denoting what is possibly true cannot always be not true. The relationship is symmetrical, that is, DA 2 '10'1A (2.3) indicating what is necessarily true cannot be not possible. 2.1 Temporal Logic Systems The majority of temporal logic operators are based on systems derived from modal logic. As many as 15 different modal systems [25] can be constructed depending on the axioms and inference rules chosen for the system. When choosing a modal system, and especially when giving the modal system a temporal semantic interpretation, the path is strewn with many traps that can lead to inconsistent systems or systems that allow statements that make no sense in the real world. All modal systems assume the fundamentals of logic including standard definitions for disjunction (V), conjunction (A), Modus Ponens, De Morgan’s laws, etc. To these are added definitions and axioms that describe the characteristics of necessity and possibility as de- scribed in the previous section. We follow convention and use the notation DP for “P is necessary” and OP for “P is possible.” Following the naming convention of Cresswell and Hughes [24], the simplest of the modal systems is called T. T consists of definitions TDEFl and two axioms, TAl and TA2: TDEFI Elp E -u<>-1p TAl Dp==>p TM [30!} => a) = (Up => Dq) where p and q are any well-formed formulas. Definition TDEFl is basic to all modal and temporal systems and states “what is possible (henceforth, always) true is not possibly (eventually, sometimes) not true.” Axiom TA2 permits CI to commute with implication. System S4 [24] is obtained by adding only one additional axiom to T: 84A]. Up => UUp S4A1 enables the reduction of compounded modal operators but also produces a profound difference between System T and S4. The combined use of TDEFl and S4A1 allow any sequence of compounded modal operators to be reduced to one of the following: 1. -none— (no operator) Cl 0 [:10 OD DOC! 7'99"???" 000 When combined with the negated forms, only 13 different compounded modal operators (including no modal operator) are possible in S4. Contrast this with an infinite number of compounded modal operators in T, which has no reduction rule. System S5 [24] is obtained from T by adding: 85A]. Op => E101) Rule S5A1 is similar to S4A1, enabling reduction of compounded modal operators. In contrast to S4Al, S5A1 allows reduction of any sequence of modal operators to no more than one operator. Compounded operators can be reduced in 85 to either no operator, 0, or Cl. Although powerful reductions are possible in system S5, we will see below that such reduction power introduces semantic difficulties when S5 is used in a temporal context. S4 and S5 are simple variants of the T system, but each has distinct semantics. For example, consider the temporal implications of Axiom SSAl. While a tool to reduce any long sequence of modal operators may be convenient, the tool also permits the following reduction: 00p : Up (2.4) If the symbols D and O are assigned the meaning henceforth and eventually, respectively, then Theorem (2.4) takes the meaning “if p is eventually henceforth true then it is true now and from now on.” This theorem, while a logic consistency in S5, makes no sense in the real world. In fact, as will be seen in Section 5.4.3, specification of a latch is not possible in S5. The problem with Theorem (2.4) perhaps lies not with the logic of S5 but with the assign- ment of meaning to operators for necessity (CI) and possibility (0). An important semantic choice is whether the necessity operator will represent all time or all future time. When necessity is associated with “always,” possibility is analogously associated with “some- times.” This system is referred to as non-ordered time and is best axiomatized by SS. Re-interpreting Theorem (2.4) under non-ordered time semantics, the meaning becomes “what is sometimes always true is always true,” which does make sense. If making strong statements about ordering in time is a requirement of the temporal specification system, then choosing a non-ordered time logic system would be inappropriate. Ordered time re- quires interpretation of necessity, (D), and possibility, (O), as henceforth and eventually, respectively. The modal system applicable for order-time semantics is S4. The necessity operator is assigned the meaning henceforth and the possibihty operator becomes eventually. The S4 system does not include Theorem (2.4) and thus the interpretation “eventually, henceforth p implies henceforth p” is not a problem. The frequently referenced temporal systems of Manna and Pnueli are generally based on S4 with the passage of time indicated by state transitions} Specification systems often include predicates and quantification to increase expressive capability. There are several ways to add predicates and quantification to a logic system [23, 24, 25]. In combination with the 15 or so possible modal systems, various ways of quan- tification can produce 50 or 60 different quantified modal systems. As with the fundamental modal systems, the choice of axioms has a major bearing on expressive power and meaning, and consequent theorems of the logic. Great care must be taken to prevent theorems whose semantics are inappropriate, as in the example of Theorem (2.4). 1Ostroff [13] concisely consolidates much of the work of Manna and Pnueli. Consider a temporal system based on S4 to which we wish to add quantification. Quan- tification is often added to temporal systems to enable statements about alternate futures. This problem is discussed later in detail in Section 5.3. As a preview, Ina Jo, also discussed later in Section 3.6, contains S4 with standard quantification as found in normal predicate logic. In the expressions that follow, we denote individual, single value variables by simple letters such as p, q, z, y. We denote complex expressions involving operators and predicates by Greek letters such as a,fl. First, we add to S4 the definition of a stronger implication operator2=o>z SIMP CI(p==>q) Ep=g-> q In addition to standard inference rules such as Modus Ponens, add the rule: N1 l- (a=> ,6) -——->i- (Da = Dfl) Rule N1 permits us to infer that whenever theorem a implies theorem fl, henceforth 0 implies henceforth B. To the axioms for S4, we add the following axioms for quantification: Q1 vo(o = fl) ==> (Va:(a) = Vx(fl)) Q2 Va:(a a [3) => (Va:(a) a Vz(fl)) 03 Vz(a) '=' a(3x-(a)) The scope of the quantifiers is indicated by the parenthesized expression immediately fol- lowing the quantifier. As expected, V:r(a) means :1: takes any value wherever it occurs within the expression a. Variable :c is normally called a bound variable in such an expression. S4 without quantification is sufficient for simple interpretations of time, but when several alternate future state sequences are allowed, quantification is required to distinguish between characteristics of sequences. The additional problems quantification introduce can be seen from the following exam- ple. Axiom Q1 means that, if for all 2:, expression a implies expression fl is true, then for 2Many modal logic texts such as [24] include =3 as part of the definition of system T. The intent of strong implication is to describe causahty between two statements. 10 all 1: over a implies for all 2 over 5 is also true. The importance of Q1 hes in the ability of universal quantification to distribute over implication. Replacing “implies” (=) with causally implies (=D>) makes the statement “if for all z, or causes fl, then for all a: over or causes ,6 to also be true for all 2:.” Since Q1 is valid, it seems intuitive that its analog, expressed symbolically, Va:(a =°> 3) => (Va:(a) .—E> was» (2.5) would also be true. Yet, Formula (2.5) is not a theorem of our new system‘.3 Expanding Formula (2.5) by SIMP produces: Va:(CJ(a = fl)) => Cl(‘v’:r:(a) => Vz(fl)) (2.6) Expression (2.6) appears correct, but notice that operators D and V switch scopes from the left to the right side of the central implication. The axiom set currently contains no tools permitting Formula (2.5) to be proven true. A similar expression that can be proved is: C1(V:c(a = fl)) => D(Va:(a) => Vz(fl)) (2.7) Formula (2.7) follows directly from Q1 and N1. The difference between Formulas (2.6) and (2.7) lies in the order of operators CI and V on the left side of the central implication. If we had the following axiom in our system: V2:(Cl(a => (3)) = C1(V:r(a => 5)) (2.8) then we could prove Expression (2.6) from Expression (2.7) and (2.8). Expression (2.8) is a special form of : (Va:(C1a)) => (D(V:c(a)) (2.9) which can be rewritten using negation and the definitions of V and CI to: BF <>(3z(a)) => 3z(<>a)) aFormula (2.5) can be shown to be a theorem of SS, but as we have already seen, S5 based systems are not appropriate for the kind of specifications we wish to write. 11 Formula BF is commonly known as the Barcan formula [24], and its converse is the Inverse Barcan formula. The Barcan formula has important semantic implications if included in S4 based tem- poral systems. Permitting temporal and quantification operators to commute can facilitate proving theorems, but the semantics associated with Barcan can constrain the behavior of the system with respect to its objects. Consider the meaning of Barcan: 03z(P(:c)) = 3z(<>P(:r)) (2.10) Expression (2.10) means if eventually there will exist an object a: with property P(z) then there (already) exists an object a: for which P(:c) will eventually become true. Since the right side of Formula (2.10) implies that 2: already exists, the formula constrains the universe of objects to not grow. This follows from the ability Barcan gives us to replace “eventually there exists 2:” with “there exists 2:.” Likewise, inverse Barcan implies the eventual existence of an object a: satisfying P(:c), based on the existence of a: now. Therefore, inverse Barcan implies the universe of objects cannot shrink. Barcan written as: 033(0) 4:) 323(00) (2.11) implies a statically sized universe of objects. What is the practical implication of Barcan? Suppose we wish to specify behaviors of a system allowing users to log on and off. A timesharing system or a distributed database are examples. Inclusion of Barcan requires all users to always be a part of the specified system and to exist in a “logged-on” state or a “logged-off” state instead of randomly appearing and disappearing from beyond the boundaries of the system. The flexibility of permitting commutation of quantification and temporal operators must be weighed against potential constraints imposed by a statically sized universe. Statically sizing the universe may re- quire extra predicates to express the membership or non-membership of an object within a system. Even with membership predicates, all potential objects require identification and specification. 12 The example of Barcan in the previous paragraphs illustrates the sensitivity of semantics to the choices for axioms in the temporal system. Unlike standard predicate logic, quantifi- cation cannot be added in an ad hoc fashion to modal systems without potentially serious side efiects. As seen by the example above, adding axioms to a system to facilitate proof of a theorem that seems intuitive can result in unintended meanings, such as the statically sized universe. CHAPTER 3 Survey of Temporal Specification Systems This section reviews several well-known specification systems for specifying program prop- erties that require special attention to temporal details. The systems surveyed are chosen to represent a broad range of specification techniques. Not all of the surveyed systems use modal-based temporal logic, but all systems attempt to handle relationships in time generated by concurrent and distributed systems problems. Approaches to the temporal specification and semantic representation of programs can be grouped into three categories: Operational: In this approach, programs are considered to be generators of program state sequences. Temporal reasoning about a program proceeds by examining properties of possible sequences of states. Denotational In this approach a program is regarded as a function from some set of inputs to some set of outputs. Since it is difficult to introduce time into the concept of function mapping, this approach, in its pure form, is not often applied to temporal specifications. Deductive: This approach emphasizes the behavior of the system as derived from sets of axioms. Deductive systems are necessarily based in logic and usually take an algebraic 13 14 form. The operational approach to temporal specification and verification seems to be the most prevalent today. Operational specifications can often be executed or simulated directly, deductive approaches are used less but have greater expressive power. The deductive system analog to execution and simulation in an operational system is theorem proving. To be truly useful for significant applications, a deductive system requires automated theorem proving tools. The denotational approach is used rarely for temporal specification, mostly because function application tends to be atemporal. In this paper we survey a variety of techniques for specifying temporal properties of systems. Each of the approaches discussed above is covered by one of more of the techniques. The remainder of this chapter is organized as follows: In Section 3.1 we survey pro- cess algebras and discuss their origins relative to CSP. In Section 3.2 an example of an extended process algebra called LOTOS, is presented. Section 3.3 examines temporal char- acteristics of process algebras in more detail. Section 3.4 surveys two specification systems that focus on the flow of data through the system, known as Streams. In Section 3.5 the temporal characteristics of stream networks are examined in more detail. An algebraic de- ductive system called Ina Jo, extended with temporal operators, is presented in Section 3.6. Section 3.7 presents an alternative to temporal logic through a system that contains no temporal operators. Common features of the systems are drawn together and contrasted in Section 3.8. 3.1 Process Algebras — CSP and CCS Communicating Sequential Processes [26] is an early attempt to specify the properties of concurrent and distributed programs. Instead of a functional theory based on the semantic content of the program, CSP, and its derivatives are based on the notion of primitive inter- action and communication. The following example illustrates the motivation for focusing on interaction and communication: Suppose we have two fragments of a program: 15 X:=1 and X:=0 X:=X+1 In the absence of any interfering agent, the post-condition of both fragments is X = 1. 0n the other hand, if some devious agent is executing in parallel with the above fragments and interferes with the second fragment by setting X := 1 between the statements X := 0 and X := X + 1, the two fragments produce different results. The difference in behavior between the two sections of code is due to communication through variable X and interaction at an inopportune time. The problem illustrated in this example has led to specification systems that concentrate on interaction and communication. CSP is a procedural approach to specifying concurrent system properties that relies heavily on the notion of agents, interaction and communication. The major features of CSP are Dijkstra’s guarded commands for sequential process control, both sequential and parallel composition constructs, the latter to permit multiple processes to begin and execute together, and a simple notation for communication and synchronization between processes. Since CSP has been widely covered in the literature, only the basic constructs and ideas required for background will be discussed here. The central idea of CSP is a set of concurrent cooperating communicating processes. Each process can manipulate local process variables with a variety of assignment and arith- metic operators. Communication between processes is accomplished by two basic operators. A statement of the form C !V generally denotes the value V output on channel C. A state- ment of the form C?V generally denotes waiting for and receiving a value on channel C which is assigned to V. Channels between processes are assumed to exist by virtue of definition and are associated with an identifier, such as C in the example. An interaction between processes through a channel is assumed to be instantaneous and to require the complement operation in some other process for completion. For example, each C ?V form must have a matching C !V form ready to execute somewhere in the model for the former process to continue. Matching transactions explicitly synchronize processes and form the 16 basis of interactions between processes. A CSP construct of the form AHB indicates parallel execution of A and B. Combined with the channel operators, a construct of the form (n = n + 1; Cln)|[(C?m) (3.1) describes a classic producer-consumer relationship. In Statement (3.1) everything between parentheses denotes a process. Two processes in parallel composition are described in Statement (3.1). The first process generates numbers that are presented to the second process on channel C. The second process consumes the numbers offered by the first process. The production and consumption are perfectly synchronized by the requirement that each send operation must find a matching receive operation in order for each to continue. Communication and synchronization are permitted between any number of matching processes, thus one producer can satisfy many consumers simultaneously. Guarded com- mand construction and semantics follow Dijkstra’s definition, for example: G] => CllnG'z => Cle . . -UGn 3 Cln, (3.2) where G,- is the guard statement predicating the execution of statement Cl,-. CSP also contains an iterative command, variable typing, and many more constructs, matching the facilities of many programming languages. Unlike languages introduced later, CSP vari- able typing is fairly simple and limited to simple non-aggregate types such as integer and character. The primary contribution CSP has made to other specification systems is a syntax and semantics for specifying, and even executing, parallel processes in a synchronized fash- ion. CSP contains no explicit temporal operators since temporal relationships are implied through the construction of the CSP program. About the same time CSP was being developed, R. Milner proposed A Calculus of Communicating Processes (CCS) [27]. CCS has been further refined [28] and serves as the basis of the LOTOS specification system discussed later. Like CSP, CCS is based on the notion of interaction and communication but adds the dimension of encapsulation and observational equivalence. The processes of CSP are known 17 as agents in CCS. CCS is a mix of procedural and algebraic systems that contains rewrite rules for transforming statements. CCS rewrite rules are used for simplification and to denote the meaning of the specification. CCS is not based on logic and is not directly deductive. Instead, CCS rehes heavily on its syntax and context for meaning. Both CCS and CSP fall into a class of specification systems called process algebras. The following example, taken from [28], illustrates the use of CCS. Suppose we have two people, jobbers, sharing a hammer and a mallet at a workbench on a production hne. Unassembled parts flow in from one side of the bench and finished assemblies are required to flow from the other side of the workbench. Component assembly consists of inserting a peg into a base, which can sometimes be done by hand, sometimes with either a mallet or a hammer, and occasionally for very difficult jobs, only with a hammer. This example involves scheduling of limited resources (a hammer and a mallet) and coordination between agents (the jobbers). The description of a jobber is shown in Figure 3.1. Line 1 of Fig- ure 3.1 contains an axiom that specifies when Jobber receives input, denoted “in”, for some job, job, the rule whose left side is labeled Start is followed next. Although this appears deductive, the semantics more closely follow an algebraically specified transition rule, hence our justification for calling CCS “procedural”. Several other characteristics of CCS are illustrated in this example. The identifier to the left of the dot in each rule denotes Action while the subject to the right of the dot denotes the Agent receiving the action. A complete rule, or axiom, consists of a new “state” (the agent operating next) and the actions involved in the transition. Parameters such as job can be passed between rules. Formal descriptions of the semantics for value passing is very complex and omitted here. Line 5 of Figure 3.1 illustrates the use of alternation, denoted by +. The Usetool predicate can be satisfied either with Usehammer or Usemallet. Usetool appears as a next state from Line 4 in the Start( job) rules. Line 6 of Figure 3.1 specifies how a hammer can be used. CCS uses the idea of a labeled transition to indicate action. Figure 3.2 shows a diagram for the interaction between the jobber and the hammer. In CCS notation, overlines are 18 Jobber ‘é’ in(job).Start(job) Start(job) dg if easy(job) then Finish(job) else if hand(job) then Usehammer(job) else Usetool(job) Usetool(job) déf Usehammer(job)+ Usemallet(job) Usehammer{job) d-i-f Wfinishfiob) Usemallet(job) “.1! getTprit—hfinishfiob) Finish(job) dg m(done(job)).Jobber Figure 3.1. CCS Description of Jobber’s Behavior oath 96“) Hammer) < Jobber puth 97h Figure 3.2. Transisition Diagram for Jobber and Hammer used to signify complementary sides of a communication. Neither side is designated as the input or output. CCS rules require that only complements can interact. When Line 6 of Figure 3.1 is combined with the diagram in Figure 3.2, we see that the axiom specifies that the completed transaction of getting and putting a hammer is equivalent to the transitions that put the jobber into a Finish state. Parallel composition of several agents is denoted by a vertical bar. Using this notation, the two jobbers and the hammer would be written as (JobberlJobberlHammer). (3.3) If we add Mallet to Expression (3.3) we get Expression (3.4) that gives a complete specifi- cation for the jobshop: 19 (JobberIJobberI Hammerl Mallet). (3.4) As a specification grows in complexity and requires higher levels of abstraction, complex agents can be constructed from a series of simpler agent expressions. In CCS definitional meta-notation, but not in the CCS language itself, action and transition are denoted by: p _'_+ Q (3.5) where P and Q are agents associated with states and l is the action that caused the tran- sition, or agent Q to act. Note that this notation is not part of CCS, itself, but rather a notation used to describe actions in CCS. Referring again to the jobshop example, the rule: Hammer dg geth.Busyhammer (3.6) signifying that a hammer becomes busy through the geth action (see Figure 3.2) is written in labeled transition notation as: Hammer 51".: Busyhammer (3.7) If we intend to use the entire jobshop as an agent in a larger model, we may wish to hide the interactions between jobbers, the hammer and the mallet. Hiding is accomplished through a Restriction operator, “\.” An expression of the form (AlB)\c means the c action is private to the composition of A and B. If an action between members of a composite is not hidden, it is possible for the action to be supplied by a third agent. Suppose we define agents A and B as follows: A déf a.A' (3.8) A’ “'2 M (3.9) B {if c.B’ (3.10) B’ “.3 EB (3.11) Since: A .1. A’ (3.12) 20 we can infer that AlB _°_. A’|B (3.13) because B does not take part in A’s transition. a can be supplied to A by an outside agent and leaves B unaffected. When placed in composition, we can immediately see that A and B can interact, or hand- shake, through complementarylactions c and E without the outside world. Statements (3.12) and (3.13) imply a rule for writing transitions for compositions, but the handshake produces A’ i. A and B —°_. 8’ (3.14) This indicates that A and B change state simultaneously and presents the question of how to write a handshake transition. CCS solves this with a 7 transition, also called a perfect transition, which is written as follows: A’lB —'» AIB’. (3.15) The meaning of 1' is that both agents change state simultaneously through a handshake interaction. 1' transitions require pairs of actions of the form (a,?I) within the composition. A statement of the form of (3.15) denotes that although both c and E are available outside of the composition, there is an internal, hidden handshake possible between them. The restriction operator can explicitly hide the handshake: C = (AIB)\c (3.16) so only transitions a and b are observable. Agent C is now defined by the equations: Co dé’ 5.0. + a.C2 (3.17) 01 ‘11! (1.03 (3.18) 02 “’2 3.03 (3.19) 1The actions are complementary in the sense that they are opposite sides of a handshake operation. The actual contents of the actions do not have to form a “complement” in the logical sense 21 03 “‘é’ ac, (3.20) Multiple compound internal handshake operations can produce expressions such as T Pl—I-rPg-L...—>P,, (3.21) that CCS rules allow reduction to P1 —T—> P, (3.22) Although it may seem that 1' actions can always be ehminated and ignored, the following example shows this case is not true. One has to be very careful how an agent with internal structure is reduced? Consider a recursively defined agent: D = d.D + 1'.e.D (3.23) with a transition graph represented as follows: The meaning of Equation (3.23) and Figure 3.1 is that state D can result from action d or an internal transition (1') followed by action e. If the transform 1".P -+ P (3'24) were always valid then agent D described by Equation (3.23) would be equivalent to and agent E described by: E = (LE + 8.E (3.25) and E’s transition graph would be as follows: 2Milner claims in [28] one has to be very careful how r involved statements are reduced. -‘l 22 E But are agent D and agent E really the same? Agent E always accepts either d or e and “resets” again ready to accept either action. The behavior of D is different. From the initial state of D, only d is valid. If the r transition has occurred, only e is acceptable. The external, observable behavior of D and E differ in that D appears non-deterministic while E is deterministic. We suggest, without proof, that the 1' transition can always be ignored in composition except when it occurs first, that is, syntactically on the left side of a construct. At all other times, 1' is truly internal and unobservable. When on the left, it is observable in the sense that the handshake(s) must occur before the composed agent is ready for other external actions. The justification for 1' arises from the premise that only observable interactions are important. In a composition, an internal handshake is not observable directly, although its effects are. The handshake therefore needs a representation (for the reasons just seen), but not a detailed description. As mentioned earlier, CCS includes a variety of complex expressions and inference rules for reducing equations to equivalent forms. The major agent expressions of CCS, some of which have already been introduced are: 1. a.E, denotes a is a prefix action to agent E 2. 2,6119, is shorthand for E1 + E2 + E3 + . . ., denoting alternation. 3. E1|Eg as introduced, denotes the parallel composition operation. 4. E\L is written for restriction that hides all actions in L (L may be a set of actions) 5. E[ f] denotes relabehng where f is a relabeling function that re-writes E according to the rules of f. 23 For each of the constructs above, there is at least one inference rule to manipulate the algebra. For example, the composition rules already introduced have the following rules: E -°—'v E’ 3.26 EIF —°> E’IF ( ) E —'> E’, F i» F’ ., (3.27) EIF —+ E’IF’ A simple transition is defined as : a.E 1+ E (3.28) Rule (3.26) and (3.27) have already been discussed. Rule (3.28) is a formalization of the intuitive notation that E is followed after the or action takes place. Although deductive in form, these rules are not part of a deductive system. The 1' transition appears in some sense to be at the core of CCS. Composition and observable action are foundational CCS ideas, and the 1' transition is important to both. Observable action, as seen by the example of an equivalent C agent constructed for A and B above, forms a central theme appropriately called observational equivalence. In that example, Statements (3.8) through (3.11) were replaced by Statements (3.17) through (3.20) thus forming agent C. Agents that appear to behave equivalently can be inferred to be interchangeable. 1' plays the role of abstracting away handshake details internal to A and B’s interaction. Process algebras statements, and CCS statements in particular, are frequently manipulated for simplification and equivalent forms. A frequent proof technique is to show that one form of an agent expression is equivalent in some way to another. This concept is known as Bisimulation. Bisimulation, and therefore observational equivalence, can take on many forms. The two primary forms are called strong and weak, each denoting equivalence between agents from a certain point of view. It appears that there may be many forms of observational equivalence, depending on what is observed and how equivalence is defined. Traditional automata theory provides a definition of equivalence based on the languages a state machine accepts. Both strong and weak equivalence are based differently. As an 24 \ o 1‘ b A, \‘B a B] b B: C \l‘ . 3: ° >8. Figure 3.3. Language equivalent state machines with differing behavior example, borrowed with modifications from [28], consider the two descriptions in Figure 3.3. If treated as finite state automata, we can easily see that both accept the language: L = (a.c.d)".a.b.0 (3.29) where 0 denotes a state from which the agent cannot escape. Although L represents the language for both diagrams, B is non-deterministic and after accepting a can choose to either accept c or b but not both. Agent A, on the other hand, accepts either b or c. An experimenter trying multiple runs of sequences on both A and B would identify this behavioral difference, and find nothing she can do determines whether b or c is accepted next after a by A. Agents A and B are not strongly equivalent. To be strongly equivalent, two agents must have corresponding transitions for each action. This means they must always behave in an identical fashion for a sequence of operations. The algebra used to completely describe and reason about concurrent systems in CCS is much more complex than described here and space limitations do not permit a thorough treatment of the subject. Milner has more completely described process algebras and the ideas on which CCS is based in [28]. 25 3.2 LOTOS LOTOS [29] (Language of Temporal Ordering Specifications) is a formal description lan- guage based on many of the formalisms and syntax from CCS and CSP. Although LOTOS is a process algebra, its syntax is more procedural than CCS or CSP and resembles imper- ative programming languages. In fact, systems for executing LOTOS specifications have been constructed [30]. LOTOS’s CCS heritage is so strong that the LOTOS interpreter described in [30] transforms LOTOS specifications into CCS prior to execution. LOTOS contains a rich set of operators and has a syntax at least as complex as CCS. For a description of the entire LOTOS language see [29]. The basic LOTOS constructs are presented in this paper as a framework for discussion of the temporal characteristics of LOTOS. LOTOS’s procedural constructs emphasize communication and interaction between pro- cesses using notions very similar to CSP and CCS. It’s primary emphasis on procedural contents, using the interaction-communication paradigm, are the justification for classify— ing LOTOS as a process algebra. Basic LOTOS units of action, equivalent to CCS agents, are called processes. Expres- sions involving process identifiers, communication and synchronization constructs, and pro- cess composition, are called behavior expressions. LOTOS specifications are a marriage of two types of specification methods: procedurally oriented state transition descriptions that are used for process descriptions, and an algebraic abstract data type (ADT) description language used for complex objects and special variable types manipulated by processes. LOTOS’s ADT language is a typed algebra employing axioms and is derived from ACT ONE [31]. The ADT portion of LOTOS is used to describe the behavior of the objects manipulated by processes in the procedural portion of a LOTOS specification. Objects described in the ADT language can be freely used in behavior expressions and behavior expressions can invoke ADT functions defined within the ADT specification. An example of a commonly found use of LOTOS behavior expressions combined with ADT specifications is a system that contains communicating systems with multiple processes 26 requiring a. queue for interaction. The behavior of the system processes is described with a process definition containing behavior expressions that resemble CSP and CCS constructs. The queue data structure is described through a series of function signatures and universally quantified axioms specifying how the queue and its functions behave. An example using an ADT description of a natural number type is given later. LOTOS adopts the “l” and “1’” operators from CSP to denote synchronization through output and input, respectively, on an associated channel. A sequential series of actions are composed with the “;” operator. For example, the expression a?a:; b?y; cllargest(:c, y); stop (3.30) specifies reading variable a: from port a followed by reading variable y from port b, then outputting the larger of the two values on port c. Two special actions, stop and exit, signify halting a process and terminating a process normally, respectively. The stop process is capable of no further action, including termination. It offers no actions that can be matched and it can match no actions. The special process exit signifies normal termination. The process expression containing an exit terminates normally, an event which may be observed and used by other processes. Statement (3.30) is not quite explicit enough, in that we can infer from the context of specification that .1: and y are integers or natural numbers, but the type is not conveyed explicitly. Both 1: and y need typing. Typing is written in LOTOS by post-fixing variables with :type. A better form of Expression (3.30) with typing information added would then be: a?:c : nat; b?y : nat; c!largest(:c, y); stop. (3.31) The description of function largest(a:, y) is found in conjunction with the definition of type nat. This is a typical example of an ADT exported function definition in LOTOS. CCS and CSP style interactions are augmented in LOTOS by providing an optional predicate to be satisfied before the interaction can complete successfully. To illustrate, the following expression: a?1: : nat[1: > 3]; b!1:;stop (3.32) 27 requires inputting :1: on port a to succeed only for offered values of 0,1 and 2. Until one of these values is offered by another process, this process waits. Interactions within composed processes is captured by the concept of the i action that denotes “internal”, or hidden action. The i action is equivalent to the CCS 1' transition. The idea is that an action external to a macro-process may trigger a series of actions with the macro-process that are to be hidden from the rest of the system. Hidden, in the LOTOS, sense means actions on channels are not to be available for transition matches elsewhere in the system. Hiding appears to have its greatest use in composed processes that require internal synchronization that is not to be interfered with by any later additions or deletions to the specification. LOTOS contains a complete set of constructs for composing processes sequentially, concurrently, with guards, and with alternation. Normal sequential composition has already been introduced in the form A; B. Enabling composition is denoted by A > B and is interpreted to mean B is enabled upon, and only upon, the successful termination of action A. Note that if A contains a stop, B will never be enabled. LOTOS has three major constructs to signify parallel operation and synchronization of processes. The formal description is somewhat complex, so the explanation here will be by example. We will begin by breaking down the following expression: a; c; stop|[c]|b; c; stop (3.33) The three composed actions to the left of “I” form one composite process made from actions a, c, and stop. The three terms to the right of the second “I” form a second process. The first process is free to execute action a at any time and similarly, the second is free to execute action b at any time. Once both a and b have occurred, each macro-process is ready to execute action c, but only in synchronization. Vertical bars in LOTOS denote parallel composition of processes. Processes of the form of Expression (3.33) mean that the parallel composition can continue only when each process is ready to execute the shared actions between the bars. The shared actions are called synchronization gates in LOTOS. In Expression (3.33), the synchronization gate is c. This statement represents the temporal 28 notion “a and b before c” When the set of synchronization gates is empty, the composed processes are free to execute in parallel in a pure interleaved mode. This is denoted by A|||B in LOTOS notation. When all gates (actions) are in common between processes, the composed processes are in full synchronization and must proceed in lockstep as each action of each process occurs. This is denoted by AIIB. The alternation command takes the form A[]B. The informal meaning of alternation is either A or B may be executed depending on the interaction of A and B with their environments. The alternation expression a; b; c; stop[]b; a; c; stop (3.34) offers either action a then b followed by c, or b then a, followed by c. Expression (3.34) is, in fact, exactly equivalent to Expression (3.33). Alternation also permits the specification of non-determinism as follows: a; b; stopfla; c; stop (3.35) Expression (3.35) permits either b or c after a as neither is specified as preferred and there is no environmental action possible that would choose one over the other. Unlike a non—deterministic automata, Expression (3.35) implies no look-ahead. Once an alternative has been (non-deterministically) chosen, execution will continue along the chosen path. If a;c is the required behavior in Expression (3.35), then the expression permits a;b to be nondeterministically chosen and a deadlock to potentially occur. Alternation combined with the hidden i action is often used in protocol specifications to provide a kind of asymmetric nondeterminism. Statements of the form: normal-course-of-actionfli; disconnect-indication (3.36) appear frequently in connection with protocols. Guarded commands take a form very similar to alternation. Given a guard predicate P, [P] —+ A has the expected interpretation of executing A when P is true. A series of guards combined with alternation forms a case statement. 29 type natural is sorts nat opns zero:—> nat succ: nat -> nat largest: nat, nat -> nat eqns ofsort nat forall x,y: nat largest(zero, x) = x; largest(x, y) = largest(y, x); largest(succ(x), succ(y)) = succ(largest(x, y)); endtype Figure 3.4. Algebraic description of type not Returning to the example in Statement (3.31), above, type nat and function largest() re- quire definition. This is accomplished in the LOTOS abstract data typing language (ADT) as shown in Figure 3.4. The ADT language is an algebraic specification language derived from ACT ONE [31] based on axioms and rewrite rules, but unlike many algebraic lan— guages, LOTOS’s language has provisions for parametric types. The ADT language plays no particular role in the temporal characteristics of LOTOS specifications. 3.3 Temporal Characteristics of Process Algebras All process algebras concentrate on temporal properties such as synchronization, safety, and precedence from a procedural, process interaction point of view. For example, LOTOS Expressions (3.34) and (3.35), earlier, both make equivalent algorithmic statements about the temporal precedence of a, b, and c. Assuming the existence of a two place infix pred- icate “<” meaning one action is before another, the intention of both Expressions (3.34) and (3.35) could be concisely expressed in declarative form as: (a