Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben

2010 | Buch

Building a Simple Sequential Process Kapitel lesen Erstes Kapitel lesen

Understanding Concurrent Systems

verfasst von: A.W. Roscoe

Verlag: Springer London

Buchreihe : Texts in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

CSP notation has been used extensively for teaching and applying concurrency theory, ever since the publication of the text Communicating Sequential Processes by C.A.R. Hoare in 1985. Both a programming language and a specification language, the theory of CSP helps users to understand concurrent systems, and to decide whether a program meets its specification. As a member of the family of process algebras, the concepts of communication and interaction are presented in an algebraic style. An invaluable reference on the state of the art in CSP, Understanding Concurrent Systems also serves as a comprehensive introduction to the field, in addition to providing material for a number of more advanced courses. A first point of reference for anyone wanting to use CSP or learn about its theory, the book also introduces other views of concurrency, using CSP to model and explain these. The text is fully integrated with CSP-based tools such as FDR, and describes how to create new tools based on FDR. Most of the book relies on no theoretical background other than a basic knowledge of sets and sequences. Sophisticated mathematical arguments are avoided whenever possible. Topics and features: presents a comprehensive introduction to CSP; discusses the latest advances in CSP, covering topics of operational semantics, denotational models, finite observation models and infinite-behaviour models, and algebraic semantics; explores the practical application of CSP, including timed modelling, discrete modelling, parameterised verifications and the state explosion problem, and advanced topics in the use of FDR; examines the ability of CSP to describe and enable reasoning about parallel systems modelled in other paradigms; covers a broad variety of concurrent systems, including combinatorial, timed, priority-based, mobile, shared variable, statecharts, buffered and asynchronous systems; contains exercises and case studies to support the text; supplies further tools and information at the associated website: http://www.comlab.ox.ac.uk/ucs/. From undergraduate students of computer science in need of an introduction to the area, to researchers and practitioners desiring a more in-depth understanding of theory and practice of concurrent systems, this broad-ranging text/reference is essential reading for anyone interested in Hoare’s CSP.

Inhaltsverzeichnis

Frontmatter

A Foundation Course in CSP

Frontmatter
Chapter 1. Building a Simple Sequential Process
Abstract
We introduce the syntax that CSP uses to create basic sequential processes: prefixing, recursion and conditional, external and internal choice. The ideas and syntax of events and channels is introduced. We learn the distinction between deterministic and nondeterministic behaviour. Examples include buffer and counter processes, and processes that describe a human’s life in terms of constituent events. We see the ideas of traces and trace refinement. The FDR tool is introduced, as is its input language CSP M .
A. W. Roscoe
Chapter 2. Understanding CSP
Abstract
This introduces the three types of formalism that this book uses to study CSP. The first of these is algebra: we give and explain many examples of algebraic laws that CSP operators satisfy as well as comparing these to familiar laws from arithmetic and set theory. Denotational semantics is based on behavioural models such as traces: we introduce rules for computing traces and fixed points, as well as the Unique Fixed Point (UFP) principle for guarded recursions. Operational semantics are motivated by LTSs and the operation of FDR. We discuss trace refinement in depth and understand how to use it in formulating and running specifications for FDR.
A. W. Roscoe
Chapter 3. Parallel Operators
Abstract
We meet the main parallel operators of CSP: synchronous, alphabetised, interleaving and generalised parallel. We see how processes can influence each other and transfer data along channels by synchronising on all or some of their events. Examples include people trying to agree on joint lives, bargaining in a shop, and the five dining philosophers who can deadlock through contention for resources. All of these are implemented in the accompanying example files, and we explain how these new operators affect FDR.
A. W. Roscoe
Chapter 4. CSP Case Studies
Abstract
This chapter introduces a number of case studies that we will meet many times in the rest of the book. The first of these shows you how you can code Sudoku puzzles in CSP and use FDR to solve them. The second shows how designing a routing network can easily lead to deadlock but how well designed networks can work reliably: we offer a number of alternatives for this in trees, general networks, rings and cartesian grids. The final example describes ways of overcoming an erroneous communication medium. As well as introducing the Alternating Bit Protocol and other ways of gaining reliability, we also introduce techniques for modelling error-prone systems in CSP.
A. W. Roscoe
Chapter 5. Hiding and Renaming
Abstract
We meet some new operators. Hiding (P\X) allows you to conceal the internal actions of a process from the outside world. Renaming (P〚R〛) gives a flexible way of changing the labels on the events that a process communicates into different labels seen by the outside world. We see how hiding can create more natural models of parallel systems but can create a few theoretical difficulties, and how renaming combined with parallelism can create seemingly magical effects such as allowing Adam and Eve to achieve a variable renaming so each can have their own choice of apple. We introduce link parallel: a combination of parallel, hiding and renaming that makes constructing practical networks comparatively simple, and see how it can be used in building some natural dynamic networks such as one for implementing mergesort. We find that renaming can help FDR solve Sudoku puzzles faster.
A. W. Roscoe
Chapter 6. Beyond Traces
Abstract
In previous chapters we have already discovered that traces give an incomplete picture of how processes behave, for example by failing to distinguish deterministic from nondeterministic behaviour and failing to capture deadlock properly. In this chapter we introduce the ideas of failures and divergences, which allow us to develop models that do capture these phenomena accurately. We see how these models allow to formulate and verify richer specifications on FDR. The phenomenon of divergence is described and we show one way to ensure it does not happen. We introduce lazy abstraction as a variant on hiding and show how it can be applied to capturing fault tolerance and computer security.
A. W. Roscoe
Chapter 7. Further Operators
Abstract
This chapter completes the CSP language by introducing three operators that allow one process to hand control on to another. In sequential composition P;Q this happens when the first process terminates successfully via a special action ✓. In interrupt \(P\mathrel {\mathord {\triangle }}Q\) this happens when the environment communicates an initial action of Q, and in throw \(P\mathop{ \varTheta _{A}}Q\) any occurrence of an action in A within P counts as an exception which hands control to Q. We study in particular the relationship between termination and parallel composition, and the effect of termination on the semantic models seen in earlier chapters.
A. W. Roscoe
Chapter 8. Using FDR
Abstract
This chapter describes FDR and how to use this tool effectively. We describe how to interact with the FDR user interface, and how to program in CSP M and its functional sub-language which is roughly equivalent to Haskell. We see what FDR can and cannot do, and how to play to its strengths. For example we see—in an example based on finding a Hamiltonian path—how it is better to code complex systems as parallel compositions rather than as large sequential processes. We show in outline how FDR actually carries out a refinement check, and how this algorithm can be adapted to check determinism. We discuss the relative advantages of depth-first and breadth-first search, and finally show how compression operators that FDR supplies can enable one to (at least partially) overcome the state explosion problem that limits the size of systems the tool can handle.
A. W. Roscoe

