Using model checkers in an introductory course on operating systems
- 1 October 2008
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGOPS Operating Systems Review
- Vol. 42 (6), 101-111
- https://doi.org/10.1145/1453775.1453793
Abstract
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.Keywords
This publication has 10 references indexed in Scilit:
- Checking a Multithreaded Algorithm with + CALLecture Notes in Computer Science, 2006
- UPPAAL 4.0Published by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Verification of mutual exclusion algorithms with SMV systemPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- A Tutorial on UppaalLecture Notes in Computer Science, 2004
- Myths about the mutual exclusion problemInformation Processing Letters, 1981
- Experience with processes and monitors in Mesa (Summary)Published by Association for Computing Machinery (ACM) ,1979
- MonitorsCommunications of the ACM, 1974
- The humble programmerCommunications of the ACM, 1972
- Hierarchical ordering of sequential processesActa Informatica, 1971
- Comments on a problem in concurrent programming controlCommunications of the ACM, 1966