Using Model Checkers in "Intro to OS" Courses

The advent of mature model-checking tools has made algorithmic model-based verification much more accessible to the average computer scientist/engineer. So much so that we can now teach first-year students to use model-checking tools by sweeping essentially all of the theory behind them under the carpet. See, for example, the very recent experience report:

Roelof Hamberg and Frits Vaandrager. Using Model Checkers in an Introductory Course on Operating Systems. Technical Report ICIS-R07031,
ICIS, Radboud University Nijmegen, December 2007.

I strongly recommend reading this report to anybody with even a passing interest in formal methods. It is well written, content rich, and presents material that can inspire many of us in the lecture room. I myself wish that the paper had been posted last August, when I was planning (at the last minute) a second-year course on Operating Systems. I would have used the authors' tips and teaching material then. Not to mention great quotes like:

“Programs are not released without being tested; why should algorithms be published without being model checked?” (Leslie Lamport)

Last November, on the spur of a sudden moment of inspiration, I did use the Uppaal model checker in a one-week intensive course on operating systems for engineering students, and the results were very encouraging.

Frits and his coauthor have done all of us a great service by making their material available on the web, and by sharing their experience with the rest of us. Let's expose our students to easy-to-use model checkers like Uppaal from the first year of the studies in CS and Engineering. This will also a increase the impact of research in formal methods. Several of the students taking my one-week course wrote in their course evaluation that they were glad to have been exposed to Uppaal, and that they think they will use the tool again in their future studies on, e.g., control systems. This indicates that, once students have seen how useful model checkers are, they will be enticed to use them later on when facing similar problems. Last, but not least, the mathematically inclined students may be motivated to carry out independent studies and (under)graduate research in formal methods and other areas of theoretical computer science.

Quoting from the concluding section of the paper:

“Why should algorithms be explained without the use of a model checker?”

Indeed, why not? It will be a good day for the construction of reliable software systems when our students will routinely simulate and analyze concurrent algorithms using model checkers. For the moment, let's share our teaching experiences following the example set by Frits and his coworker, and let's make model checking and logic permeate our undergraduate education as much as possible.