| Formal verification technique for grid service chain model and its application |
| |
| 作者单位： | XU Ke（Automation Department, Tsinghua University, Beijing 100084, China） ;
WANG YueXuan（Automation Department, Tsinghua University, Beijing 100084, China） ;
WU Cheng（Automation Department, Tsinghua University, Beijing 100084, China） ; |
| |
| 摘 要： | Ensuring the correctness and reliability of large-scale resource sharing and complex job processing is an important task for grid applications. From a formal method perspective, a grid service chain model based on state Pi calculus is pro- posed in this work as the theoretical foundation for the service composition and collaboration in grid. Following the idea of the Web Service Resource Framework (WSRF), state Pi calculus enables the life-cycle management of system states by associating the actions in the original Pi calculus with system states. Moreover, model checking technique is exploited for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effective- ness of the proposed work.
|
| 收稿时间： | 12 October 2005 |
| 修稿时间： | 1 September 2006 |
Formal verification technique for grid service chain model and its application |
| |
| Authors: | Xu Ke Wang YueXuan Wu Cheng |
| |
| Affiliation: | Automation Department, Tsinghua University, Beijing 100084, China |
| |
| Abstract: | Ensuring the correctness and reliability of large-scale resource sharing and complex job processing is an important task for grid applications. From a formal method perspective, a grid service chain model based on state Pi calculus is pro- posed in this work as the theoretical foundation for the service composition and collaboration in grid. Following the idea of the Web Service Resource Framework (WSRF), state Pi calculus enables the life-cycle management of system states by associating the actions in the original Pi calculus with system states. Moreover, model checking technique is exploited for the design-time and run-time logical verification of grid service chain models. A grid application scenario of the dynamic analysis of material deformation structure is also provided to show the effective- ness of the proposed work. |
| |
| Keywords: | grid grid service chain formal method model checking state Pi calculus |
| 本文献已被 万方数据 SpringerLink 等数据库收录！ |
