Simulation and verification of the virtual memory management system with MSVL

The paging mechanism is widely used in most modern systems to handle the virtual memory. Many page replacement algorithms have been proposed. Therefore, the cor-rectness and reliability of virtual memory management systems become very important. It is essential to formalize and verify the system in a formal way. In this paper, we model the virtual memory management system with MSVL, which is a parallel programming language used for the modeling, simulation and verification of software and hardware systems. Then we employ the model checking approach based on MSVL to verify the interval related properties and periodic repeated properties of the system.