Theory

Frontmatter
Chapter 9. Operational Semantics
Abstract
This is an in-depth study of the operational semantics of CSP and of the transition systems these are based on. We study the difference between finitely and infinitely branching transition systems, and between ordinary LTSs and ones where there may be acceptance or divergence information in additional labels on states. We show how CSP can be given an operational semantics in either the traditional Structured Operational Semantics (SOS) style or in a less flexible Combinator style that captures the spirit of CSP. We show what any operator with a combinator operational semantics can be expressed in CSP. Combinators lead to Supercombinators, the technique that FDR uses to implement transition systems effectively. Finally we show how formal “observations” of transition systems allow us to deduce what a process’s traces, failures and divergences are.
A. W. Roscoe
Chapter 10. Denotational Semantics and Behavioural Models
Abstract
This chapter studies denotational semantics in more depth than in the introductory chapters. We discuss the nature of behavioural models and what is required of them. We see how CSP definitions of operators naturally lead to distributive operators, and discuss topics such as full abstraction and congruence with operational semantics. We look in detail at each of the traces, stable failures and failures divergences model, and understand their healthiness conditions. We are able to specify determinism formally and study its relationship with the related concept of confluence.
A. W. Roscoe
Chapter 11. Finite Observation Models
Abstract
There are two dimensions to study when we try to understand what behavioural models for CSP exist: what finitely observable things to record and what infinitely observable things to add to these. In this chapter we study what finite observation models exist. We examine the long-understood acceptances or ready-sets and refusal testing models. We discover two newer models: the acceptance-traces model of all finite linear observations, which is the finest possible model in this category, and the revivals model which sits above traces and stable failures, and below all other models. The structural result that proves this last fact puts ideas such as full abstraction in a completely new light. For each model we see what sorts of specification are best cast in terms of it.
A. W. Roscoe
Chapter 12. Infinite-Behaviour Models
Abstract
Here we study how infinite behaviours can be added to these models. We get three classes of models in addition to the finite observation ones. The first of these, adding only divergence, can cope with finitely nondeterministic CSP with divergence strictness. The second, in which infinite traces and similar behaviours are added, can handle infinitely nondeterministic but divergence strict CSP. In the final class divergence strictness, or at least most of it, is removed. The resulting models are very natural except for requiring an exotic fixed point theory. We are able to get similar structural results to those in Chap. 11, for the divergence-strict models.
A. W. Roscoe
Chapter 13. The Algebra of CSP
Abstract
We introduce a formal algebraic semantics for CSP. First we show how algebraic laws can systematically reduce all finite CSP terms to a head normal form, and therefore create an Algebraic Operational Semantics. Then we show how to reduce this to a normal form for the finest CSP model as developed in Chap. 12. We can then show how a small selection of optional laws such as \(P=P\mathbin{\Box}P\) allow this normal form to be transformed into normal forms for any of the main models of CSP. This provides an elegant explanation for why the hierarchy of models developed in the previous two chapters is as it is.
A. W. Roscoe

