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