Introduction to process algebra.pdf-资料库

sindy_jen-8501733-4744300845214394576.pdf-第1页.png

第1页 / 共174页

sindy_jen-8501733-4744300845214394576.pdf-第2页.png

第2页 / 共174页

sindy_jen-8501733-4744300845214394576.pdf-第3页.png

第3页 / 共174页

sindy_jen-8501733-4744300845214394576.pdf-第4页.png

第4页 / 共174页

sindy_jen-8501733-4744300845214394576.pdf-第5页.png

第5页 / 共174页

sindy_jen-8501733-4744300845214394576.pdf-第6页.png

第6页 / 共174页

sindy_jen-8501733-4744300845214394576.pdf-第7页.png

第7页 / 共174页

sindy_jen-8501733-4744300845214394576.pdf-第8页.png

第8页 / 共174页

Wan Fokkink Introduction to Process Algebra Computer Science { Monograph (English) 2nd edition April 10, 2007 Springer-Verlag Berlin Heidelberg NewYork London Paris Tokyo Hong Kong Barcelona Budapest

Preface Computer software and network protocols are increasingly important in daily life. At the same time the complexity of software has rocketed, so that its correctness is at stake. New methodologies and disciplines are being devel- oped to bring structure to the ever growing jungle of computer technology. (Semi-)automated manipulation has become an important means in discover- ing aws in software and hardware systems. Process algebra is a mathematical framework in which system behaviour is expressed in the form of algebraic terms, enhancing the available techniques for manipulation. Concurrency is omnipresent in system behaviour, and in a large part responsible for its complexity: even simple behaviours become wildly compli- cated when they are executed in parallel. In order to study such systems in detail, it is imperative that they are dissected into their concurrent compo- nents. Fundamental to process algebra is a parallel operator, to break down systems into their concurrent components. A set of equations is imposed to derive whether two terms are behaviourally equivalent. In this framework, non-trivial properties of systems can be established in an elegant fashion. For example, it may be possible to equate an implementation to the speciﬂcation of its required input/output relation. In recent years a variety of automated tools have been developed to facilitate the derivation of such properties. Applications of process algebra exist in diverse ﬂelds such as safety criti- cal systems, network protocols, and biology. In the educational vein, process algebra has been recognised to teach skills to deal with complex concurrent systems, by representing and reasoning about such systems in a mathemati- cally clear and precise manner. This text developed from an undergraduate course on process algebra at the computer science department of the University of Wales Swansea during the autumn of 1997 and of 1998. Chapters 2-7 contain su–cient material for more than twenty hours of lecturing; a set of slides and further mate- rial to support such a course are available from my homepage (currently at http://www.cwi.nl/»wan). It is recommended to use a tool set based on process algebra, such as the „CRL tool set, the Concurrency Workbench Ed- inburgh, or the Labelled Transition System Analyser to enliven the course. „CRL speciﬂcations of the protocols in Chapter 6 can be obtained from the

VI Preface author. Appendices A and B provide useful background information; they are not intended to be included in the course. I am grateful to John Tucker for his encouragement to further develop a raw set of lecture notes, and to Judi Romijn for her support. Over the years I have beneﬂted from discussions with Jan Bergstra, Rob van Glabbeek, Jan Friso Groote, Frits Vaandrager, Alban Ponse, Chris Verhoef, Jaco van de Pol, Jos Baeten, Luca Aceto, Jos van Wamel, Steven Klusener, Bas Luttik, Dennis Dams, and many others. Amsterdam, November 1999 Wan Fokkink

Contents 1. Introduction : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 1 7 2. Basic Process Algebra : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 2.1 Basic Process Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 Transition Rules for BPA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 Bisimulation Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.4 Axioms for BPA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3. Algebra of Communicating Processes : : : : : : : : : : : : : : : : : : : : : 19 3.1 Parallelism and Communication . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.2 Left Merge and Communication Merge . . . . . . . . . . . . . . . . . . . . 21 3.3 Axioms for PAP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3.4 Deadlock and Encapsulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 4. Recursion : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 33 4.1 Guarded Recursive Speciﬂcations . . . . . . . . . . . . . . . . . . . . . . . . . 33 4.2 Transition Rules for Guarded Recursion . . . . . . . . . . . . . . . . . . . 35 4.3 Recursive Deﬂnition and Speciﬂcation Principles . . . . . . . . . . . 38 4.4 Completeness for Regular Processes . . . . . . . . . . . . . . . . . . . . . . . 41 4.5 Approximation Induction Principle . . . . . . . . . . . . . . . . . . . . . . . 44 5. Abstraction : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 49 5.1 Rooted Branching Bisimulation Equivalence . . . . . . . . . . . . . . . 49 5.2 Guarded Linear Recursion Revisited . . . . . . . . . . . . . . . . . . . . . . 53 5.3 Axioms for the Silent Step . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 5.4 Abstraction Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 5.5 An Example with Buﬁers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 5.6 Cluster Fair Abstraction Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 6. Protocol Veriﬂcations : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 71 6.1 Alternating Bit Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 6.2 Bounded Retransmission Protocol . . . . . . . . . . . . . . . . . . . . . . . . 80 6.3 Veriﬂcation Techniques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 6.4 Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

VIII Contents 7. Extensions : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 97 7.1 Renaming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 7.2 State Operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 7.3 Priorities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 7.4 Further Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 A. Equational Logic : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 113 A.1 Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 A.2 Axiomatisations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 A.3 Initial Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115 A.4 Term Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 B. Structural Operational Semantics : : : : : : : : : : : : : : : : : : : : : : : : : 123 B.1 Transition System Speciﬂcations . . . . . . . . . . . . . . . . . . . . . . . . . . 123 B.2 The Meaning of Negative Premises . . . . . . . . . . . . . . . . . . . . . . . 125 B.3 Bisimulation as a Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129 B.4 Branching Bisimulation as a Congruence . . . . . . . . . . . . . . . . . . 132 B.5 Conservative Extension . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 B.6 Modal Logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 Solutions to Selected Exercises : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 141 References : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 155

1. Introduction System behaviour generally consists of processes and data. Processes are the control mechanisms for the manipulation of data. While processes are dynamic and active, data are static and passive. System behaviour tends to be composed of several processes that are executed concurrently, where these processes exchange data in order to inuence each other’s behaviour. The picture below presents a typical architecture for a concurrent system. Each process Pi sends messages to its neighbouring processes Pi¡1 and Pi+1, giving them information on the state of Pi. The neighbouring processes use this information in their internal computations, to update their own states. ¢¢¢ P¡1 P0 P1 P2 ¢¢¢ Some examples of concurrent systems are: † A colony of ants; Ants behave as separate entities, which inuence each other’s behaviour. As soon as one ant discovers a goody such as a lump of sugar, it radiates a smell to attract other ants. Tofts [192] was able to explain certain phenomena of colonies of ants by modelling such colonies as concurrent systems in process algebra. † A network protocol, being a high-level description of a data communication procedure. As an example we consider the so-called alternating bit protocol [31]. A Sender and a Receiver are the separate processes, which in concurrency make up the system;

2 1. Introduction Sender Receiver Data elements d1; d2; d3; : : : are sent from the Sender to the Receiver via a faulty channel, so that data may be corrupted. In the alternating bit protocol, the Sender attaches a bit 0 to data elements d2k¡1 and a bit 1 to data elements d2k for positive natural numbers k. As soon as the Re- ceiver receives a datum, it sends the attached bit to the Sender via a faulty channel, to acknowledge reception. If the Receiver receives a corrupted message, then it resends the previous acknowledgement. The Sender keeps on sending out the pair (di; b) until it receives the acknowledgement b. Then it starts sending out the next pair (di+1; 1 ¡ b) until it receives the acknowledgement 1 ¡ b, et cetera. Alternation of the attached bit enables the Receiver to determine whether a received datum is really new, and al- ternation of the acknowledgement enables the Sender to determine whether a datum reached the Receiver unscathed. † A pocket calculator; 5765 + ¡ 8 9 5 2 6 3 ⁄ 0 = C 7 4 1 The buttons represent the separate actions of this system, which all inu- ence the state (i.e., the intermediate result of a computation) of the pocket calculator in a diﬁerent way. The pocket calculator in combination with a user make up a concurrent system. In this text, system behaviour is represented as a labelled transition sys- tem, which basically consists a set of nodes together with a set of labelled edges between these nodes. For example, a fraction of the full labelled tran- sition system of the pocket calculator is depicted in Fig. 1.1. Each node in this labelled transition system represents a diﬁerent state of the calculator, and an edge from one node to the other expresses that the calculator can change from one state to the other, by pushing a button; the label of an edge represents the button that has to be pushed in order to realise this state transition. In general it is much easier to study a concurrent system such as the pocket calculator by breaking it up into its concurrent components. Although its full labelled transition system is enormous, the process behaviour of the

1. Introduction 3 = 0 + 7 C 7.. 0 +.. ¡ 0 ¡.. 1 0 ¡ 1.. = 8 0 + 8.. 3 0 + 83.. = 83 ¡1 ⁄ 7 ⁄.. 4 7 ⁄ 4.. = 28 Fig. 1.1. Labelled transition system of a pocket calculator pocket calculator is not so di–cult. It can be captured by specifying the behaviour of the separate buttons, and putting them in parallel. For example, the behaviour of the +-button is displayed in Fig. 1.2, where d1; : : : ; dk are digits and m = n + d1 ¢¢¢ dk. Execution is started in the state that is pictured at the top, where the computation has the intermediate value n. Similarly, the arithmetic operations subtraction and multiplication can be speciﬂed on the data domain of numbers. An extra error element needs to be added to the data domain, to represent that the result of an arithmetic computation exceeds the screen size, or that an operation is undeﬂned (such as division by zero). n + n + :: d1 ... dk + m + :: C 0 m n + d1:::dk:: = ¡ m ¡ :: ⁄ m ⁄ :: Fig. 1.2. Behaviour of the plus button A process graph is a labelled transition system in which one state is se- lected to be the root state, i.e., the initial state of the process. If the labelled

资料库

Introduction to process algebra.pdf

相关推荐

课程资源

热门标签

最新资料