IntroductiontoProcessAlgebra(进程代数)_CSPcontrolsequentialprocess

5星 · 超过95%的资源需积分: 19 48 浏览量更新于2023-05-26 评论收藏 1005KB PDF 举报

身份认证购VIP最低享 7 折!

领优惠券(最高得80元）

资源详情

资源评论

资源推荐

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

Contents

1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

2. Basic Process Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2.1 Basic Process Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

2.2 Transition Rules for BPA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

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

Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167

剩余173页未读，继续阅读

treefound

2013-05-20

当时做进程代数的时候看过，算是这个领域还不错的一份资料，建议初学者先建立基本概念再深入研究

wofy2008

粉丝: 3
资源: 14

会员权益专享

Introduction to Process Algebra(进程代数)

评论2

会员权益专享

最新资源

Introduction to Process Algebra(进程代数)

评论2

Introduction to Linear Algebra [Fifth Edition] 答案

INTRODUCTION TO LINEAR ALGEBRA 清晰版 第五版 习题解答

Introduction to Linear Algebra(第四版答案).pdf

Solutions Manual for Introduction to Linear Algebra 5th 习题解答.pdf

Introduction to Linear Algebra 5th Gilbert Strang

introduction to linear algebra

introduction to linear algebra电子版

introduction to linear algebra中文版

Linear Algebra 线性代数课后答案

introduction to linear algebra 1.3 中文版

【免费提供】Introduction_to_Linear_Algebra_5th_Gilbert_Strang

统计学的矩阵代数:Matrix algebra from a statistician's perspective,2008

线性代数 矩阵的秩 ppt

linear algebra and its applications

Elementary Linear Algebra Applications 11th

numerical linear algebra

linear algebra done right中文版

Linear Algebra and Its Applications Fourth Edition by Gilbert Strang 带目录书签

会员权益专享

最新资源

INTRODUCTION TO LINEAR ALGEBRA 清晰版第五版习题解答

线性代数矩阵的秩 ppt