Title :
Using model checking tool for teaching concurrent programming concepts
Author :
Abdulsalam, Abdulrahman AAl
Author_Institution :
Coll. of Appl. Sci., Nizwa, Oman
Abstract :
This paper presents a tool that can be used to simulate a system of concurrent processes which communicate through shared variables. Mechanisms for defining nondeterminism, atomic actions and process synchronization are supported. In addition, it includes a prototype for verifying basic safety properties such as mutual exclusion and absence of deadlocks using model checking technique. The aim is to provide teachers and students with a simple framework where concurrency concepts can be examined and grasped easily in an abstract and pure environment away from the complexities and sophistication of conventional programming environments.
Keywords :
computer aided instruction; computer science education; teaching; atomic actions; concurrent programming teaching; conventional programming environment; model checking technique; model checking tool; mutual exclusion; process synchronization; safety properties; Concurrent computing; Education; Educational institutions; Graphical user interfaces; Java; Libraries; Power system modeling; Safety; Unified modeling language; Visualization;
Conference_Titel :
Innovations in Information Technology, 2009. IIT '09. International Conference on
Conference_Location :
Al Ain
Print_ISBN :
978-1-4244-5698-7
DOI :
10.1109/IIT.2009.5413772