| 
|
Topic: calculus of communicating processes
topics >
computer science >
communicating sequential processes
Topic:
formal methods and languages
Topic:
models of parallel computation
Topic:
Petri net transitions and events
Topic:
proving concurrent programs
Topic:
requirement specification by behaviors
Topic:
specification and design of distributed systems
Topic:
synchronous communication through a channel
Summary
A process calculus is a formal notation for composing processes. It is used with communicating sequential processes. Processes may be selected, execute concurrently, or execute in a pipeline. A process may be triggered by an event. Each process and event has a name. (cbb 4/28)
Subtopic: pi-calculus
Quote: combine Petri net theory with a compositional view of systems; like combining Turing machines with lambda-calculus [»milnR1_1993] Quote: combine occam process by sequence, conditional, parallel, or alternative [»mayD_1987] Quote: mathematical functions are a good foundation for sequential computation; nothing comparable for concurrent programming [»milnR1_1993]
Subtopic: events
Quote: the key idea of pi-calculus is naming or reference; concurrency requires the independent identity of its components [»milnR1_1993] Quote: pi-calculus expressions consist of names and processes; names may be a channel or a datum [»milnR1_1993]
Subtopic: CSP notation
Quote: to describe patterns of behavior, first pick names for types of events; i.e., event classes [»hoarCA_1985] Quote: an object's 'alphabet' is the set of names of events that it can engage in [»hoarCA_1985] Quote: the alphabet (events) for an object simplifies its behavior; e.g., ignore emptying the coin box of a vending machine [»hoarCA_1985]
Quote: in CSP, x->P describes an object engaging in event x and then doing process P [»hoarCA_1985] Quote: in CSP, (x->P | y->Q) describes an object that engages in events x or y and then behaves as process P or Q [»hoarCA_1985] Quote: P||Q is a process composed of synchronous, interacting processes P and Q; same as Q||P [»hoarCA_1985] Quote: P||Q are concurrent when the alphabets of P and Q differ; only shared events require simultaneous participation [»hoarCA_1985] Quote: a process specified by 'P .upendedBox. Q' can be implemented by building either P or Q; non-deterministic
[»hoarCA_1985]
Topic: communicating sequential processes (33 items)
Topic: formal methods and languages (53 items)
Topic: models of parallel computation (33 items)
Topic: Petri net transitions and events (21 items)
Topic: proving concurrent programs (37 items)
Topic: requirement specification by behaviors (16 items)
Topic: specification and design of distributed systems (14 items)
Topic: synchronous communication through a channel
(28 items)