Using Pi-calculus To Formalize Grid Workflow And Verify Process Soundness

As rapid developing of grid technology, the application of it has grown boomly and expanded into more areas. Being with the ability to automate, manage, schedule and monitor complex grid applications, grid workflow is becoming one of the most important technology. Until now, most of researches on grid workflow focused on enable technology while the investigation on formalization and verification is at the infancy stage. Due to the multi-level abstract and complexity of grid workflow, it is very urgent and necessary to build a grid workflow model based on rigid formalizing semantics.Firstly, the article studies grid workflow characteristics and Pi calculus theory, then applies basic Pi calculus to formalize the grid workflow tasks, processes, specification and parallel computing patterns from different points. A closed formal grid workflow model is provided by the composition of a set of clear formal semantics. Moreover, the dissertation verifies procedure soundness based on the formal semantics of grid workflow with basic Pi calculus. With the analysis and application in different instances, It is shown that the solution can effectively and expediently locate some problems such as deadlock, redundancy etc. Compared with former research, the paper's work mainly includes: 1)Describing grid workflow's parallel computing patterns with basic Pi calculus; 2)Constructing a closed grid workflow formal model on which a semantic-based grid workflow system can be built; 3)Verifying the interaction soundness in grid workflow by expanding the model checking method used in business process management to the grid workflow field.Finally, the article verified typical grid workflow processes and the instances in grid workflow system developed by staff room. Results show that the method used by the article can effectively detect the deadlock during process.