Research On Co-Verification Oriented Towards Semantic Constraints

With the continuous development of grid technology and further research on grid application, the workflow process under the grid environment is getting more and more complex. The large-scale of the workflow process due to inter-organizational cooperation will result in highly complexity of the workflow model. The grid workflow verification is very difficult because of state space explosion. In order to solve this problem, the research on co-verification oriented towards semantic constraints has been studied. Co-verification method based on reduction is helpful to enhance efficiency. The following several aspects of the research work mainly have been done.(1) Research on the concept and model of co-verification. According to further study of the current situation in workflow verification, the limitation in structure verification has been break through, the theory of co-verification has been studied, the theoretical model has been given and the viewpoint that the co-verification has two-dimensional has been proposed.(2) Issues on the process of co-verification. There are no distributed properties on verification in the existing research, but co-verification is. Considering the relationship between sub-models, the cooperative approaches based on SCN have been given, the verification on synthesis model has been analyzed, and the reasonable of cross-validation process has been proved. The co-verification which has the advantage of dynamic has been illustrated through comparing cross-validation with "first sub-model, then the synthesis model" method.(3) Research on the reduction rules of co-verification. The principle in structure verification is no structure conflicts, but it does not apply to co-verification. The reduction rules in co-verification see the consistency in semantic constraints as principle, reducing the model when there are no semantic conflicts gradually. According to different network structure, a subnet level reduction rules has been put forward based on SCN and the liveness, effectiveness and completeness of these rules have been demonstrated. An instance of shopping online is given to illustrate the availability of the techniques described above.