Virtualization has become a key tool for optimizing resource use, and ARM virtualization extensions have made it easier for hypervisors to run on embedded systems. As a fundamental behavior of the system, interrupt handling is a critical component of operating systems, and the same holds true for interrupt virtualization in hypervisors. However, the implementation of interrupt virtualization can be complex, even with the hardware-assisted virtualization provided by the Generic Interrupt Controller (GIC). The behavior of the virtual GIC on a virtual machine could be inconsistent with that of the GIC in a non-virtualized environment, potentially leading to issues such as interrupt loss and priority inversion. As a key method for proving system correctness, formal modeling and verification are essential for proving the priority handling properties of interrupt virtualization. In this paper, we examine how interrupt injection is managed in existing open-source hypervisors on ARM platforms with GIC hardware-assisted virtualization extensions, focusing particularly on how hypervisors handle interrupt overflow during injection. Finally, we apply formal methods to describe the behavior of interrupt injection and verify that priority inversion can occur if the virtual interrupts in the list registers are not evicted according to their priority.