Title :
Model Checking in Concurrent Programming Teaching
Author :
Krystosik, Artur
Author_Institution :
Warsaw Univ. of Technol., Warsaw
Abstract :
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.
Keywords :
computer science education; distributed programming; embedded systems; finite state machines; program verification; specification languages; synchronisation; DT-CSM automata; EMLAN C-like high level language; EMLAN modeling language; concurrent programming teaching; embedded system model checking; synchronization mechanisms; Automata; Computer science; Concurrent computing; Education; Embedded system; Error correction; Information technology; Logic; Paper technology; Programming profession; Modeling; Software verification and validation; Teaching;
Conference_Titel :
EUROCON, 2007. The International Conference on "Computer as a Tool"
Conference_Location :
Warsaw
Print_ISBN :
978-1-4244-0813-9
Electronic_ISBN :
978-1-4244-0813-9
DOI :
10.1109/EURCON.2007.4400379
