Overview From
Feb 13, 1997
Using CCS to
model a system
- What are the agents?
- What are the actions?
- What exactly do we want
to model?
Critical Region
Problem
- Agents:
Process1, Process2, and Lock
- Action:
action (represents the Critical Region)
- Safe System:
(Process1 | Process2 | Lock)
\ {lock, unlock}
Process1 = lock.action.unlock.Process1
Process2 = lock.action.unlock.Process2
Lock = lock.unlock.Lock
- Trace:
(action, action, action, … , action, action)
Duration of Each
Process in C.R.
- Modeling Duration
- beginning event
- ending event
- Process1 and Process2 revised
- Process1 = lock.enter1.exit1.unlock.Process1
- Process2 = lock.enter2.exit2.unlock.Process2
- Trace
(enter1, exit1, enter2, exit2,
… , enter2, exit2)
Bounded Buffer Problem
- Buffer bounded by N
- How do you count in CCS?
Make N + 1 buffers to represent
its states
Let N = 2
Buffer0 = put.Buffer1
Buffer1 = put.Buffer2 + get.Buffer0
Buffer2 = get.Buffer1
Does the System
Work?
- Critical Region:
- Spec=enter1.exit1.SafeSpec+enter2.exit2.Spec
- Is the System equal to the Specifications?