Using CSP in Practice

Frontmatter
Chapter 14. Timed Systems 1: tock-CSP
Abstract
This chapter develops the tock-CSP model of CSP introduced in Chap. 14 of Theory and Practice of Concurrency. We see how incorporating time into CSP models necessarily changes our understanding of the processes represented in this dialect. We develop a major new case study: the Bully algorithm for leadership election, and explain the use of the τ-priority model that FDR uses to support timed analysis, implementing the principle of maximal progress. We create timed versions of some of the routing algorithms described in Sect. 4.2 and compare their timed performance.
A. W. Roscoe
Chapter 15. Timed Systems 2: Discrete Timed CSP
Abstract
Here we look at the other CSP view of timed systems, namely Timed CSP in which time appears implicitly rather than as an explicit tock. We concentrate on the discrete variant of this, based on a semantic model involving tock to record the passage of time, and show how it can be implemented in a variant of tock-CSP. We use the alternating bit protocol as an example, and show how it relates to the more traditional continuous timed CSP through Ouaknine’s theory of digitisation.
A. W. Roscoe
Chapter 16. More About FDR
Abstract
This chapter covers a number of more advanced topics in the implementation and use of FDR. The first of these are in-depth studies of normalisation and the other compression operators that FDR uses, the latter including types of bisimulation and the CSP-specific diamond operator. We then look at ideas for partial order reduction and “lazy compression” including the chase operator. We look at options for using parallel execution and improved memory usage in FDR. Finally we look at ways of making FDR handle a wider range of specifications, including ones that are not refinement-closed an distributive, certain types of infinite-state specifications, and LTL.
A. W. Roscoe
Chapter 17. State Explosion and Parameterised Verification
Abstract
Here we look in depth at the state explosion problem and the related parameterised verification problem: how to prove a property of a general class of processes or networks. We look at induction and data independence separately, and combine them into data independent induction, which can handle many networks that neither parent method can. These include networks based on one of the routing examples from Chap. 4, which are proved correct in general. We study the topic of buffer tolerance: when can we prove a property of a system with buffered channels by studying the corresponding unbuffered network, typically with a much smaller state space. This is closely related to the data flow model of concurrency. Finally, we study how Counter-Example Guided Abstraction Refinement (CEGAR) can be integrated naturally into FDR.
A. W. Roscoe

Exploring Concurrency

Frontmatter
Chapter 18. Shared-Variable Programs
Abstract
This chapter shows how one can write a compiler in CSP M and base a tool around the result. In this case that compiler is for shared variable programs, so this chapter is also an introduction to that subject. We study this through examples such as mutual exclusion, including Lamport’s bakery algorithm, and the dining philosophers. The compiler is based on programs described in a CSP data type, which is generated and interpreted by the front end of the tool, which we call SVA. SVA, a front end for FDR, is available from this book’s web site.
A. W. Roscoe
Chapter 19. Understanding Shared-Variable Concurrency
Abstract
Here we look at shared variables in depth, including a study of dirty variables via the bakery algorithm and Simpson’s 4-slot algorithm (where we propose a version that avoids known difficulties arising from dirty flag variables). We also define what it means for one shared variable program to refine another one, and introduce various ideas necessary to create finite model-checked proofs of programs (such as the bakery algorithm) that involve unbounded integer types.
A. W. Roscoe
Chapter 20. Priority and Mobility
Abstract
We look at two ideas which are not normally thought of as within the scope of CSP, namely priority and mobility. These are motivated by a CSP study of finding a (chess) knight’s tour. We introduce a priority operator that is consistent with some of the standard models of CSP. As examples of priority we study Statecharts via a burglar alarm case study, and a simplified form of these, namely two-phase synchronous automata. We contemplate how to add mobility into CSP’s alphabet-based model of interaction and make a few tentative proposals, including a “closed-world” form of mobile parallel composition. This is illustrated via a model of a simple telephone network, which is also simulated in standard CSP M .
A. W. Roscoe
Backmatter
Metadaten
Titel
Understanding Concurrent Systems
verfasst von
A.W. Roscoe
Copyright-Jahr
2010
Verlag
Springer London
Electronic ISBN
978-1-84882-258-0
Print ISBN
978-1-84882-257-3
DOI
https://doi.org/10.1007/978-1-84882-258-0

Premium Partner

    Bildnachweise