Modeling an Operating System Kernel