没有合适的资源?快使用搜索试试~ 我知道了~
首页Introduction to Process Algebra(进程代数)
进程代数英文为:process algebra,在英文中,这个词组中的process代表一个system(系统的)behavior(行为);一个系统就是一个能表现出各种行为的事物,在计算机世界,process主要指一个软件系统的行为;这句话很抽象,说白了就是,一个软件系统可以表现为一个动作(action),比如转换一个文件的格式,也可以发生一个个事件(event),比如格式转换完毕,另外,一个软件系统也可以在一定的序列下完成一系列动作(action);我们可以从各个角度(aspect)去观察一个系统的行为。研究者往往会关注一个角度的系统行为,这是他们会把系统进行抽象,称这种抽象为对系统行为的一种观察(observation)
资源详情
资源评论
资源推荐
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 flaws 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 specification
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 fields 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 sufficient 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 specifications 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 benefited 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
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 Specifications . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.2 Transition Rules for Guarded Recursion . . . . . . . . . . . . . . . . . . . 35
4.3 Recursive Definition and Specification 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 Buffers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5.6 Cluster Fair Abstraction Rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
6. Protocol Verifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.1 Alternating Bit Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
6.2 Bounded Retransmission Protocol . . . . . . . . . . . . . . . . . . . . . . . . 80
6.3 Verification 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 Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . 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页未读,继续阅读
wofy2008
- 粉丝: 3
- 资源: 14
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- stc12c5a60s2 例程
- Android通过全局变量传递数据
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功
评论2