Enforcing dependable operations by model checking a visualization layer

This paper describes the verification technique for enforcing and verifying correct operations of a virtualization software layer by applying model checking. Software model checking is a method of reading software programs, exploring all execution paths and checking whether developer-specified properties (conditions) are satisfied or not. Software model checking is first applied for enforcing the correct operations especially to ensure the isolation of the virtualization layer itself. It is also applied to a device driver so that the device handler of the virtualization layer enforces a guest OS operates in correct orders in order to avoid putting the device in error states. We are currently working on widening the areas where model checking can be applied in our virtualization software layer.