Testing Concurrent and Parallel Software, 2017 (1DL570)
Promela Models
- Useful macros
- Promela Models in the first lecture
- Promela Models corresponding to the first set of exercises
- Models of a simple Alternating Bit Protocol
- ab-1.pml, ab-2.pml, a test harness with a counter: ab-harness-seed.pml, a test harness with only two distinct messages: ab-harness-rwb.pml
- Models of the simple Mutual exclusion protocol
.