Lecture 20Reasoning with CSP

Table of Contents

Lecture 20Reasoning with CSP

CSP Concurrency: Four Lectures

Last Time

SKIP

Input/OutputChannels and Messages

Problems with this

General Input/Output

Communication

Examples

Another Example

More Examples

Sequencing

Basics of a Formal System

Semantics (for now)

Operations on Traces

Traces and || Operator

More Formally:Trace Laws

Specifications

Induction for CSP Processes

Example

tr(Y) = {<>, <coin>, <coin,choc>} ??

4. <coin,choc> ^ t satisfies NOLOSS, since

CSP: Algebraic Laws

Laws about || Processes

Different alphabets

More Laws

Example

PPT Slide

Last Slide

Alternate Description of Recursion

Email: shawnh@cs.cmu.edu

Home Page: http://www.cs.cmu.edu/afs/cs.cmu.edu/academic/class/15671-f97/www/index.html