Abstract :
Grid service is composed of elementary services and the execution procedure is characterized by dynamical evolvement and exceptional no-determinism. The existing service description language, BPEL4WS (abbreviated to BPEL), only provides static service description, which cannot guarantee the correct composition of elementary services and dynamically monitor the occurrence of the exceptional events. According to the problems mentioned above, a verification approach to check the validity of the behavior partial order sequence of a grid service is proposed in this paper, which converts the grid service script based on BPEL into the behavior sequence described in Cpi-calculus automatically, and extracts the partial order constraint rules on the behavior of elementary services in a grid service, based on which to check the reachability of elementary services and validity of the behavior sequence during the execution of a grid service. A validity check algorithm is proposed finally.
Keywords :
formal verification; grid computing; pi calculus; BPEL4WS service description language; Cpi-calculus; grid service behavior partial order sequence; grid service composition validity checking; grid service verification; partial order constraint rules; Algebra; Automata; Computer science; Constraint optimization; Data mining; Grid computing; High performance computing; Monitoring; Petri nets; Tin;
