Alexander M., Gardner W. (eds.) Process Algebra for Parallel and Distributed Processing

Chapman & Hall/CRC, 2009. — 440 p.This book brings together the state of the art in research on applications of process algebras to parallel and distributed processing.
Process algebras constitute a successful field of computer science. This field has existed for some 30 years and stands nowadays for an extensive body of theory of which much has been deeply absorbed by the researchers in computer science. Moreover, the theoretical achievements of the field are to a great extent justified by applications. The applications, in turn, strongly influence how the field evolves; some of the field’s success may be attributed to frequently addressing needs that arose in practice.
This book is not intended as a tutorial in process algebras, but there is space here for a brief orientation: Just as with the algebra we all learned in grade school, its ingredients include symbols standing for constant values and for variables, and operators that act on the symbols. While elementary algebra is concerned with manipulating numbers, a process algebra — or the synonymous term process calculus — is concerned with the creation, life, and death of processes that carry out computations. The emphasis is on interactions of processes among each other and with their environment. Symbols are used to stand for individual actions or events that a process may engage in; the processes themselves; channels, an abstraction used for interprocess communication; and data transmitted over the channels. Operators specify a sequential ordering of events; a choice between several events; if/then decisions; looping or recursive invocation of processes; composition of processes so that they execute concurrently, either synchronizing cooperatively on specified events, or running independently; and syntax for parameterizing and renaming so that process definitions can be reused in a modular fashion. Practitioners can use one of the classical process algebras mentioned in the Foreword — CCS, CSP, and ACP — or a more recent one such as the pi-calculus. Established process algebras have the advantage of the availability of automated tools that can be used for exploring a specification’s state space and proving properties such as absence of deadlock (see Section 9.1 for a good explanation of these provable properties). Alternatively, practitioners can extend any of the base algebras by adding new symbols and operators, or even invent a new process algebra from scratch. A key advantage of formal, mathematical notations with rigorous semantics is that one can prove that particular conditions such as deadlock states do or do not exist, not just hope for the best, or discover them at runtime.
While the notion of process algebras goes back over two decades, what is new is the rapid proliferation of parallel computing environments that need their help in transforming sequential programming models to new ones better suited to parallelism. The urgent necessity for reliably exploiting concurrent computing resources has caused researchers to press classical process algebras into practical service, along with their invention of new ones. This book is intended as a showcase for recent applications of process algebras by current researchers from diverse parts of the international computer science community. While these contributions may appear largely theoretical due to the quantities of symbols and formulas, they are, in reality, process algebras applied to specific problems. The formalism is needed to establish the soundness of the theoretical basis, and to prove that the resulting tools are properly derived.
This book will be of special interest to students of process algebras, to practitioners who are applying process algebras, and to developers who are looking for fresh approaches to software engineering in the face of concurrency. The chapters are worth studying from two perspectives: first, those who identify with the problem domains (e.g., middleware systems or multicore programming) may ask, Are the authors doing something that I could use, or can I adapt their approach? and second, those who are interested in process algebras as a tool can ask, How did the authors use a process algebra in their solution? What role did it play? How did they formally define it, and what did they prove in order to give it a sound basis? A common pattern is to first create a process algebra whose symbols and operators are tailored to the problem domain (e.g., mobile agents). Next, a virtual (or abstract) machine (VM) is defined that executes specifications in the process algebra. Because both are formally defined, it is possible to prove that the VM is correct with respect to the algebra. The last step is to implement the VM, and this may be done by transferring it into a language that is semantically close, e.g., a functional programming language. Since the target language already possesses a compiler and/or runtime framework, the job of implementation is done, at least for prototyping and demonstration purposes.Part I Parallel Programming
Synthesizing and Verifying Multicore Parallelism in Categories of Nested Code Graphs
Semi-Explicit Parallel Programming in a Purely Functional Style: GpH
Refinement of Parallel Algorithms
Part II Distributed Systems
Analysis of Distributed Systems with mCRL2
Business Process Specification and Analysis
Behavioral Specification of Middleware Systems
Abstract Machine for Service-Oriented Mobility
Specifying and Implementing Secure Mobile Applications
Part III Embedded Systems
Calculating Concurrency Using Circus
PARS: A Process Algebraic Approach to Resources and Schedulers
Formal Approach to Derivation of Concurrent Implementations in Software Product Lines