The reliability of the design of a real-time system is important. For example, when there are errors in avionics control systems or nuclear reactor control systems, the loss of finance, time or even the loss of human lives could be enormous. Therefore when one designs a real-time system, methods to guarantee the correctness of the system are needed before the implementation of the system. We specify a scheduling algorithm of real-time systems called priority ceiling protocol using ACSR-VP and perform schedulability analysis on real-time systems by checking for a bisimulation relation.