Using model checking tool for teaching concurrent programming concepts

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.