Formal Modeling and Verifications of Deadlock Prevention Solutions in Web Service Oriented System

Competitions of shared web resources have been widely concerned today. Under the circumstances of networks, especially in distributed systems, central supervisor can hardly be implemented, which makes it more complicated to prevent deadlock problems. This paper describes the competitions of web services for shared web resources using CSP method. Deadlocks can be analyzed based on the formal model by means of the trace semantics. The capability of deadlock prevention solutions which have been applied in industry can be proved theoretically under this approach. Moreover, the FDR which is a model checking tool for CSP can be used to automate the verifications.