In my OS course (both as an undergrad and later as a teaching assistant) we used Xinu [1] which seemed to work well.

[1] http://en.wikipedia.org/wiki/Xinu