Design of Concurrent
Software
1. Basic sequential programming
a. Object-oriented software engineering
tools and procedures – use cases, object model, sequence diagrams, etc.
b. Add shared variables – orders of
magnitude more states
2. Building a Model of a Concurrent Program
a. Develop the Object Model
b. Develop Collaboration Diagram
c. Isolate shared variables
d. Use await until(RelationalExpressionOnSharedVariables) to synchronize processess
3. Build model in Promela
a. Example: model of a bounded buffer
i.
Object Model
ii.
Shared Variables
1.
Number of empty buffers – NBuffEmpty
2.
Number of full buffers – NBuffFull
iii.
Condition for Consumer to GetBuff is NBuffFull > 0
iv.
Condition for Producer to PutBuff is NbuffEmpty > 0
vi.
Use wait until to synchronize
producers and consumers