{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:34:39Z","timestamp":1750307679724,"version":"3.41.0"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2008,10,1]],"date-time":"2008-10-01T00:00:00Z","timestamp":1222819200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2008,10]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/1453775.1453793","type":"journal-article","created":{"date-parts":[[2008,10,22]],"date-time":"2008-10-22T12:25:40Z","timestamp":1224678340000},"page":"101-111","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Using model checkers in an introductory course on operating systems"],"prefix":"10.1145","volume":"42","author":[{"given":"Roelof","family":"Hamberg","sequence":"first","affiliation":[{"name":"Embedded Systems Institute, Eindhoven, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems, LNCS 3185","author":"Behrmann G.","year":"2004"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/EURCON.2003.1248127"},{"volume-title":"MIT Press","year":"1999","author":"Clarke E.","key":"e_1_2_1_4_1"},{"volume-title":"Programming Languages","year":"1968","author":"Dijkstra E. W.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289519"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/355604.361591"},{"key":"e_1_2_1_8_1","unstructured":"A. Downey. The Little Book of Semaphores. Green Tea Press second edition 2005.  A. Downey. The Little Book of Semaphores. Green Tea Press second edition 2005."},{"key":"e_1_2_1_9_1","unstructured":"A. Downey. The Little Book of Semaphores. Green Tea Press 2.1.2 edition 2007.  A. Downey. The Little Book of Semaphores. Green Tea Press 2.1.2 edition 2007."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"volume-title":"Addison Wesley","year":"2004","author":"Holzmann G.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/365153.365167"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11864219_11"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/800215.806568"},{"key":"e_1_2_1_15_1","unstructured":"N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers San Fransisco CA 1996.   N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers San Fransisco CA 1996."},{"volume-title":"John Wiley","year":"2006","author":"Magee J.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","unstructured":"G. Nutt. Operating Systems: A Modern Perspective. Addison Wesley Longman 2nd ed 2000.   G. Nutt. Operating Systems: A Modern Perspective. Addison Wesley Longman 2nd ed 2000."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_2_1_19_1","unstructured":"A. Silberschatz and P. Galvin. Operating System Concepts. Addison Wesley Longman 5th ed 1997.   A. Silberschatz and P. Galvin. Operating System Concepts. Addison Wesley Longman 5th ed 1997."},{"key":"e_1_2_1_20_1","unstructured":"W. Stallings. Operating Systems: Internals and Design Principles. Prentice-Hall 5th ed 2005.   W. Stallings. Operating Systems: Internals and Design Principles. Prentice-Hall 5th ed 2005."},{"issue":"3","key":"e_1_2_1_21_1","article-title":"The free lunch is over -- a fundamental turn toward concurrency in software","volume":"30","author":"Sutter H.","year":"2005","journal-title":"Dr. Dobb's Journal"},{"key":"e_1_2_1_22_1","unstructured":"A. Tanenbaum and A. Woodhull. Operating Systems: Design and Implementation. Prentice-Hall 2nd ed 1997.   A. Tanenbaum and A. Woodhull. Operating Systems: Design and Implementation. Prentice-Hall 2nd ed 1997."}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1453775.1453793","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1453775.1453793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:29:45Z","timestamp":1750253385000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1453775.1453793"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10]]},"references-count":22,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2008,10]]}},"alternative-id":["10.1145\/1453775.1453793"],"URL":"https:\/\/doi.org\/10.1145\/1453775.1453793","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2008,10]]},"assertion":[{"value":"2008-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}