Using model checkers in an introductory course on operating systems
conference paper
During the last three years, we have been experimenting with the use of the Uppaal model checker in an introductory course on operating systems for first-year Computer Science students at the Radboud University Nijmegen. The course uses model checkers as a tool to explain, visualize and solve concurrency problems. Our experience is that students enjoy to play with model checkers because it makes concurrency issues tangible. Even though it is hard to measure objectively, we think that model checkers really help students to obtain a deeper insight into concurrency. In this article, we report on our experiences in the classroom, explain how mutual exclusion algorithms, semaphores and monitors can conveniently be modeled in Uppaal, and present some results on properties of small, concurrent patterns.
TNO Identifier
953993
ISSN
01635980
Publisher
ACM
Source title
Operating Systems Review (ACM)
Pages
101-111
Files
To receive the publication files, please send an e-mail request to TNO Repository.