Model-based Development of Concurrent Programs

We will use the following design, implementation, and testing steps. Good design is a result of an iterative (creative) problem-solving process. At each step, we may need to go back one or more steps to refine the design to meet functional and/or performance specifications.

1. Programming logic proofs of safety and correctness in concurrent programs

2. Build model in modeling language (PROMELA)

3. Verify safety, security, and performance properties of the model

4. Translate model to concurrent programming language (Concurrent Java)

a. Encapsulate shared variables in objects

b. Build monitor synchronization code

5. Verify safety, security, and performance of the real synchronization code

6. Optimize thread-switching (and re-verify) until suitable performance

7. Add application code and test