Model Checking in Concurrent Programming Teaching
Artur Krystosik · 2007
The paper presents an application of model checking in teaching a concurrent programming. The success of this approach is based on features of DT-CSM automata and EMLAN modeling language. EMLAN is a C-like, high level language for modeling and model checking of embedded systems. The language is equipped with a lot of synchronization mechanisms (semaphores, mutexes, monitors). This allows easy modeling and verification of concurrent, cooperating tasks, which is very useful for educational purposes. As an example, a typical student exercise: a producer-consumer is given.