网格服务流的状态π演算形式化验证技术研究与应用
|
摘要
网格服务流是实现复杂网格应用中大规模异构资源协作与共享的重要手段。如何确保其设计和实现上的正确性是系统科学和计算机科学领域的前沿性研究方向,具有重要的理论意义和实用价值。本文通过提出一种称为状态π演算的状态/事件混合形式化工具,采用与模型验证(Model Checking)相结合的手段,系统研究了以状态π演算为基础的网格服务流形式化建模、验证及验证性能优化技术。部分研究成果已在LIGO数据网格项目和银行法律法规验证中得到应用。
结合网格中Web服务资源框架对有状态资源的管理特点,本文首先提出了一种状态π演算的新形式化工具并分析了其语义和性质,它实现了对系统状态的灵活抽象与管理,有效简化了网格服务流及其业务逻辑的建模和验证。基于状态π演算,本文实现了网格服务及其选择、BPEL4WS、DAGMan规范和网格服务流中并发与管道模式的形式化语义。这不仅为部分晦涩复杂的网格服务流规范提供了重要的形式化基础,也验证了状态π演算自身的表达能力。
在此形式化语义的基础上,本文从网格服务流的结构验证、规范语义约束验证、业务逻辑验证及其一致性检验的四个方面和静态/动态两个层面对其形式化验证技术进行了研究。通过提出状态π演算的强/弱状态断言和灵活复用模型验证的方法为以上问题提供了系统的解决方法。通过应用实例发现,该方法实现了对状态π演算的状态/事件混合推演和模型验证支持,且有减少重复验证和验证方法独立于特定模型验证技术的优点。
进一步,本文还从服务流验证分解和错误过程模式的两种思路,研究了对网格服务流形式化验证的性能改进。一方面,通过将网格服务流分解为一系列串行域和并发支,提出了基于模块化验证的验证分解策略;另一方面,通过分析网格服务流中可能存在的错误过程模式及其特点,提出了基于错误过程模式搜索向导的快速证伪方法。通过不同复杂度的LIGO引力波数据分析服务流实例和数值比较结果,验证了以上两方法在验证效率和内存占用上均有明显提高。
最后介绍了本文工作的系统化集成,即GridPiAnalyzer原型系统的模块和应用。它目前已提供了对Condor DAGMan、BPEL 1.1规范和IBM WBITM的支持。
Grid service flow is an important paradigm for realizing complex heterogeneous resource collaboration and sharing in various grid applications. Correctness verification in the design and implementation of grid service flows is an active research topic in the domain of system science and computer science which enjoys both great theoretical and practical values. Based on realistic applications like LIGO data grid, this dissertation has systematically investigated the formal modeling, verification and its performance issues for grid service flows by proposing a calculus called the stateπcalculus and the study of its formal verification support.
Following the new feature of stateful resource management introduced in the Web Service Resource Framework, first a new stateπcalculus is proposed to further strengthen its capability in managing the life-cycle of system states. The proposed calculus not only enables the flexible abstraction and management of historical system events, but also facilitates the modeling and verification of grid service flows. Moreover, based on the stateπcalculus, the formal semantics of grid service execution and selection, the specification of BPEL4WS, DAGMan and the parallel / pipeline patterns in grid service flows are also rigidly captured, which at the same time has verified the full expressiveness of our stateπcalculus.
Based on the formal semantics of grid service flows with stateπcalculus, the dissertation fully studies from both the static and dynamic aspects of its formal verification issues including its structural correctness, specification satisfiability, business logic satisfiability and consistency. Systematic solution is provided for the above issues by the proposal of strong/weak state assertion for our stateπcalculus with its model checking support. By the gravitational wave data analysis application from LIGO data grid, it is shown the proposed solution enjoys the advantages of: (1) supports the state / event hybrid analysis and model checking of stateπcalculus models; (2) reduce unnecessary verifications to save the verification cost; (3) be independent of specific model checking engine and thus enjoys a wider choice of new formal verification techniques.
Furthermore, the improvement of verification performance is also investigated by following the two ideas of grid service flow decomposition and process bug patterns respectively. On the one hand, by decomposing a grid service flow into a set of sequential standard regions with parallel branches, the corresponding verification strategy is also decomposed following the idea of modular verification. On the other hand, by identifying the potential process bug patterns in the structure of grid service flows, the idea of guided search is combined into the formal verification of grid service flow to efficiently falsify its correctness. With the performance evaluation on verifying multiple gravitational wave data analysis applications with different complexity from LIGO, it is illustrated that the proposed approaches can effectively reduce both the required CPU time and memory cost compared to using various traditional verification approaches alone.
Finally, the framework and application background of GridPiAnalyzer, an automatic tool support for the formal verification of grid service flows based on this dissertation, is introduced. It currently provides the support for Condor DAGMan, BPEL4WS 1.1 specification and IBM’s Websphere Business Integrator TM model.
结合网格中Web服务资源框架对有状态资源的管理特点,本文首先提出了一种状态π演算的新形式化工具并分析了其语义和性质,它实现了对系统状态的灵活抽象与管理,有效简化了网格服务流及其业务逻辑的建模和验证。基于状态π演算,本文实现了网格服务及其选择、BPEL4WS、DAGMan规范和网格服务流中并发与管道模式的形式化语义。这不仅为部分晦涩复杂的网格服务流规范提供了重要的形式化基础,也验证了状态π演算自身的表达能力。
在此形式化语义的基础上,本文从网格服务流的结构验证、规范语义约束验证、业务逻辑验证及其一致性检验的四个方面和静态/动态两个层面对其形式化验证技术进行了研究。通过提出状态π演算的强/弱状态断言和灵活复用模型验证的方法为以上问题提供了系统的解决方法。通过应用实例发现,该方法实现了对状态π演算的状态/事件混合推演和模型验证支持,且有减少重复验证和验证方法独立于特定模型验证技术的优点。
进一步,本文还从服务流验证分解和错误过程模式的两种思路,研究了对网格服务流形式化验证的性能改进。一方面,通过将网格服务流分解为一系列串行域和并发支,提出了基于模块化验证的验证分解策略;另一方面,通过分析网格服务流中可能存在的错误过程模式及其特点,提出了基于错误过程模式搜索向导的快速证伪方法。通过不同复杂度的LIGO引力波数据分析服务流实例和数值比较结果,验证了以上两方法在验证效率和内存占用上均有明显提高。
最后介绍了本文工作的系统化集成,即GridPiAnalyzer原型系统的模块和应用。它目前已提供了对Condor DAGMan、BPEL 1.1规范和IBM WBITM的支持。
Grid service flow is an important paradigm for realizing complex heterogeneous resource collaboration and sharing in various grid applications. Correctness verification in the design and implementation of grid service flows is an active research topic in the domain of system science and computer science which enjoys both great theoretical and practical values. Based on realistic applications like LIGO data grid, this dissertation has systematically investigated the formal modeling, verification and its performance issues for grid service flows by proposing a calculus called the stateπcalculus and the study of its formal verification support.
Following the new feature of stateful resource management introduced in the Web Service Resource Framework, first a new stateπcalculus is proposed to further strengthen its capability in managing the life-cycle of system states. The proposed calculus not only enables the flexible abstraction and management of historical system events, but also facilitates the modeling and verification of grid service flows. Moreover, based on the stateπcalculus, the formal semantics of grid service execution and selection, the specification of BPEL4WS, DAGMan and the parallel / pipeline patterns in grid service flows are also rigidly captured, which at the same time has verified the full expressiveness of our stateπcalculus.
Based on the formal semantics of grid service flows with stateπcalculus, the dissertation fully studies from both the static and dynamic aspects of its formal verification issues including its structural correctness, specification satisfiability, business logic satisfiability and consistency. Systematic solution is provided for the above issues by the proposal of strong/weak state assertion for our stateπcalculus with its model checking support. By the gravitational wave data analysis application from LIGO data grid, it is shown the proposed solution enjoys the advantages of: (1) supports the state / event hybrid analysis and model checking of stateπcalculus models; (2) reduce unnecessary verifications to save the verification cost; (3) be independent of specific model checking engine and thus enjoys a wider choice of new formal verification techniques.
Furthermore, the improvement of verification performance is also investigated by following the two ideas of grid service flow decomposition and process bug patterns respectively. On the one hand, by decomposing a grid service flow into a set of sequential standard regions with parallel branches, the corresponding verification strategy is also decomposed following the idea of modular verification. On the other hand, by identifying the potential process bug patterns in the structure of grid service flows, the idea of guided search is combined into the formal verification of grid service flow to efficiently falsify its correctness. With the performance evaluation on verifying multiple gravitational wave data analysis applications with different complexity from LIGO, it is illustrated that the proposed approaches can effectively reduce both the required CPU time and memory cost compared to using various traditional verification approaches alone.
Finally, the framework and application background of GridPiAnalyzer, an automatic tool support for the formal verification of grid service flows based on this dissertation, is introduced. It currently provides the support for Condor DAGMan, BPEL4WS 1.1 specification and IBM’s Websphere Business Integrator TM model.
引文
[1] Foster I, Kesselman C and Tuecke S. The anatomy of the grid: Enabling scalable virtual organizations. International Journal of High Performance Computing Applications, 2001, 15 (3): 200-222
[2] Foster I and Kesselman C. 网格计算 (金海, 袁平鹏, 等., 译者). 北京: 电子工业出版社, 2004. 1-54
[3] Stevens R, Woodward P, DeFanti T, et al. From the I-WAY to the national technology grid. Communications of the ACM, 1997, 40 (11): 50-60
[4] Catlett C E. TeraGrid: A foundation for US cyberinfrastructure. Network and Parallel Computing, LNCS, 2005, 3779: 1
[5] Coles J. The evolving grid deployment and operations model within EGEE, LCG and GridPP. in: H. Stockinger, R. Buyya, et al. (eds). Proceedings of the First International Conference on e-Science and Grid Computing. California: IEEE Computer Society, 2005. 90-97
[6] Miura K. Overview of Japanese science Grid project NAREGI. Progress in Informatics, 2006 (3): 67-75
[7] Jin H. ChinaGrid: Making grid computing a reality. Digital Libraries: International Collaboration and Cross-Fertilization, LNCS, 2004, 3334: 13-24
[8] Depei Q. CNGrid: A test-bed for grid technologies in China. in: B. Xu, U. Ramachandran, et al. (eds). 10th IEEE International Workshop on Future Trends of Distributed Computing Systems. New Zealand: IEEE Computer Society, 2004. 135-139
[9] 怀进鹏, 胡春明, 李建欣, 等. CROWN:面向服务的网格中间件系统与信任管理. 中国科学 E 辑, 2006, 36 (10): 1127-1155
[10] 徐志伟, 冯百明, 李伟. 网格计算技术. 北京: 电子工业出版社, 2004. 25-162
[11] Deak O. Grid service execution for JOpera: [Master Thesis]. Zurich: Swiss Federal Institue of Technology, 2005
[12] Czajkowski K, Ferguson D F, Foster I, et al. The WS-Resource Framework [EB/OL]. [2004-3-5]. http://www.globus.org/wsrf/specs/ws-wsrf.pdf
[13] Foster I, Frey J, Graham S, et al. Modeling stateful resources with Web services [EB/OL]. [2004-3-5]. http://www-128.ibm.com/developerworks/library/ws-resource/ws-modelingresources.pdf
[14] Wasson G, Humphrey M, Wasson G, et al. State and events for Web services:a comparison of five WS-resource framework and WS-Notification implementations. in: A. Grimshaw, M. Parashar, et al. (eds). 14th IEEE International Symposium on High Performance Distributed Computing. Research Triangle Park: IEEE Computer Society, 2005. 24-27
[15] Foster I. GT4 Primer [EB/OL]. [2005-5-8]. http://www.globus.org/toolkit/docs/4.0/key/
[16] Sotomayor B. The Globus Toolkit 4 Programmer's Tutorial [EB/OL]. [2005-11-26].http://gdp.globus.org/gt4-tutorial/
[17] Li M and Baker M. 网格计算核心技术 (王相林, 张善卿, 等., 译者). 北京: 清华大学出版社, 2006. 165-261
[18] Foster I, Czajkowski K, Ferguson D F, et al. Modeling and managing state in distributed systems: The role of OGSI and WSRF. Proceedings of the IEEE, 2005, 93 (3): 604-612
[19] Czajkowski K, Ferguson D, Foster I, et al. From Open Grid Services Infrastructure to WSResource Framework: Refactoring & Evolution [EB/OL]. [2004-3-5]. http://www.globus.org/wsrf/specs/ogsi_to_wsrf_1.0.pdf
[20] 吴澄, 李伯虎. 从计算机集成制造到现代集成制造--兼谈中国 CIMS 系统论的特点. 计算机集成制造--CIMS, 1998, 4 (5): 1-6
[21] 吴澄. 现代集成制造系统的理论基础--一类复杂性问题及其求解. 计算机集成制造--CIMS, 2001, 7 (3): 1-7
[22] Yu J and Buyya R. A taxonomy of workflow management systems for grid computing. (TR). Grid Computing and Distributed Systems Laboratory, University of Melbourne. Australia: March 10, 2005, p.1-31. 2005
[23] Cesare Pautasso G A. Parallel computing patterns for grid workflows. in: E. Deelman (eds). Workshop on Workflows in Support of Large-Scale Science. Paris: IEEE Computer Society, 2006.
[24] Fu X, Bultan T and Su J W. Realizability of conversation protocols with message contents. in: B. Werner (eds). IEEE International Conference on Web Services. California: IEEE Computer Society, 2004. 96-103
[25] 李景霞, 侯紫峰. Web 服务组合综述. 计算机应用研究, 2005, 22 (12): 4-7
[26] Antonioletti M. 'Workflow' issues in data access and integration: An OGSA-DAI/DAIS perspective. in: D. Berry and S. Parastatidis (eds). e-Science Workflow Services Workshops. Edinburgh: National e-Science Center, 2003.
[27] Brown. D A, Brady. P R, Alexander D, et al. A case study on the use of workflow technologies for scientific analysis: Gravitational wave data analysis. in: I. J. Taylor., D. Ewa, et al. (eds). Workflows for e-Science. Heidelberg: Springer-Verlag, 2006. 41-61
[28] Maglio P P, Srinivasan S, Kreulen J T, et al. Service systems, service scientists, SSME, and innovation. Communications of the ACM, 2006, 49 (7): 81-85
[29] Giblin C, Liu A Y, Muller S, et al. Regulations Expressed As Logical Models (REALM). in: M.-F. Moens and P. Spyns (eds). 18th Annual Conference on Legal Knowledge and Information Systems. Amsterdam: IOS Press, 2005. 37-48
[30] 中 国 人 民 银 行 . 金 融 机 构 反 洗 钱 规 定 [EB/OL]. [2003-1-3]. http://www.pbc.gov.cn/detail.asp?col=1510&ID=17
[31] BCBS. The Revised Basel Capital Framework (Basel II) [EB/OL]. [2004-6-26]. http://www.federalreserve.gov/boarddocs/press/bcreg/2004/20040626/attachment.pdf
[32] Statutory Instrument No. 3075. The Money Laundering Regulations 2003 [EB/OL]. [2003-11-28]. http://www.opsi.gov.uk/si/si2003/20033075.htm
[33] Electronic Privacy Information Center. USA Patriot Act of 2001, PL 107-56, HR 3162 RDS[EB/OL]. [2001-10-24]. http://www.epic.org/privacy/terrorism/hr3162.html
[34] (All first authors) Xu K, Samuel M and Liu Y. A Static Compliance Checking Framework for Business Process Models. IBM Systems Journal, 2007, 46 (2): 1-27
[35] Xu K, Wang Y X and Wu C. Formal verification technique for grid service chain model and its application. Science in China (Series F), 2006, 50 (1): 1-20
[36] Xu K, Liu L C and Wu C. A Three Layered Method for Business Process Discovery and its Application. Computers in Industry, 2007, 58(3): 265-278
[37] Xu K, Wang Y X and Wu C. Ensuring secure and robust grid applications - From a formal method point of view. Advances in Grid and Pervasive Computing, LNCS, 2006, 3947: 537-546
[38] Xu K, Wang Y X and Wu C. Aspect oriented region analysis for efficient equipment grid application reasoning. in: L. O'Conner (eds). 5th International Conference on Grid and Cooperative Computing. California: IEEE Computer Society, 2006. 28-31
[39] Wang Y X, Wu C and Xu K. Study on pi-calculus based equipment grid service chain model. Network and Parallel Computing, LNCS, 2005, 3779: 40-47
[40] Xu K, Liu Y and Wu C. Guided reasoning of complex E-business processes with business bug patterns. in: S. Kawada (eds). International Conference on E-Business Engineering. California: IEEE Computer Society, 2006. 195-202
[41] Xu K, Liu Y, Zhu J, et al. Pi Calculus based Bi-transformation of State-driven Model and Flow-driven Model. International Journal of Business Process Integration and Management, 2007, 1(4): 292-306
[42] Xu K, Wang Y X and Wu C. Service provenance based abstraction of grid application knowledge. in: L. O'Conner (eds). International Conference on Semantic and Knowledge Grid. California: IEEE Computer Society, 2006. 50-53
[43] Xu K, Liu Y and Wu C. BPSL Modeler - Visual notation language for intuitive business property reasoning. in: R. Bruni and D. Varro (eds). Electronic Notes in Theoretical Computer Science. Austria: Elsevier, 2006. 205-214
[44] 许可, 刘连臣, 吴澄. 时间π演算及其弱时间互模拟分析. 计算机集成制造系统, 2006, 12 (4): 511-516
[45] Abramovici A, Althouse W E, Drever R W P, et al. LIGO - The Laser Interferometer Gravitational-Wave Observatory. Science, 1992, 256 (5055): 325-333
[46] Barish B C and Weiss R. LIGO and the detection of gravitational waves. Physics Today, 1999, 52 (10): 44-50
[47] Blythe J, Deelman E and Gil Y. Automatically composed workflows for grid environments. IEEE Intelligent Systems, 2004, 19 (4): 16-23
[48] Deelman E, Blythe J, Gil Y, et al. Mapping abstract complex workflows onto grid environments. Journal of Grid Computing, 2003, 1 (1): 9-23
[49] Snyder K. deconstruction: LIGO analysis. Symmetry, 2005, 2 (9): 32-33
[50] Brown D A. Using the INSPIRAL program to search for gravitational waves from low-mass binary inspiral. Classical and Quantum Gravity, 2005, 22 (18): S1097-S1107
[51] 许可, 王跃宣, 吴澄. 网格服务链模型的验证分析技术及应用. 中国科学 F 辑, 2006: 已接收
[52] Li H C and Yang Y. Dynamic checking of temporal constraints for concurrent workflows. Electronic Commerce Research and Applications, 2005, 4 (2): 124-142
[53] Chen J J and Yang Y. Key Research Issues in Grid Workflow Verification and Validation. in: R. Buyya and T. Ma (eds). 4th Australasian Symposium on Grid Computing and e-Research. Australia: Australian Grid Forum, 2006.
[54] Chaki S, Clarke E M, Ouaknine J, et al. State/Event-Based software model checking. Integrated Formal Methods, LNCS, 2004, 2999: 128-147
[55] Hansen H, Virtanen H and Valmari A. Merging state-based and action-based verification. in: J. Lilius, F. Balarin, et al. (eds). 3rd International Conference on Application of Concurrency to System Design. Portugal: IEEE Computer Society, 2003. 150-156
[56] Chechik M and Paun D O. Events in property patterns Theoretical and Practical Aspects of SPIN Model Checking, LNCS, 1999, 1680: 154 - 167
[57] Clarke E M, Jr Grumberg O and Peled D A. Model Checking. Cambridge, Mass: MIT Press, 1999. 1-231
[58] Amin K, Von Laszewski G, Hategan M, et al. GridAnt: A client-controllable grid workflow system. in: R. H. Sprague (eds). 37th Annual Hawaii International Conference on System Sciences. Hawaii: IEEE Computer Society, 2004. 3293-3301
[59] Andrews T, Curbera F, Dholakia H, et al. Business Process Execution Language for Web Services Version 1.1 [EB/OL]. [2003-5-5]. http://www-128.ibm.com/developerworks/library/ specification/ws-bpel/
[60] Alexandre Alves, Arkin A, Askary S, et al. Web Services Business Process Execution Language Version 2.0 (Public Review Draft) [EB/OL]. [2006-8-23]. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-specification-draft.html
[61] Yu J and Buyya R. A novel architecture for realizing grid workflow using tuple spaces. in: B. Gropp, D. Reed, et al. (eds). 5th IEEE/ACM International Workshop on Grid Computing. Pittsburgh: IEEE Computer Society, 2004. 119-128
[62] Taylor I, Shields M, Wang I, et al. Visual grid workflow in Triana. Journal of Grid Computing, 2005, 3 (3-4): 153-169
[63] Pautasso C and Alonso G. The JOpera visual composition language. Journal of Visual Languages and Computing, 2005, 16 (1-2): 119-152
[64] Deelman E, Blythe J, Gil Y, et al. Pegasus and the pulsar search: From metadata to execution on the grid. Parallel Processing and Applied Mathematics, LNCS, 2004, 3019: 821-830
[65] Fahringer T, Jun Q and Hainzer S. Specification of Grid workflow applications with AGWL: An abstract Grid workflow language. in: D. W. Walker and C. Kesselman (eds). IEEE International Symposium on Cluster Computing and the Grid. Cardiff: Institute of Electrical and Electronics Engineers Computer Society, 2005. 676-685
[66] Hunt C S, Ferner C S and Brown J L. JXPL: An XML-based scripting language for workflow execution in a grid environment. in: Y. Levy (eds). IEEE SouthestCon. Ft. Lauderdale:Institute of Electrical and Electronics Engineers Inc, 2005. 345-350
[67] Krishnan S, Wagstrom P and Laszewski G v. GSFL: A workflow framework for Grid services [EB/OL]. [2002-7-19]. http://www-unix.globus.org/cog/papers/gsfl-paper.pdf
[68] Long Y, Lam H and Su S Y W. Adaptive grid service flow management: Framework and model. in: B. Werner (eds). IEEE International Conference on Web Services. California: IEEE Computer Society, 2004. 558-565
[69] Pllana S, Fahringer T, Testori J, et al. Towards an UML based graphical representation of grid workflow applications. Grid Computing, LNCS, 2004, 3165: 149-158
[70] Hoheisel A and Der U. An XML-based framework for loosely coupled applications on Grid environments. Computational Science, LNCS, 2003, 2657: 245-254
[71] Slomiski A. On using BPEL extensibility to implement OGSI and WSRF Grid workflows. Concurrency and Computation-Practice & Experience, 2006, 18 (10): 1229-1241
[72] Wang Y, Hu C and Huai J. A new grid workflow description language. in: C. K. Chang and L. J. Zhang (eds). IEEE International Conference on Services Computing. Orlando: IEEE Computer Society, 2005. 257-258
[73] Chao K-M, Younas M, Griffiths N, et al. Analysis of grid service composition with BPEL4WS. in: L. Barolli (eds). 18th International Conference on Advanced Information Networking and Applications. Washington: IEEE Computer Society, 2004.
[74] Vardi M Y. Branching vs. Linear time: Final showdown. Tools and Algorithms for the Construction and Analysis of Systems, LNCS, 2001, 2031: 1-22
[75] Alur R, Henzinger T A and Kupferman O. Alternating-time temporal logic. Compositionality: The Significant Difference, LNCS, 1997, 1536: 23-60
[76] Lamport L. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 1994, 16 (3): 872-923
[77] Hornos M J and Capel M I. On-the-fly model checking from interval logic specifications. ACM SIGPLAN Notices, 2002, 37 (12): 108 - 119
[78] Bimbo D, L R A and E V. Visual specification of branching time temporal logic. in: V. Harrslev (eds). 11th IEEE Symp. on Visual Languages. Darmstadt: IEEE Computer Society, 1995. 61-68
[79] Brambilla M, Deutsch A, Sui L, et al. The role of visual tools in a Web application design and verification framework: A visual notation for LTL formulae. Web Engineering, LNCS, 2005, 3579: 557-568
[80] Ferrari G L, Gnesi S, Montanari U, et al. A model-checking verification environment for mobile processes. ACM Transactions on Software Engineering and Methodology, 2003, 12 (4): 440-473
[81] Chen T, Han T and Lu J. A modal logic for Pi-calculus and model checking algorithm. Electronic Notes in Theoretical Computer Science, 2005, 123: 19-33
[82] Geist D. The PSL/Sugar specification language a language for all seasons. Journal on Data Semantics, LNCS, 2003, 2800: 3-3
[83] Clarke E M, McMillan K L, Campos S, et al. Symbolic model checking. Computer AidedVerification, LNCS, 1996, 1102: 419
[84] Clarke E, Biere A, Raimi R, et al. Bounded model checking using satisfiability solving. Formal Methods in System Design, 2001, 19 (1): 7-34
[85] Grumberg O and Long D E. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 1994, 16 (3): 843-871
[86] Yorav K and Grumberg O. Syntax-directed model checking of sequential programs. Journal of Logic and Algebraic Programming, 2002, 52-53: 129-162
[87] Jonsson B and Tsay Y-K. Assumption/Guarantee specifications in Linear-Time temporal logic. Theoretical Computer Science, 1996, 167: 47-72
[88] Loiseaux C, Graf S, Sifakis J, et al. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 1995, 6 (1): 11-44
[89] Bloem R, Ravi K and Somenzi F. Symbolic guided search for CTL model checking. in: IEEE (eds). 37th Design Automation Conference. Los Angeles: ACM, 2000. 29-34
[90] Peranandam P M, Weiss R J, Ruf J, et al. Dynamic guiding of bounded property checking. in: L. Fournier (eds). IEEE International High Level Design Validation and Test Workshop. Los Alamitos: IEEE Computer Society, 2004. 15-18
[91] Emerson E A and Halpern J Y. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 1986, 33 (1): 151-178
[92] Clarke E M and Draghicescu I A. Expressibility results for linear-time and branching-time logics. Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS, 1988, 354: 428-437
[93] Vardi M Y. Sometimes and not never re-revisited: on branching vs. linear time. Concurrency Theory, LNCS, 1998, 1466: 1-17
[94] Wang W L, Hidvegi Z, Bailey A D, et al. E-process design and assurance using model checking. Computer, 2000, 33 (10): 48-+
[95] Anderson B B, Hansen J V, Lowry P B, et al. Model checking for design and assurance of e-Business processes. Decision Support Systems, 2005, 39 (3): 333-344
[96] OASIS WSBPEL TC No. 42. Need for formalization [EB/OL]. [2003-7-31]. http://www.oasis-open.org/archives/wsbpel/200307/msg00177.html
[97] Baeten J C M. A brief history of process algebra. Theoretical Computer Science, 2005, 335 (2-3): 131-146
[98] Sangiorgi D and Walker D. The Pi-calculus : a theory of mobile processes. Cambridge: Cambridge University Press, 2001. 1-310
[99] Wombacher A, Fankhauser P and Neuhold E J. Transforming BPEL into annotated deterministic finite state automata for service discovery. in: B. Werner (eds). IEEE International Conference on Web Services. California: IEEE Computer Society, 2004. 316-323
[100] Fu X, Bultan T and Su J W. WSAT: A tool for formal analysis of web services. Computer Aided Verification, LNCS, 2004, 3114: 510-514
[101] Farahbod R, Glasser U and Vajihollahi M. Specification and validation of the business processexecution language for web services. Abstract State Machines: Advances in Theory and Practice, LNCS, 2004, 3052: 78-94
[102] Berardi D, De Rosa F, De Santis L, et al. Finite state automata as conceptual model for e-Services. Journal of Integrated Design and Process Science, 2004, 8 (2): 105-121
[103] Cimatti A, Clarke E, Giunchiglia E, et al. NuSMV2: an open source tool for symbolic model checking. Computer Aided Verification, LNCS, 2002, 2404: 359-364
[104] Ben-David S, Eisner C, Geist D, et al. Model checking at IBM. Formal Methods in System Design, 2003, 22 (2): 101-108
[105] Foster H, Uchitel S, Magee J, et al. LTSA-WS: a tool for model-based verification of web service compositions and choreography. in: L. J. Osterweil, H. D. Rombach, et al. (eds). 28th International Conference on Software Engineering. Shanghai: ACM, 2006. 771-774
[106] Tang Y, Chen L, He K-T, et al. SRN:an extended Petri-net-base workflow model for web service composition. in: B. Werner (eds). IEEE International Conference on Web Services. California: IEEE Computer Society, 2004. 591-599
[107] Yang Y, Tan Q, Xiao Y, et al. Exploiting hierarchical CP-Nets to increase the reliability of Web services workflow. in: (eds). International Symposium on Applications on Internet. California: IEEE Computer Society, 2006. 116 - 122
[108] Ouyang C, Verbeek E, van der Aalst W M P, et al. WofBPEL: A tool for automated analysis of BPEL processes. Service-Oriented Computing, LNCS, 2005, 3826: 484-489
[109] Lohmann N, Massuthe P, Stahl C, et al. Analyzing interacting BPEL processes. Business Process Management, LNCS, 2006, 4102: 17-32
[110] Puhlmann F and Weske M. Using the Pi-calculus for formalizing workflow patterns. Business Process Management, LNCS, 2005, 3649: 153-168
[111] Decker G, Puhlmann F and Weske M. Formalizing service interactions. Business Process Management, LNCS, 2006, 4102: 414-419
[112] Salaun G, Bordeaux L and Schaerf M. Describing and reasoning on Web services using process algebra. in: B. Werner (eds). IEEE International Conference on Web Services, 2004. 43-50
[113] Camara J, Canal C and Cubo J. Issues in the formalization of Web service orchestrations. in: S. Becker, C. Canal, et al. (eds). 2nd International Workshop on Coordination and Application Techniques for Software Entities. Scotland: Springer-Verlag, 2005. 17-24
[114] Liu F, Zhang L, Shi Y, et al. Formal analysis of compatibility of Web services via CCS. in: M. Paprzycki (eds). International Conference on Next Generation Web Services Practices. California: IEEE Computer Society, 2005. 143-148
[115] Yinxing W, Shensheng Z and Farong Z. On formalizing and verifying web services. High Technology Letters, 2005, 11 (1): 47-50
[116] Gao C, Liu R, Song Y, et al. A model checking tool embedded into services composition environment. in: L. O'Conner (eds). 5th International Conference on Grid and Cooperative Computing. California: IEEE Computer Society, 2006. 355-362
[117] 廖军, 谭浩, 刘锦德. 基于 Pi-演算的 Web 服务组合的描述和验证. 计算机学报, 2005, 28(4): 635-643
[118] Victor B and Moller F. The mobility workbench - A tool for the Pi-calculus. Computer Aided Verification, LNCS, 1994, 818: 428-440
[119] Zsolt N and Vaidy S. Characterizing grids: Attributes, definitions, and formalisms. Journal of Grid Computing, 2003, 1: 9-23
[120] Nemeth Z and Sunderam V. A formal framework for defining grid systems. in: IEEE (eds). 2nd IEEE/ACM International Symposium on Cluster Computing and the Grid, CCGRID2002. Berlin: IEEE Computer Society, 2002. 202-211
[121] 张鹏, 杜玉越, 左风朝. 网格体系的 Petri 网模拟与分析. 系统仿真学报, 2005, 17 (z1): 223-228
[122] Nemeth Z, Perez C and Priol T. Workflow enactment based on a chemical metaphor. in: B. K. Aichernig and B. Beckert (eds). 3rd IEEE International Conference on Software Engineering and Formal Methods. California: IEEE Computer Society, 2005. 127-136
[123] Groth P and Moreau M L L. Formalising a protocol for recording provenance in Grids. in: S. Cox (eds). UK OST e-Science second All Hands Meeting. Nottingham: EPSRC, 2004. 147-154
[124] 卢暾, 张望, 李志蜀, 等. 基于 I/O 自动机的网格服务组合的形式化. 华南理工大学学报(自然科学版), 2005, 33 (11): 55-60
[125] van der Aalst W M P. Pi Calculus versus Petri Nets: Let us eat humble Pie rather than further inflate the Pi hype. BPTrends, 2005, 3 (5): 1-11
[126] Smith H. Business process management—the third wave: business process modeling language (bpml) and its pi-calculus foundations. Information and Software Technology, 2003, 45: 1065-1069
[127] Lumpe M, Achermann F and Nierstrasz O. Foundations of component based systems. Cambridge: Cambridge University Press, 2000. 69-90
[128] Nierstrasz O and Meijler T D. Requirements for a composition language. Object-Based Models and Languages for Concurrent Systems, LNCS, 1995, 924: 147-161
[129] Pahl C. A formal composition and interaction model for a Web component platform. Electronic Notes in Theoretical Computer Science, 2002, 66 (4): 1-15
[130] Lumpe M. A Pi-calculus based approach for software composition. Switzerland: Institute of Computer Science and Applied Mathematics, University of Bern, 1999
[131] Vitus S W L and Julian P. Analyzing equivalences of UML statechart diagrams by structural congruence and open bisimulations. in: J. Hosking and P. Cox (eds). IEEE Symposium on Human Centric Computing Languages and Environments. New Zealand: IEEE Computer Society, 2003. 137-144
[132] Yang D and Zhang S S. Using pi-calculus to formalize UML activity diagram for business process modeling. in: P. Alexander (eds). 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems. California: IEEE Computer Society, 2003. 47-54
[133] Puhlmann F and Weske M. Investigations on soundness regarding lazy activities. BusinessProcess Management, LNCS, 2006, 4102: 145-160
[134] Gorla D. On the relative expressive power of calculi for mobility. Technical Report in Dip. di Informatica, Univ. di Roma "La Sapienza", 2006: 1-31
[135] Dam M. Model checking mobile processes. Information and Computation, 1996, 129 (1): 35-51
[136] Bouali A, Gnesi S and Larosa S. JACK: Just another concurrency kit: The integration project. Bulletin of the European Association for Theoretical Computer Science, 1994, 54: 207-224
[137] Foster I. Globus toolkit version 4: Software for service-oriented systems. Network and Parallel Computing, LNCS, 2006, 3779: 2-13
[138] 郭小群, 郝克刚. Web 服务的 Pi 演算描述. 计算机科学, 2006, 33 (3): 261-262
[139] Bolognesi T. A conceptual framework for state-based and event-based formal behavioural specification languages. in: B. Steffen, P. Bellini, et al. (eds). 9th International Conference on Engineering of Complex Computer Systems. Florence: IEEE Computer Society, 2004. 107-116
[140] Abadi M and Lamport L. Composing specifications. ACM Transactions on Programming Languages and Systems, 1993, 15 (1): 73-132
[141] Nicola R D and Vaandrager F. Three logics for branching bisimulation. Journal of the ACM, 1995, 42 (2): 458-487
[142] Giannakopoulou D and Magee J. Fluent model checking for event-based systems. in: L. Barroca (eds). 11th ACM SIGSOFT Symposium on Foundations of Software Engineering. Helsinki: ACM, 2003. 257-266
[143] Taguchi K, Dong J S and Ciobanu G. Relating pi-calculus to Object-Z. in: B. Steffen, P. Bellini, et al. (eds). 9th International Conference on Engineering of Complex Computer Systems. Florence: IEEE Computer Society, 2004. 97-106
[144] Milner R. Communicating and Mobile Systems: the Pi Calculus. Cambridge: Cambridge University Press, 1999. 16-97
[145] Kacsuk P, Dozsa G, Kovacs J, et al. P-GRADE: A grid programming environment. Journal of Grid Computing, 2003, 1 (2): 171-197
[146] 穆黎森. CGSP 网格中工作流系统的研究:复合资源管理: [硕士论文]. 北京: 清华大学, 2006
[147] Montanari U and Pistore M. Checking bisimilarity for finitary Pi-calculus. Concurrency Theory, LNCS, 1995, 962: 42-56
[148] Chen J and Yang Y. An activity completion duration based checkpoint selection strategy for dynamic verification of fixed-time constraints in grid workflow systems. Lecture Notes in Informatics, 2005, 69: 296-310
[149] Chen J and Yang Y. Temporal dependency for dynamic verification of fixed-date constraints in grid workflow systems. Web Technologies Research and Development, LNCS, 2005, 3399: 820-831
[150] Ioannidis Y E and Sellis T K. Supporting inconsistent rules in database systems. Journal of Intelligent Information Systems, 1992, 1 (3-4): 243-270
[151] Quinlan J R. Induction of decision trees. Machine Learning, 1986, 1: 81-106
[152] Chomicki J, Lobo J and Naqvi S. Conflict resolution using logic programming. IEEE Transactions on Knowledge and Data Engineering, 2003, 15 (1): 244-249
[153] Lindgren T. Methods for rule conflict resolution. Machine Learning, LNCS, 2004, 3201: 262-273
[154] Giannakopoulou D and Lerda F. From states to transitions: Improving translation of LTL formulae to Buchi automata. Formal Techniques for Networked and Distributed Sytems, LNCS, 2002, 2529: 308-326
[155] Ho Y-C and Pepyne D L. Simple explanation of the No Free Lunch Theorem of Optimization. in: M. Dymkov, I. Gaishun, et al. (eds). EEE Conference on Decision and Control. Orlando: Institute of Electrical and Electronics Engineers Inc., 2001. 4409-4414
[156] Liu R and Kumar A. An analysis and taxonomy of unstructured workflows. Business Process Management, LNCS, 2005, 3649: 268-284
[157] Vardi M Y. On the complexity of modular model checking. in: (eds). San Diego, CA, USA: IEEE, Piscataway, NJ, USA, 1995. 101-111
[158] 董威, 王戟, 齐治昌. UML 模型中并发对象的组合验证. 计算机科学, 2005, 32 (7): 231-234
[159] Een N and Sorensson N. An extensible SAT-solver. Theory and Applications of Satisfiability Testing, LNCS, 2003, 2919: 502-518
[160] Yang C H and Dill D L. Validation with guided search of the state space. in: IEEE (eds). 35th Design Automation Conference. San Francisco: ACM, 1998. 599-604
[161] Seppi K, Jones M and Lamborn P. Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae, 2006, 70 (1-2): 111-126
[162] Ravi K and Somenzi F. Hints to accelerate symbolic traversal. Correct Hardware Design and Verification Methods, LNCS, 1999, 1703: 250-264
[163] W.M.P. van der Aalst, A.H.M. ter Hofstede, B. Kiepuszewski, et al. Workflow patterns. Distributed and Parallel Databases, 2003, 14: 5-51
[164] Havey M. Essential Business Process Modeling. USA: O'Reilly, 2005. 1-332
[165] Hulse R A and Taylor J H. Discovery of a pulsar in a binary system. Journal of Astrophys, 1975, 195: L51
[166] Mantell K. From UML to BPEL. IBM DeveloperWorks, 2005: 1-10
[167] Heinis T, Pautasso C, Alonso G. Mirroring resources or mapping requests: implementing WS-RF for grid workflows. in: IEEE (eds). 6th IEEE International Symposium on Cluster Computing and the Grid (CCGRID'06). Florence: IEEE Computer Society, 2006. 497-504
[2] Foster I and Kesselman C. 网格计算 (金海, 袁平鹏, 等., 译者). 北京: 电子工业出版社, 2004. 1-54
[3] Stevens R, Woodward P, DeFanti T, et al. From the I-WAY to the national technology grid. Communications of the ACM, 1997, 40 (11): 50-60
[4] Catlett C E. TeraGrid: A foundation for US cyberinfrastructure. Network and Parallel Computing, LNCS, 2005, 3779: 1
[5] Coles J. The evolving grid deployment and operations model within EGEE, LCG and GridPP. in: H. Stockinger, R. Buyya, et al. (eds). Proceedings of the First International Conference on e-Science and Grid Computing. California: IEEE Computer Society, 2005. 90-97
[6] Miura K. Overview of Japanese science Grid project NAREGI. Progress in Informatics, 2006 (3): 67-75
[7] Jin H. ChinaGrid: Making grid computing a reality. Digital Libraries: International Collaboration and Cross-Fertilization, LNCS, 2004, 3334: 13-24
[8] Depei Q. CNGrid: A test-bed for grid technologies in China. in: B. Xu, U. Ramachandran, et al. (eds). 10th IEEE International Workshop on Future Trends of Distributed Computing Systems. New Zealand: IEEE Computer Society, 2004. 135-139
[9] 怀进鹏, 胡春明, 李建欣, 等. CROWN:面向服务的网格中间件系统与信任管理. 中国科学 E 辑, 2006, 36 (10): 1127-1155
[10] 徐志伟, 冯百明, 李伟. 网格计算技术. 北京: 电子工业出版社, 2004. 25-162
[11] Deak O. Grid service execution for JOpera: [Master Thesis]. Zurich: Swiss Federal Institue of Technology, 2005
[12] Czajkowski K, Ferguson D F, Foster I, et al. The WS-Resource Framework [EB/OL]. [2004-3-5]. http://www.globus.org/wsrf/specs/ws-wsrf.pdf
[13] Foster I, Frey J, Graham S, et al. Modeling stateful resources with Web services [EB/OL]. [2004-3-5]. http://www-128.ibm.com/developerworks/library/ws-resource/ws-modelingresources.pdf
[14] Wasson G, Humphrey M, Wasson G, et al. State and events for Web services:a comparison of five WS-resource framework and WS-Notification implementations. in: A. Grimshaw, M. Parashar, et al. (eds). 14th IEEE International Symposium on High Performance Distributed Computing. Research Triangle Park: IEEE Computer Society, 2005. 24-27
[15] Foster I. GT4 Primer [EB/OL]. [2005-5-8]. http://www.globus.org/toolkit/docs/4.0/key/
[16] Sotomayor B. The Globus Toolkit 4 Programmer's Tutorial [EB/OL]. [2005-11-26].http://gdp.globus.org/gt4-tutorial/
[17] Li M and Baker M. 网格计算核心技术 (王相林, 张善卿, 等., 译者). 北京: 清华大学出版社, 2006. 165-261
[18] Foster I, Czajkowski K, Ferguson D F, et al. Modeling and managing state in distributed systems: The role of OGSI and WSRF. Proceedings of the IEEE, 2005, 93 (3): 604-612
[19] Czajkowski K, Ferguson D, Foster I, et al. From Open Grid Services Infrastructure to WSResource Framework: Refactoring & Evolution [EB/OL]. [2004-3-5]. http://www.globus.org/wsrf/specs/ogsi_to_wsrf_1.0.pdf
[20] 吴澄, 李伯虎. 从计算机集成制造到现代集成制造--兼谈中国 CIMS 系统论的特点. 计算机集成制造--CIMS, 1998, 4 (5): 1-6
[21] 吴澄. 现代集成制造系统的理论基础--一类复杂性问题及其求解. 计算机集成制造--CIMS, 2001, 7 (3): 1-7
[22] Yu J and Buyya R. A taxonomy of workflow management systems for grid computing. (TR). Grid Computing and Distributed Systems Laboratory, University of Melbourne. Australia: March 10, 2005, p.1-31. 2005
[23] Cesare Pautasso G A. Parallel computing patterns for grid workflows. in: E. Deelman (eds). Workshop on Workflows in Support of Large-Scale Science. Paris: IEEE Computer Society, 2006.
[24] Fu X, Bultan T and Su J W. Realizability of conversation protocols with message contents. in: B. Werner (eds). IEEE International Conference on Web Services. California: IEEE Computer Society, 2004. 96-103
[25] 李景霞, 侯紫峰. Web 服务组合综述. 计算机应用研究, 2005, 22 (12): 4-7
[26] Antonioletti M. 'Workflow' issues in data access and integration: An OGSA-DAI/DAIS perspective. in: D. Berry and S. Parastatidis (eds). e-Science Workflow Services Workshops. Edinburgh: National e-Science Center, 2003.
[27] Brown. D A, Brady. P R, Alexander D, et al. A case study on the use of workflow technologies for scientific analysis: Gravitational wave data analysis. in: I. J. Taylor., D. Ewa, et al. (eds). Workflows for e-Science. Heidelberg: Springer-Verlag, 2006. 41-61
[28] Maglio P P, Srinivasan S, Kreulen J T, et al. Service systems, service scientists, SSME, and innovation. Communications of the ACM, 2006, 49 (7): 81-85
[29] Giblin C, Liu A Y, Muller S, et al. Regulations Expressed As Logical Models (REALM). in: M.-F. Moens and P. Spyns (eds). 18th Annual Conference on Legal Knowledge and Information Systems. Amsterdam: IOS Press, 2005. 37-48
[30] 中 国 人 民 银 行 . 金 融 机 构 反 洗 钱 规 定 [EB/OL]. [2003-1-3]. http://www.pbc.gov.cn/detail.asp?col=1510&ID=17
[31] BCBS. The Revised Basel Capital Framework (Basel II) [EB/OL]. [2004-6-26]. http://www.federalreserve.gov/boarddocs/press/bcreg/2004/20040626/attachment.pdf
[32] Statutory Instrument No. 3075. The Money Laundering Regulations 2003 [EB/OL]. [2003-11-28]. http://www.opsi.gov.uk/si/si2003/20033075.htm
[33] Electronic Privacy Information Center. USA Patriot Act of 2001, PL 107-56, HR 3162 RDS[EB/OL]. [2001-10-24]. http://www.epic.org/privacy/terrorism/hr3162.html
[34] (All first authors) Xu K, Samuel M and Liu Y. A Static Compliance Checking Framework for Business Process Models. IBM Systems Journal, 2007, 46 (2): 1-27
[35] Xu K, Wang Y X and Wu C. Formal verification technique for grid service chain model and its application. Science in China (Series F), 2006, 50 (1): 1-20
[36] Xu K, Liu L C and Wu C. A Three Layered Method for Business Process Discovery and its Application. Computers in Industry, 2007, 58(3): 265-278
[37] Xu K, Wang Y X and Wu C. Ensuring secure and robust grid applications - From a formal method point of view. Advances in Grid and Pervasive Computing, LNCS, 2006, 3947: 537-546
[38] Xu K, Wang Y X and Wu C. Aspect oriented region analysis for efficient equipment grid application reasoning. in: L. O'Conner (eds). 5th International Conference on Grid and Cooperative Computing. California: IEEE Computer Society, 2006. 28-31
[39] Wang Y X, Wu C and Xu K. Study on pi-calculus based equipment grid service chain model. Network and Parallel Computing, LNCS, 2005, 3779: 40-47
[40] Xu K, Liu Y and Wu C. Guided reasoning of complex E-business processes with business bug patterns. in: S. Kawada (eds). International Conference on E-Business Engineering. California: IEEE Computer Society, 2006. 195-202
[41] Xu K, Liu Y, Zhu J, et al. Pi Calculus based Bi-transformation of State-driven Model and Flow-driven Model. International Journal of Business Process Integration and Management, 2007, 1(4): 292-306
[42] Xu K, Wang Y X and Wu C. Service provenance based abstraction of grid application knowledge. in: L. O'Conner (eds). International Conference on Semantic and Knowledge Grid. California: IEEE Computer Society, 2006. 50-53
[43] Xu K, Liu Y and Wu C. BPSL Modeler - Visual notation language for intuitive business property reasoning. in: R. Bruni and D. Varro (eds). Electronic Notes in Theoretical Computer Science. Austria: Elsevier, 2006. 205-214
[44] 许可, 刘连臣, 吴澄. 时间π演算及其弱时间互模拟分析. 计算机集成制造系统, 2006, 12 (4): 511-516
[45] Abramovici A, Althouse W E, Drever R W P, et al. LIGO - The Laser Interferometer Gravitational-Wave Observatory. Science, 1992, 256 (5055): 325-333
[46] Barish B C and Weiss R. LIGO and the detection of gravitational waves. Physics Today, 1999, 52 (10): 44-50
[47] Blythe J, Deelman E and Gil Y. Automatically composed workflows for grid environments. IEEE Intelligent Systems, 2004, 19 (4): 16-23
[48] Deelman E, Blythe J, Gil Y, et al. Mapping abstract complex workflows onto grid environments. Journal of Grid Computing, 2003, 1 (1): 9-23
[49] Snyder K. deconstruction: LIGO analysis. Symmetry, 2005, 2 (9): 32-33
[50] Brown D A. Using the INSPIRAL program to search for gravitational waves from low-mass binary inspiral. Classical and Quantum Gravity, 2005, 22 (18): S1097-S1107
[51] 许可, 王跃宣, 吴澄. 网格服务链模型的验证分析技术及应用. 中国科学 F 辑, 2006: 已接收
[52] Li H C and Yang Y. Dynamic checking of temporal constraints for concurrent workflows. Electronic Commerce Research and Applications, 2005, 4 (2): 124-142
[53] Chen J J and Yang Y. Key Research Issues in Grid Workflow Verification and Validation. in: R. Buyya and T. Ma (eds). 4th Australasian Symposium on Grid Computing and e-Research. Australia: Australian Grid Forum, 2006.
[54] Chaki S, Clarke E M, Ouaknine J, et al. State/Event-Based software model checking. Integrated Formal Methods, LNCS, 2004, 2999: 128-147
[55] Hansen H, Virtanen H and Valmari A. Merging state-based and action-based verification. in: J. Lilius, F. Balarin, et al. (eds). 3rd International Conference on Application of Concurrency to System Design. Portugal: IEEE Computer Society, 2003. 150-156
[56] Chechik M and Paun D O. Events in property patterns Theoretical and Practical Aspects of SPIN Model Checking, LNCS, 1999, 1680: 154 - 167
[57] Clarke E M, Jr Grumberg O and Peled D A. Model Checking. Cambridge, Mass: MIT Press, 1999. 1-231
[58] Amin K, Von Laszewski G, Hategan M, et al. GridAnt: A client-controllable grid workflow system. in: R. H. Sprague (eds). 37th Annual Hawaii International Conference on System Sciences. Hawaii: IEEE Computer Society, 2004. 3293-3301
[59] Andrews T, Curbera F, Dholakia H, et al. Business Process Execution Language for Web Services Version 1.1 [EB/OL]. [2003-5-5]. http://www-128.ibm.com/developerworks/library/ specification/ws-bpel/
[60] Alexandre Alves, Arkin A, Askary S, et al. Web Services Business Process Execution Language Version 2.0 (Public Review Draft) [EB/OL]. [2006-8-23]. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-specification-draft.html
[61] Yu J and Buyya R. A novel architecture for realizing grid workflow using tuple spaces. in: B. Gropp, D. Reed, et al. (eds). 5th IEEE/ACM International Workshop on Grid Computing. Pittsburgh: IEEE Computer Society, 2004. 119-128
[62] Taylor I, Shields M, Wang I, et al. Visual grid workflow in Triana. Journal of Grid Computing, 2005, 3 (3-4): 153-169
[63] Pautasso C and Alonso G. The JOpera visual composition language. Journal of Visual Languages and Computing, 2005, 16 (1-2): 119-152
[64] Deelman E, Blythe J, Gil Y, et al. Pegasus and the pulsar search: From metadata to execution on the grid. Parallel Processing and Applied Mathematics, LNCS, 2004, 3019: 821-830
[65] Fahringer T, Jun Q and Hainzer S. Specification of Grid workflow applications with AGWL: An abstract Grid workflow language. in: D. W. Walker and C. Kesselman (eds). IEEE International Symposium on Cluster Computing and the Grid. Cardiff: Institute of Electrical and Electronics Engineers Computer Society, 2005. 676-685
[66] Hunt C S, Ferner C S and Brown J L. JXPL: An XML-based scripting language for workflow execution in a grid environment. in: Y. Levy (eds). IEEE SouthestCon. Ft. Lauderdale:Institute of Electrical and Electronics Engineers Inc, 2005. 345-350
[67] Krishnan S, Wagstrom P and Laszewski G v. GSFL: A workflow framework for Grid services [EB/OL]. [2002-7-19]. http://www-unix.globus.org/cog/papers/gsfl-paper.pdf
[68] Long Y, Lam H and Su S Y W. Adaptive grid service flow management: Framework and model. in: B. Werner (eds). IEEE International Conference on Web Services. California: IEEE Computer Society, 2004. 558-565
[69] Pllana S, Fahringer T, Testori J, et al. Towards an UML based graphical representation of grid workflow applications. Grid Computing, LNCS, 2004, 3165: 149-158
[70] Hoheisel A and Der U. An XML-based framework for loosely coupled applications on Grid environments. Computational Science, LNCS, 2003, 2657: 245-254
[71] Slomiski A. On using BPEL extensibility to implement OGSI and WSRF Grid workflows. Concurrency and Computation-Practice & Experience, 2006, 18 (10): 1229-1241
[72] Wang Y, Hu C and Huai J. A new grid workflow description language. in: C. K. Chang and L. J. Zhang (eds). IEEE International Conference on Services Computing. Orlando: IEEE Computer Society, 2005. 257-258
[73] Chao K-M, Younas M, Griffiths N, et al. Analysis of grid service composition with BPEL4WS. in: L. Barolli (eds). 18th International Conference on Advanced Information Networking and Applications. Washington: IEEE Computer Society, 2004.
[74] Vardi M Y. Branching vs. Linear time: Final showdown. Tools and Algorithms for the Construction and Analysis of Systems, LNCS, 2001, 2031: 1-22
[75] Alur R, Henzinger T A and Kupferman O. Alternating-time temporal logic. Compositionality: The Significant Difference, LNCS, 1997, 1536: 23-60
[76] Lamport L. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 1994, 16 (3): 872-923
[77] Hornos M J and Capel M I. On-the-fly model checking from interval logic specifications. ACM SIGPLAN Notices, 2002, 37 (12): 108 - 119
[78] Bimbo D, L R A and E V. Visual specification of branching time temporal logic. in: V. Harrslev (eds). 11th IEEE Symp. on Visual Languages. Darmstadt: IEEE Computer Society, 1995. 61-68
[79] Brambilla M, Deutsch A, Sui L, et al. The role of visual tools in a Web application design and verification framework: A visual notation for LTL formulae. Web Engineering, LNCS, 2005, 3579: 557-568
[80] Ferrari G L, Gnesi S, Montanari U, et al. A model-checking verification environment for mobile processes. ACM Transactions on Software Engineering and Methodology, 2003, 12 (4): 440-473
[81] Chen T, Han T and Lu J. A modal logic for Pi-calculus and model checking algorithm. Electronic Notes in Theoretical Computer Science, 2005, 123: 19-33
[82] Geist D. The PSL/Sugar specification language a language for all seasons. Journal on Data Semantics, LNCS, 2003, 2800: 3-3
[83] Clarke E M, McMillan K L, Campos S, et al. Symbolic model checking. Computer AidedVerification, LNCS, 1996, 1102: 419
[84] Clarke E, Biere A, Raimi R, et al. Bounded model checking using satisfiability solving. Formal Methods in System Design, 2001, 19 (1): 7-34
[85] Grumberg O and Long D E. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 1994, 16 (3): 843-871
[86] Yorav K and Grumberg O. Syntax-directed model checking of sequential programs. Journal of Logic and Algebraic Programming, 2002, 52-53: 129-162
[87] Jonsson B and Tsay Y-K. Assumption/Guarantee specifications in Linear-Time temporal logic. Theoretical Computer Science, 1996, 167: 47-72
[88] Loiseaux C, Graf S, Sifakis J, et al. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 1995, 6 (1): 11-44
[89] Bloem R, Ravi K and Somenzi F. Symbolic guided search for CTL model checking. in: IEEE (eds). 37th Design Automation Conference. Los Angeles: ACM, 2000. 29-34
[90] Peranandam P M, Weiss R J, Ruf J, et al. Dynamic guiding of bounded property checking. in: L. Fournier (eds). IEEE International High Level Design Validation and Test Workshop. Los Alamitos: IEEE Computer Society, 2004. 15-18
[91] Emerson E A and Halpern J Y. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 1986, 33 (1): 151-178
[92] Clarke E M and Draghicescu I A. Expressibility results for linear-time and branching-time logics. Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS, 1988, 354: 428-437
[93] Vardi M Y. Sometimes and not never re-revisited: on branching vs. linear time. Concurrency Theory, LNCS, 1998, 1466: 1-17
[94] Wang W L, Hidvegi Z, Bailey A D, et al. E-process design and assurance using model checking. Computer, 2000, 33 (10): 48-+
[95] Anderson B B, Hansen J V, Lowry P B, et al. Model checking for design and assurance of e-Business processes. Decision Support Systems, 2005, 39 (3): 333-344
[96] OASIS WSBPEL TC No. 42. Need for formalization [EB/OL]. [2003-7-31]. http://www.oasis-open.org/archives/wsbpel/200307/msg00177.html
[97] Baeten J C M. A brief history of process algebra. Theoretical Computer Science, 2005, 335 (2-3): 131-146
[98] Sangiorgi D and Walker D. The Pi-calculus : a theory of mobile processes. Cambridge: Cambridge University Press, 2001. 1-310
[99] Wombacher A, Fankhauser P and Neuhold E J. Transforming BPEL into annotated deterministic finite state automata for service discovery. in: B. Werner (eds). IEEE International Conference on Web Services. California: IEEE Computer Society, 2004. 316-323
[100] Fu X, Bultan T and Su J W. WSAT: A tool for formal analysis of web services. Computer Aided Verification, LNCS, 2004, 3114: 510-514
[101] Farahbod R, Glasser U and Vajihollahi M. Specification and validation of the business processexecution language for web services. Abstract State Machines: Advances in Theory and Practice, LNCS, 2004, 3052: 78-94
[102] Berardi D, De Rosa F, De Santis L, et al. Finite state automata as conceptual model for e-Services. Journal of Integrated Design and Process Science, 2004, 8 (2): 105-121
[103] Cimatti A, Clarke E, Giunchiglia E, et al. NuSMV2: an open source tool for symbolic model checking. Computer Aided Verification, LNCS, 2002, 2404: 359-364
[104] Ben-David S, Eisner C, Geist D, et al. Model checking at IBM. Formal Methods in System Design, 2003, 22 (2): 101-108
[105] Foster H, Uchitel S, Magee J, et al. LTSA-WS: a tool for model-based verification of web service compositions and choreography. in: L. J. Osterweil, H. D. Rombach, et al. (eds). 28th International Conference on Software Engineering. Shanghai: ACM, 2006. 771-774
[106] Tang Y, Chen L, He K-T, et al. SRN:an extended Petri-net-base workflow model for web service composition. in: B. Werner (eds). IEEE International Conference on Web Services. California: IEEE Computer Society, 2004. 591-599
[107] Yang Y, Tan Q, Xiao Y, et al. Exploiting hierarchical CP-Nets to increase the reliability of Web services workflow. in: (eds). International Symposium on Applications on Internet. California: IEEE Computer Society, 2006. 116 - 122
[108] Ouyang C, Verbeek E, van der Aalst W M P, et al. WofBPEL: A tool for automated analysis of BPEL processes. Service-Oriented Computing, LNCS, 2005, 3826: 484-489
[109] Lohmann N, Massuthe P, Stahl C, et al. Analyzing interacting BPEL processes. Business Process Management, LNCS, 2006, 4102: 17-32
[110] Puhlmann F and Weske M. Using the Pi-calculus for formalizing workflow patterns. Business Process Management, LNCS, 2005, 3649: 153-168
[111] Decker G, Puhlmann F and Weske M. Formalizing service interactions. Business Process Management, LNCS, 2006, 4102: 414-419
[112] Salaun G, Bordeaux L and Schaerf M. Describing and reasoning on Web services using process algebra. in: B. Werner (eds). IEEE International Conference on Web Services, 2004. 43-50
[113] Camara J, Canal C and Cubo J. Issues in the formalization of Web service orchestrations. in: S. Becker, C. Canal, et al. (eds). 2nd International Workshop on Coordination and Application Techniques for Software Entities. Scotland: Springer-Verlag, 2005. 17-24
[114] Liu F, Zhang L, Shi Y, et al. Formal analysis of compatibility of Web services via CCS. in: M. Paprzycki (eds). International Conference on Next Generation Web Services Practices. California: IEEE Computer Society, 2005. 143-148
[115] Yinxing W, Shensheng Z and Farong Z. On formalizing and verifying web services. High Technology Letters, 2005, 11 (1): 47-50
[116] Gao C, Liu R, Song Y, et al. A model checking tool embedded into services composition environment. in: L. O'Conner (eds). 5th International Conference on Grid and Cooperative Computing. California: IEEE Computer Society, 2006. 355-362
[117] 廖军, 谭浩, 刘锦德. 基于 Pi-演算的 Web 服务组合的描述和验证. 计算机学报, 2005, 28(4): 635-643
[118] Victor B and Moller F. The mobility workbench - A tool for the Pi-calculus. Computer Aided Verification, LNCS, 1994, 818: 428-440
[119] Zsolt N and Vaidy S. Characterizing grids: Attributes, definitions, and formalisms. Journal of Grid Computing, 2003, 1: 9-23
[120] Nemeth Z and Sunderam V. A formal framework for defining grid systems. in: IEEE (eds). 2nd IEEE/ACM International Symposium on Cluster Computing and the Grid, CCGRID2002. Berlin: IEEE Computer Society, 2002. 202-211
[121] 张鹏, 杜玉越, 左风朝. 网格体系的 Petri 网模拟与分析. 系统仿真学报, 2005, 17 (z1): 223-228
[122] Nemeth Z, Perez C and Priol T. Workflow enactment based on a chemical metaphor. in: B. K. Aichernig and B. Beckert (eds). 3rd IEEE International Conference on Software Engineering and Formal Methods. California: IEEE Computer Society, 2005. 127-136
[123] Groth P and Moreau M L L. Formalising a protocol for recording provenance in Grids. in: S. Cox (eds). UK OST e-Science second All Hands Meeting. Nottingham: EPSRC, 2004. 147-154
[124] 卢暾, 张望, 李志蜀, 等. 基于 I/O 自动机的网格服务组合的形式化. 华南理工大学学报(自然科学版), 2005, 33 (11): 55-60
[125] van der Aalst W M P. Pi Calculus versus Petri Nets: Let us eat humble Pie rather than further inflate the Pi hype. BPTrends, 2005, 3 (5): 1-11
[126] Smith H. Business process management—the third wave: business process modeling language (bpml) and its pi-calculus foundations. Information and Software Technology, 2003, 45: 1065-1069
[127] Lumpe M, Achermann F and Nierstrasz O. Foundations of component based systems. Cambridge: Cambridge University Press, 2000. 69-90
[128] Nierstrasz O and Meijler T D. Requirements for a composition language. Object-Based Models and Languages for Concurrent Systems, LNCS, 1995, 924: 147-161
[129] Pahl C. A formal composition and interaction model for a Web component platform. Electronic Notes in Theoretical Computer Science, 2002, 66 (4): 1-15
[130] Lumpe M. A Pi-calculus based approach for software composition. Switzerland: Institute of Computer Science and Applied Mathematics, University of Bern, 1999
[131] Vitus S W L and Julian P. Analyzing equivalences of UML statechart diagrams by structural congruence and open bisimulations. in: J. Hosking and P. Cox (eds). IEEE Symposium on Human Centric Computing Languages and Environments. New Zealand: IEEE Computer Society, 2003. 137-144
[132] Yang D and Zhang S S. Using pi-calculus to formalize UML activity diagram for business process modeling. in: P. Alexander (eds). 10th IEEE International Conference and Workshop on the Engineering of Computer-Based Systems. California: IEEE Computer Society, 2003. 47-54
[133] Puhlmann F and Weske M. Investigations on soundness regarding lazy activities. BusinessProcess Management, LNCS, 2006, 4102: 145-160
[134] Gorla D. On the relative expressive power of calculi for mobility. Technical Report in Dip. di Informatica, Univ. di Roma "La Sapienza", 2006: 1-31
[135] Dam M. Model checking mobile processes. Information and Computation, 1996, 129 (1): 35-51
[136] Bouali A, Gnesi S and Larosa S. JACK: Just another concurrency kit: The integration project. Bulletin of the European Association for Theoretical Computer Science, 1994, 54: 207-224
[137] Foster I. Globus toolkit version 4: Software for service-oriented systems. Network and Parallel Computing, LNCS, 2006, 3779: 2-13
[138] 郭小群, 郝克刚. Web 服务的 Pi 演算描述. 计算机科学, 2006, 33 (3): 261-262
[139] Bolognesi T. A conceptual framework for state-based and event-based formal behavioural specification languages. in: B. Steffen, P. Bellini, et al. (eds). 9th International Conference on Engineering of Complex Computer Systems. Florence: IEEE Computer Society, 2004. 107-116
[140] Abadi M and Lamport L. Composing specifications. ACM Transactions on Programming Languages and Systems, 1993, 15 (1): 73-132
[141] Nicola R D and Vaandrager F. Three logics for branching bisimulation. Journal of the ACM, 1995, 42 (2): 458-487
[142] Giannakopoulou D and Magee J. Fluent model checking for event-based systems. in: L. Barroca (eds). 11th ACM SIGSOFT Symposium on Foundations of Software Engineering. Helsinki: ACM, 2003. 257-266
[143] Taguchi K, Dong J S and Ciobanu G. Relating pi-calculus to Object-Z. in: B. Steffen, P. Bellini, et al. (eds). 9th International Conference on Engineering of Complex Computer Systems. Florence: IEEE Computer Society, 2004. 97-106
[144] Milner R. Communicating and Mobile Systems: the Pi Calculus. Cambridge: Cambridge University Press, 1999. 16-97
[145] Kacsuk P, Dozsa G, Kovacs J, et al. P-GRADE: A grid programming environment. Journal of Grid Computing, 2003, 1 (2): 171-197
[146] 穆黎森. CGSP 网格中工作流系统的研究:复合资源管理: [硕士论文]. 北京: 清华大学, 2006
[147] Montanari U and Pistore M. Checking bisimilarity for finitary Pi-calculus. Concurrency Theory, LNCS, 1995, 962: 42-56
[148] Chen J and Yang Y. An activity completion duration based checkpoint selection strategy for dynamic verification of fixed-time constraints in grid workflow systems. Lecture Notes in Informatics, 2005, 69: 296-310
[149] Chen J and Yang Y. Temporal dependency for dynamic verification of fixed-date constraints in grid workflow systems. Web Technologies Research and Development, LNCS, 2005, 3399: 820-831
[150] Ioannidis Y E and Sellis T K. Supporting inconsistent rules in database systems. Journal of Intelligent Information Systems, 1992, 1 (3-4): 243-270
[151] Quinlan J R. Induction of decision trees. Machine Learning, 1986, 1: 81-106
[152] Chomicki J, Lobo J and Naqvi S. Conflict resolution using logic programming. IEEE Transactions on Knowledge and Data Engineering, 2003, 15 (1): 244-249
[153] Lindgren T. Methods for rule conflict resolution. Machine Learning, LNCS, 2004, 3201: 262-273
[154] Giannakopoulou D and Lerda F. From states to transitions: Improving translation of LTL formulae to Buchi automata. Formal Techniques for Networked and Distributed Sytems, LNCS, 2002, 2529: 308-326
[155] Ho Y-C and Pepyne D L. Simple explanation of the No Free Lunch Theorem of Optimization. in: M. Dymkov, I. Gaishun, et al. (eds). EEE Conference on Decision and Control. Orlando: Institute of Electrical and Electronics Engineers Inc., 2001. 4409-4414
[156] Liu R and Kumar A. An analysis and taxonomy of unstructured workflows. Business Process Management, LNCS, 2005, 3649: 268-284
[157] Vardi M Y. On the complexity of modular model checking. in: (eds). San Diego, CA, USA: IEEE, Piscataway, NJ, USA, 1995. 101-111
[158] 董威, 王戟, 齐治昌. UML 模型中并发对象的组合验证. 计算机科学, 2005, 32 (7): 231-234
[159] Een N and Sorensson N. An extensible SAT-solver. Theory and Applications of Satisfiability Testing, LNCS, 2003, 2919: 502-518
[160] Yang C H and Dill D L. Validation with guided search of the state space. in: IEEE (eds). 35th Design Automation Conference. San Francisco: ACM, 1998. 599-604
[161] Seppi K, Jones M and Lamborn P. Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae, 2006, 70 (1-2): 111-126
[162] Ravi K and Somenzi F. Hints to accelerate symbolic traversal. Correct Hardware Design and Verification Methods, LNCS, 1999, 1703: 250-264
[163] W.M.P. van der Aalst, A.H.M. ter Hofstede, B. Kiepuszewski, et al. Workflow patterns. Distributed and Parallel Databases, 2003, 14: 5-51
[164] Havey M. Essential Business Process Modeling. USA: O'Reilly, 2005. 1-332
[165] Hulse R A and Taylor J H. Discovery of a pulsar in a binary system. Journal of Astrophys, 1975, 195: L51
[166] Mantell K. From UML to BPEL. IBM DeveloperWorks, 2005: 1-10
[167] Heinis T, Pautasso C, Alonso G. Mirroring resources or mapping requests: implementing WS-RF for grid workflows. in: IEEE (eds). 6th IEEE International Symposium on Cluster Computing and the Grid (CCGRID'06). Florence: IEEE Computer Society, 2006. 497-504