期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

网格服务链模型的验证分析技术及应用 被引量：1

原文传递
导出
摘要 确保网格应用中大规模资源共享和复杂任务处理的正确性与可靠性是一项重要的工作.文中从形式化方法的角度出发,提出了基于状态Pi演算的网格服务链模型作为对网格中服务协作与组合进行建模和分析的理论工具.其中,状态Pi演算针对Web服务资源框架(WSRF)的思想,协调了系统状态与行为间的关系,扩展了Pi演算对系统状态的全生命周期管理能力.在此基础上,进一步结合了模型验证技术对网格服务链进行设计和运行时的逻辑性质分析.通过材料形变与断裂过程动态分析的网格应用案例,展示了采用上述方法对网格应用进行需求验证和可靠性分析的有效性.
作者 许可 王跃宣 吴澄
机构地区 清华大学自动化系
出处 《中国科学（E辑）》 CSCD 北大核心 2007年第4期467-485,共19页 Science in China(Series E)
基金 国家自然科学基金资助项目(批准号:60604033和60553001)
关键词 网格 网格服务链 形式化方法 模型验证 状态Pi演算
分类号 TP393.01 [自动化与计算机技术—计算机应用技术] TP391.41 [自动化与计算机技术—计算机应用技术]
  • 相关文献

参考文献33

  • 1Joseph J, Fellenstein C. Grid Computing. USA: IBM Press, 2003. 3-25
  • 2Bolognesi T. A conceptual framework for state-based and event-based formal behavioral specification languages. In: Pierfrancesco B, Shawn A B, Bernhard S, eds. Proe 9th IEEE Int Conf on Engineering of Complex Computer Systems. CA:IEEE Press, 2004. 107-116
  • 3Xu 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. Berlin: Springer-Verlag,2006. 537-546
  • 4Wang 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. Berlin: Springer-Verlag, 2005.40-47
  • 5Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge: MIT Press, 1999. 1-97
  • 6Nemeth Z, Sunderam V. Characterizing grids attributes, definitions, and formalisms. J Grid Compu, 2003, 1(1): 9-23
  • 7Nemeth Z. Definition of a parallel execution model with abstract state machine. Acta Cyber, 2002, 15(3): 417-455
  • 8Sangiorgi D, Walker D. The Pi-calculus: A Theory of Mobile Processes. Cambridge: Cambridge University Press, 1999.11-154
  • 9Pahl 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
  • 10Manuei M, Sergio G. A case study of web services orchestration. In: Jacquet J M, Picco G E eds. Coordication Models and Languages. Lect Notes in Comput Sci, Vol 3454. Berlin: Springer-Verlag, 2005. 1-16

二级参考文献11

  • 1李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述[J].计算机研究与发展,2004,41(7):1097-1103. 被引量：25
  • 2Jim Davies, Jim Woodcock. Using Z: Specification, Refinement and Proof. Prentice Hall International Series in Computer Science, 1996.
  • 3Asokan. Fairness in Electronic Commerce. PhD thesis, University of Waterloo, May 1998.
  • 4Steve KREMER Formal Analysis of Optimistic Fair Exchange Protocols. PhD thesis, Universit'e Libre de Bruxelles Facult'e des Sciences, 2003-2004.
  • 5Rohit Chadha, Max Kanovich, Andre Scedrov. Inductive methods and contract signing protocols. In:Pierangela Samarati, ed. 8th ACM Conference on Computer and Communications Security, Philadelphia,PA: ACM Press, November 2001, 176-185.
  • 6Steve A. Schneider. Formal analysis of a non-repudiation protocol. In: 11th IEEE Computer Security Foundations Workshop, Washington-Brussels-Tokyo, IEEE June, 1998. 54-65.
  • 7Giampaolo Bella, Lawrence C. Paulson. Mechanical proofs about a nonrepudiation protocol. In: Richard J.Boulton, Paul B. Jackson, ed. Theorem Proving in Higher Order Logics, volume 2152 of Lecture Notes in Computer Science, Springer-Verlag, 2001, 91-104.
  • 8Colin Boyd ,Peter Kearney. Exploring fair exchange protocols using speci.cationanimation. In: Joseph Pieprzyk, Eiji Okamoto, Jennifer Seberry, ed. Information Security-International Workshop on Information Security, volume 1975 of Lecture Notes in Computer Science,Wollogong, Australia, Springer-Verlag.December 2000.
  • 9白硕,隋立颖,陈庆锋,付岩,庄超.安全协议的验证逻辑[J].软件学报,2000,11(2):213-221. 被引量：18
  • 10卿斯汉.安全协议的设计与逻辑分析[J].软件学报,2003,14(7):1300-1309. 被引量：69

共引文献14

同被引文献2

引证文献1

中国科学（E辑）
2007年 第4期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部