×

zbMATH — the first resource for mathematics

Formal verification technique for grid service chain model and its application. (English) Zbl 1122.68082
Summary: 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 proposed in this work as the theoretical foundation for the service composition and collaboration in grid. Following the idea of the web service resource framework, 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 effectiveness of the proposed work.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68M10 Network design and communication in computer systems
68M14 Distributed systems
68U35 Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.)
Software:
JOpera; NuSMV
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Joseph J, Fellenstein C. Grid Computing. IBM Press, 2003. 3–25
[2] Bolognesi T. A conceptual framework for state-based and event-based formal behavioral specification languages. In: Pierfrancesco B, Shawn A B, Bernhard S, eds. Proc. 9th IEEE Int. Conf. on Engineering of Complex Computer Systems. CA: IEEE Press, 2004. 107–116
[3] Xu K, Wang Y X, Wu C. Ensuring secure and robust grid applications – from a formal method point of view. In: Chung Y C, Moreira J E, eds. Advances in Grid and Pervasive Computing. Lect Notes in Comput Sci, Vol 3947. Beilin: Springer-Verlag, 2006. 537–546
[4] Wang Y X, Wu C, Xu K. Study on Pi-calculus based equipment grid service chain model. In: Jin H, Reed D A, Jiang W, eds. Network and Parallel Computing. Lect Notes in Comput Sci, Vol 3779. Beilin: Springer-Verlag, 2005. 40–47
[5] Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge: MIT Press, 1999. 1–97
[6] Németh Z, Sunderam V. Characterizing grids attributes, definitions, and formalisms. J Grid Comput, 2003, 1(1): 9–23 · doi:10.1023/A:1024011025052
[7] Németh Z. Definition of a parallel execution model with abstract state machine. Acta Cybernet, 2002, 15(3): 417–455 · Zbl 1065.68054
[8] Sangiorgi D, Walker D. The Pi-calculus: a Theory of Mobile Processes. Cambridge: Cambridge University Press, 1999. 11–154
[9] Pahl C. A Pi-calculus based framework for the composition and replacement of components. In: Giannakopoulou D, Leavens G T, Sitaraman M, eds. Proc. Specification and Verification of Component-Based Systems. USA: ACM Press, 2001. 97–107
[10] Manuei M, Sergio G. A case study of web services orchestration. In: Jacquet J M, Picco G P, eds. Coordination Models and Languages. Lect Notes in Comput Sci, Vol 3454. Beilin: Springer-Verlag, 2005. 1–16
[11] Nierstrasz N, Meijler T D. Requirements for a composition language. In Ciancarini P, Nierstrasz O, Yonezawa A, eds. Object-Based Models and Languages for Concurrent Systems. Lect Notes in Comput Sci, Vol 924. Beilin: Springer-Verlag, 1995. 147–161
[12] Salaun G, Bordeaux L, Schaerf M. Describing and reasoning on web services using process algebra. In: Zhang L J, Jain H, Liu L, eds. Proc. IEEE Int. Conf. on Web Services. CA: IEEE Press, 2004. 43–50
[13] Deelman E, Blythe J, Gil Y, et al. Mapping abstract complex workflows onto grid environments. J Grid Comput, 2003, 1(1): 25–39 · doi:10.1023/A:1024000426962
[14] Fahringer T, Qin J, Hainzer S. Specification of grid workflow applications with AGWL: An abstract grid workflow language. In: Walker D W, Kesselman C, eds. Proc. IEEE Int. Symp. on Cluster Computing and the Grid. Vol. 2. UK: IEEE Press, 2005. 676–685
[15] Long Y, Lam H, Su Y W. Adaptive grid service flow management: Framework and model. In: Zhang L J, Jain H, Liu L, eds. Proc. IEEE Int. Conf. on Web Services. CA: IEEE Press, 2004. 558–565
[16] Pllana S, Fahringer T, Testori J, et al. Towards an UML based graphical representation of grid workflow applications. In: Dikaiakos M D, ed. Grid Computing. Lect Notes in Comput Sci, Vol 3165. Beilin: Springer-Verlag, 2004. 149–158
[17] Pautasso C, Alonso G. The JOpera visual composition language. J Visual Lang Comput, 2005, 16: 119–152 · Zbl 05696083 · doi:10.1016/j.jvlc.2004.08.004
[18] Amnuaykanjanasin P, Nupairoj N. The BPEL orchestrating framework for secured grid services. In: Selvaraj H, ed. Proc. Int. Conf. on Information Technology: Coding and Computing. CA: IEEE Press, 2005. 348–353
[19] Qing S H, Li G C. A formal model of fair exchange protocols. Sci China Ser F-Inf Sci, 2005, 48(4): 499–512 · Zbl 1187.94036 · doi:10.1360/122004-30
[20] Su K L, Lu G F, Chen Q L. Knowledge structure approach to verification of authentication protocols. Sci China Ser F-Inf Sci, 2005, 48(4): 513–532 · Zbl 1161.68323 · doi:10.1360/122004-78
[21] Németh Z, Pérez C, Priol T. Workflow enactment based on a chemical metaphor. In: Aichernig B K, Beckert B, eds. Proc. 3rd IEEE Int. Conf. on Software Engineering and Formal Methods. CA: IEEE Press, 2005. 127–136
[22] Chaki S, Clarke E M, Ouaknine J, et al. State / event-based software model checking. In Boiten E A, Derrick J, Smith G, eds. Integrated Formal Methods. Lect Notes in Comput Sci, Vol 2999. Beilin: Springer-Verlag, 2004. 128–147 · Zbl 1196.68129
[23] Giannakopoulou D, Magee J. Fluent model checking for event-based systems. In: Paakki J, ed. Proc. 11th ACM SIGSOFT Int. Symp. on Foundations of Software Engineering. NY: ACM Press, 2003. 257–266
[24] Taguchi K, Dong J S, Ciobanu G. Relating Pi calculus to Object-Z. In: Bellini P, Bohner S, Steffen B, ed. Proc. 9th IEEE Conference on Engineering Complex Computer Systems. CA: IEEE Press, 2004. 97–106
[25] Nicola R D, Vaandrager F. Three logics for branching bisimulation. JACM, 1995, 42(2): 458–487 · Zbl 0886.68064 · doi:10.1145/201019.201032
[26] Milner R. Communicating and Mobile Systems: the Pi-calculus. Cambridge: Cambridge University Press, 1999. 49–50 · Zbl 0942.68002
[27] Cinzia B, Alessandro F, Stefania G, et al. A formal verification environment for railway signaling system design. Form Method Syst Des, 1998, 12(2): 139–161 · doi:10.1023/A:1008645826258
[28] Cimatti A, Clarke E, Giunchiglia E, et al. NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma E, Larsen K G, eds. Computer Aided Veriifcation. Lect Notes in Comput Sci, Vol 2404. Beilin: Springer-Verlag, 2002. 359–364 · Zbl 1010.68766
[29] Heitmeyer C, Kirby J, Labaw B, et al. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE T Software Eng, 1998, 24(11): 927–948 · Zbl 05114716 · doi:10.1109/32.730543
[30] Xu K, Wang Y X, Wu C. Aspect oriented region analysis for efficient grid application reasoning. In: Xiao N, Rajkumar B, Liu Y H, eds. Proc. 5th Int. Conf. on Grid and Cooperative Computing. CA: IEEE Press, 2006. 28–31
[31] Dwyer M B, Avrunin G S, Corbett J C. Patterns in property specifications for finite-state verification. In: Boehm B, Garlan D, Kramer J, eds. Proc. 21th Int. Conf. on Software Engineering. CA: IEEE Press, 1999. 411–431
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.