In this paper, we gave a formal model of OS based on Petri Nets, it transformed the deadlock problem into linear algebric problem. We obtained a sufficient and necessary condition of deadlock existence in OS, and an optimal method which removed all deadlocks and guaranteed the regular operation in the system. Specialling, for distributed OS, we have greatly improved the method of detect deadlock.