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

v. Collaboration Diagram

vi. Use wait until to synchronize producers and consumers