Verification of Virtual Machine Architecture in a Hypervisor through Model Checking

Abstract Hypervisors are used to virtualize the architecture on which it runs. These are small computer programs that are typically safety-critical, and also hard to debug. As the size of hypervisors are small that is why the formal verification at code level is feasible for these. In this paper, the authors present the formal verification of architecture of the virtual machines created by the hypervisors. Authors have verified the target by model checking with the help of mCRL2 tool. The verification is carried out on the design level. The formal verification of architecture of virtual machines along with its code written in the mCRL2 modelling language is presented.