Formal verification of mutex of concurrent system

The model of concurrent system is the research foundation of its performance evaluation, simulation, scheduling and control. Mutex is one of the most important features of concurrent. systems.This paper establishes a general mathematical model—Mutex-Model for exclusive systems. Decomposes the mutex property of concurrent system into safety, liveness and non-blocking and translates these features into LTL formulas formal specification. Gives a model checking algorithm based on fixed-point theory for Mutex-Model. And then combines with an example, the paper formally verifies the Mutex-Model Gives the explicit refinement and improvement of the model. As concurrent system´s processes increase, this model checking algorithm have to face state explosion problem. So the paper gives another symbolic model checking algorithm based on BDD and Boolean formulas. This algorithm is simple and efficient, and effectively alleviate the state explosion problem.