The PTL description of processor state transformation in virtualization system

Virtualization has become a new computing mode, the validation of virtualization system is directly related to its application in cloud computing and system security. The validation method of virtualization system is evolved from the traditional operating system validation. Because the complex of system software validation and the particularity of virtualization system, there still exist problems including non-unified treatment methods, no perfect modeling and less universal validation methods. The processor state transformation in virtualization system is complex and requires system-level software to provide severe control sequence. PTL (projection temporal logic) is an effective tool to describe and validate a system which can provide reference for the design of the system software from formalization. This paper made detailed analysis of virtualized processor state transformation, then presented the corresponding proposition and formula based on PTL which made a formal description of the processor state transformation and can provide reference for the design of the virtualization system.