Model Checking in Concurrent Programming Teaching

Author

Krystosik, Artur

Author_Institution

Warsaw Univ. of Technol., Warsaw

fYear

2007

fDate

9-12 Sept. 2007

Firstpage

2390

Lastpage

2396

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/EURCON.2007.4400379

Filename

4400379