证明和测试分布式系统的功能正确性
|
摘要
由于分布式系统的固有复杂性,结合分布式系统的领域背景来证明和验证分布式系统的功能正确性一直是计算机科学领域的重要问题。机群系统和网格系统均是高度复杂的分布式系统,其中机群文件系统共享语义和网格使用模式的研究分别是涉及各自领域的功能正确性、性能和易用性的关键问题。本文首先从文件系统共享文件语义和计算机使用模式这两个方面系统地综述了机群文件系统语义和网格使用模式领域的主要研究成果。作为本文的研究重点之一,在机群文件系统共享语义研究方面,从文件缓存协议构造、语义正确性证明和共享语义测试等方面对机群文件系统共享语义的关键问题进行了深入探讨。在网格的用户使用模式研究方面,本文对用户和服务网格系统进行理论建模,提出并证明了用户3A使用服务网格必须满足的一些性质和条件。
本文创造性的工作主要有三个方面:
(1)提出了一种基于POSIX文件锁的缓存一致性协议LBCCP,该协议能够在文件粒度支持动态调整文件共享语义。本文给出了LBCCP协议的I/O自动机模型并证明了LBCCP协议的正确性,在证明过程中找到并改正了DCFS文件系统协议中的几处错误。
(2)提出了文件系统共享语义测试概念并实现了一个文件语义测试系统FSbench。FSbench目前能够测试机群文件系统最常用的两种共享语义,分别是UNIX语义和NFS语义。FSbench可用于判断应用程序在不同文件系统无缝移植的可行性和验证新文件系统的语义正确性,我们利用FSbench进行语义测试时发现了DCFS和PVFS在共享语义支持方面的一些问题,改进后的DCFS版本已经能够通过目录的UNIX语义测试。
(3)给出了用户3A (Anytime, Anyplace and on Anydevice)使用模式的定义,利用抽象状态机(ASM)理论对用户和服务网格系统进行形式化建模,并证明了服务网格3A使用模式定理。该定理给出了服务网格系统提供3A使用模式的一些充分条件和性质,这些性质可以用于指导实际网格系统的设计和实现。
Proving and verification the functional correctness of complex distributed systems in many fields are important research problems in computer science. Both Cluster System and Grid System are very complex distributed systems. Cluster file system sharing semantics and grid utilization mode are key issues that address functional correctness, performance, and usability of cluster system and grid systems, respectively. This dissertation concentrates on specifying and verifying the application characteristic of distributed systems. It first surveys the recent development of file system sharing semantics and grid utilization mode. Then, it addresses the problems of cluster file system sharing semantics, the content of research includes the followings: building the file system cache coherence protocol, proving correctness of file sharing semantics, and file sharing semantics testing. This dissertation also introduces an ASM (Abstract State Machine) model of user and service grid system and discusses some character of service grid.
The original ideas in this dissertation are explained in detail.
1. A POSIX file lock based cache coherence protocol (LBCCP) is presented, which can tune file sharing semantics dynamically. We prove correctness of LBCCP using I/O automata theory after correcting some errors in original protocol.
2. The concept of file sharing semantics test is proposed and a file sharing semantics testing system (FSbench) is implemented. FSbench can be used for UNIX or NFS semantics test. We find some bugs of DCFS and PVFS in file sharing semantics test.
3. The definitions of 3A (Any time, Any place and Any device) utilization mode are presented and a formal model of user and service grid system (USG) is built using ASM. Based on USG model and these formal definitions, a theorem on 3A utilization mode is proposed and proved.
本文创造性的工作主要有三个方面:
(1)提出了一种基于POSIX文件锁的缓存一致性协议LBCCP,该协议能够在文件粒度支持动态调整文件共享语义。本文给出了LBCCP协议的I/O自动机模型并证明了LBCCP协议的正确性,在证明过程中找到并改正了DCFS文件系统协议中的几处错误。
(2)提出了文件系统共享语义测试概念并实现了一个文件语义测试系统FSbench。FSbench目前能够测试机群文件系统最常用的两种共享语义,分别是UNIX语义和NFS语义。FSbench可用于判断应用程序在不同文件系统无缝移植的可行性和验证新文件系统的语义正确性,我们利用FSbench进行语义测试时发现了DCFS和PVFS在共享语义支持方面的一些问题,改进后的DCFS版本已经能够通过目录的UNIX语义测试。
(3)给出了用户3A (Anytime, Anyplace and on Anydevice)使用模式的定义,利用抽象状态机(ASM)理论对用户和服务网格系统进行形式化建模,并证明了服务网格3A使用模式定理。该定理给出了服务网格系统提供3A使用模式的一些充分条件和性质,这些性质可以用于指导实际网格系统的设计和实现。
Proving and verification the functional correctness of complex distributed systems in many fields are important research problems in computer science. Both Cluster System and Grid System are very complex distributed systems. Cluster file system sharing semantics and grid utilization mode are key issues that address functional correctness, performance, and usability of cluster system and grid systems, respectively. This dissertation concentrates on specifying and verifying the application characteristic of distributed systems. It first surveys the recent development of file system sharing semantics and grid utilization mode. Then, it addresses the problems of cluster file system sharing semantics, the content of research includes the followings: building the file system cache coherence protocol, proving correctness of file sharing semantics, and file sharing semantics testing. This dissertation also introduces an ASM (Abstract State Machine) model of user and service grid system and discusses some character of service grid.
The original ideas in this dissertation are explained in detail.
1. A POSIX file lock based cache coherence protocol (LBCCP) is presented, which can tune file sharing semantics dynamically. We prove correctness of LBCCP using I/O automata theory after correcting some errors in original protocol.
2. The concept of file sharing semantics test is proposed and a file sharing semantics testing system (FSbench) is implemented. FSbench can be used for UNIX or NFS semantics test. We find some bugs of DCFS and PVFS in file sharing semantics test.
3. The definitions of 3A (Any time, Any place and Any device) utilization mode are presented and a formal model of user and service grid system (USG) is built using ASM. Based on USG model and these formal definitions, a theorem on 3A utilization mode is proposed and proved.
引文
[Adr92] A. Tang, S. Scoggins. Open Networking with OSI. Prentice-Hall Press, 1992
[All01-1] W. Allcock, A. Chervenak, I. Foster, C. Kesselman, C. Salisbury, S. Tuecke. The Data Grid: Towards An Architecture for the Distributed Management and Analysis of Large Scientific Datasets. Journal of Network and Computer Applications, 2001, Vol23, pp.187-200
[All01-2] W. Allcock, J. Bester, J. Bresnahan, A. Chervenak, I. Foster, C. Kesselman, S. Meder, V. Nefedova, D. Quesnel, and S. Tuecke. Data Management and Transfer in High-Performance Computational Grid Environments. Parallel Computing, 2001
[All02] W. Allcock, J. Bresnahan, I. Foster, L. Liming, J. Link, P. Plaszczac. Technical Report: GridFTP Update. January 2002
[Avr99] D. R. Avresky. Formal Verification and Testing of Protocol. Computer Communications 22, 1999, pp.681-690
[Bar98] J. Barkes, M. R. Barrios, F. Cougard, P. G. Crumley, D. Marin, H. Reddy, T. Thitayanun. GPFS: A Parallel File System. SG24-5165-00, April 1998
[Bar99] M. Barjaktarovic. The State-of-the-art in Formal Methods. AFOSR Summer Research technical report for Rome Research Site, AFRL/IFGB, http://www.wetstonetech.com/fm_quest.html
[Bin94] R. Binder, Object-Oriented Software Testing. Communications of the ACM, Sept. 1994, Vol.37, No.9, pp.28-29
[Bor03] E. B?rger, R. Stark. Abstract State Mahcines-A Method for High-Level System Design and Analysis. Springer-Verlag Berlin Heidelberg, 2003
[Bow95-1] J. P. Bowen, M.G. Hinchey. Ten Commandments of Formal Methods. IEEE Computer, April 1995, 28(4) pp.56-63
[Bow95-2] J. P. Bowen, M. G. Hinchey. Seven More Myths of Formal Methods. IEEE Software, July 1995, 12(4) pp.34-41
[Bra02] P. J. Braam et al. The Lustre Storage Architecture. Cluster File Systems, Inc., Mountain View, CA, 2002
[Bu02] 卜冠英. 计算网格自动机模型及其应用. 博士学位论文,中科院计算技术研究所,2002 年 6 月
[Bur00-1] R. C. Burns, R. M. Rees, and D. D. E. Long. Consistency and Locking for Distributing Updates to Web Servers Using a File System. Performance and Architecture of Web Servers (PAWS), Peformance Evaluation Review , 28(2), ACM, June 2000
[Bur00-2] R. C. Burns. Data Management in a Distributed File System for Storage Area Networks. Ph.D dissertation, University of California, Santa Cruz, March 2000
[Cal00] B. Callaghan. NFS Illustrated. Addison-Wesley. April 2000
[Car95] R. Card, T. Ts'o, S. Tweedie. Design and Implementation of the Second Extended Filesystem. In Proceedings of the First Dutch International Symposium on Linux, 1995
[Car00] P. H. Carns, W. B. Ligon III, R. B. Ross, and R. Thakur. PVFS: A Parallel File System For Linux Clusters. In Proceedings of the 4th Annual Linux Showcase and Conference, Atlanta, GA, October 2000, pp.317-327
[Cla96] E. Clarke, J. Wing. Formal Methods: State of the Art and Future Directions. CMU Computer Science Technical Report CMU-CS-96-178, August 1996
[Dou02] 都志辉,陈渝,刘鹏. 网格计算. 清华大学出版社,2002
[Dijk72] E. W. Dijkstra. Notes on Structured Programming. Structure Programming, Academic Press, 1972
[Feng01] 冯军. 机群文件系统性能优化中的关键问题研究. 硕士学位论文, 中科院计算技术研究所, 2001 年 6 月
[Fos97] I. Foster and C. Kesselman. Globus: A Metacomputing Infrastructure Toolkit. Intl J. Supercomputer Applications, 1997, 11(2) 115-128
[Fos98] I. Foster and C. Kesselman. The Globus Project: A Status Report. In Proceedings of IPPS/SPDP '98 Heterogeneous Computing Workshop, 1998
[Fos99] I. Foster, C. Kesselman. The Grid: Blueprint for a New Computing infrastructure. Morgan Kaufmann Publishers, 1999
[Fos01] I. Foster, C. Kesselman and S. Tuecke. The Anatomy of the Grid: Enabling Scalable Virtual Organizations. International Journal of Supercomputer Applications, 2001,Vol. 15, No. 3
[Fos02-1] I. Foster. The Grid: A New Infrastructure for 21st Century Science. Physics Today, 2002, 55(2), pp.42-47
[Fos02-2] I. Foster, C. Kesselman, J. Nick, S. Tuecke. Grid Services for Distributed Systems Integration. IEEE Computer, 2002, 35 (6), pp.37-46
[Gla01] U. Gl?sser, Y. Gurevich, M. Veanes. Universal Plug and Play Machine Models. Technical Report: MSR-TR-2001-59, Microsoft Research, 2001
[Glo04] Globus Toolkit 3.2 Documentation. http://www-unix.globus.org/toolkit/docs/3.2/index.html
[Goe98] A. Goel, C. Pu and G. J. Popek. View Consistency for Optimistic Replication. In Symposium on Reliable Distributed Systems, 1998, pp.36-42
[Gre01] R. Greenlaw, E. Happ. Inline/Online: Fundamentals of The Internet and The World Wide Web. The McGraw-Hill Companies, Inc., 2001
[Guo01] 郭梯云,杨家玮,李建东. 数字移动通信. 人民邮电出版社,2001
[Gur95] Y. Gurevich. Evolving Algebras 1993: Lipari Guide. Specification and Validation Methods, Oxford University Press, 1995, pp. 266-292
[Gur00] Y. Gurevich. Sequential Abstract-State Machines Capture Sequential Algorithms. ACM Transactions on Computational Logic, July 2000, Vol. 1, No. 1, pp.77–111
[Gut99] W. J. Gutjahr. Partition Testing vs. Random Testing: The Influence of Uncertainty. IEEE Transactions on Software Engineering, september/october 1999, Vol. 25, No. 5
[Hal90] J. A. Hall. Seven Myths of Formal Methods. IEEE Software, September 1990, 7(5) pp.11-19
[Has98] R. L. Haskin. Tiger Shark- a scalable file system for multimedia. IBM Journal of Research and Development, March 1998, Vol.42, No.2, pp.185-197
[He02] 贺劲. 机群文件系统性能与正确性研究. 博士学位论文,中科院计算技术研究所,2002 年 6 月
[He03] J. He, J. Xiong, S. Wu, Y. Lu, D. Men. DCFS: File Service in Commodity Cluster Dawning4000. The 4th International Parallel and Distributed Computing, Applications and Technologies, Cheng Du, China, August 27-29, 2003
[How88] J. H. Howard. A Overview of the Andrew File System. In Proceedings of UESNIX Winter Conference, February 1988(Dallas, Texas), pp.23-26
[Hu96] W. Hu. Correct Event Ordering in Share-Memory Systems. Ph.D. Thesis, Chinese Academy of Sciences: Institute of Computing Technology, 1996
[Hwa98] K. Hwang, Z. Xu. Scalable Parallel Computing Technology, Architecutre, Programming. McGraw-Hill, Inc., 1998
[IBM03] The Era of Grid Computing: A new standard for successful IT strategies. http://www-1.ibm.com/grid/pdf/it_exec_brief.pdf, January 2003
[IEEE83] IEEE Standard Glossary. IEEE Std 729-1983
[IEEE96] IEEE/ANSI Std. 1003.1. Portable Operating System Interface (POSIX)-Part 1: System Application Program Interface (API)
[C Language], 1996 edition
[IEEE04] IEEE POSIX Test Suite. http://www.opengroup.org/testing/testsuites/posix.html
[Mye79] G. J. Myers. The Art of Software Testing. New York: John Wiley & Sons, Inc. 1979
[Kaz90] M. L. Kazar et al. DEcorum file system architectural overview. In Proceedings of the Summer USENIX Conference, Anaheim, CA, June 1990, pp.151-163
[Kre01] H. Kreger. Web Services Conceptual Architecture. IBM Technical Report WCSA 1.0, 2001
[Kun96] A. Kunzmann. Efficient random testing with global weights. Design Automation Conference, 1996, with EURO-VHDL '96 and Exhibition, In Proceedings of EURO-DAC '96, European, September 1996, pp.227-232
[Lib03] 李丙辰,徐志伟. GSML 网格编程语言的一种实现方法. 计算机研究与发展,2003,40(12)pp.1715-1719
[Lig99] W. B. Ligon III and R. B. Ross. An Overview of the Parallel Virtual File System. In Proceedings of the 1999 Extreme Linux Workshop, June 1999
[Liy02] 李艳彬. 网格使用模式关键技术的研究. 硕士学位论文,国防科技大学,2002 年 3月
[Lew95] T. G. Lewis. Where is the Client/Server Software Headed. Computer, April 1995 Vol. 28, No. 4, pp.49-55
[Lu04] 吕毅,马捷,唐荣锋. FSbench: 一个机群文件系统基准程序. 计算机工程,2004,30(2), pp.49-51
[Lyn96] N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996
[McV96] L. McVoy. lmbench: Portable Tools for Performance Analysis. In Proceedings of the USENIX 1996 Annual Technical Conference, San Diego, California, USA, January 1996
[Moh94] A. Mohindra, M. Devarakonda. Distrubted Token Management in Calypso File System. In Proceedings of the IEEE Symposium on Parallel and Distributed Processing, New York, 1994
[MPI97] Message Passing Interface Forum. MPI-2: Extensions to the Message-Passing Interface. July, 1997, http://www.mpi-forum.org/docs/docs.html
[MPI04] MPI Test Suite. http://www-unix.mcs.anl.gov/mpi/mpi-test/tsuite.html
[Mum94] L. B. Mummert and M. Satyanarayanan. Variable Granularity Cache Coherence. ACM Operating Systems Review, January 1994, Vol.28, No.1, pp.55-60
[Mum96] L. B. Mummert. Exploiting Weak Connectivity in a Distributed File System. Ph.D dissertation. Computer Science Division, School of Computer Science, Carnegie Mellon University, December 1996
[Nem03] Z. Németh, V. Sunderam. Charactering Crids: Attributes, Definitions, and Formalisms. Journal of Grid Computing, 1, 2003, pp.9-23
[NFS89] NFS: Network File System Protocol Specification. RFC 1094, March 1989, http://www.ietf.org/rfc/rfc1094.txt?number=1094
[NFS95] NFS Version 3 Protocol Specification. RFC 1813, June 1995, http://www.ietf.org/rfc/rfc1813.txt?number=1813
[NFS04] NFS Connectathon. http://www.connectathon.org/
[Nor03] W. Norcott, Don Capps. IOzone Filesystem Benchmark. http://www.iozone.org/
[Pre99] K. W. Preslan et al. A 64-bit, Shared Disk File System for Linux. Sixteenth IEEE Mass Storage Systems Symposium, 1999
[Pre00] K. W. Preslan et al. Implementing Journaling in a Linux Shared Disk File System. In Proceedings of the Eighth NASA Goddard Conference on Mass Storage Systems and Technologies, 2000
[Raf90] O. Rafiq, R.Castanet. From Conformance Testing to Interoperability Testing. the 3rd International Workshop on Protocol Test Systems, 1990
[Rob99] D. Robinson. The Advancement of NFS Benchmarking: SFS 2.0. 13th Systems Administration Conference, Seattle, Washington, USA, November 1999
[Rom02] M. Roman, C. Hess et al. A Middleware Infrastructure for Active Spaces. IEEE Pervasive Computing, 2002, Vol. 1, No. 4, pp.74-83
[Sad00] D. Sadoski,F. Rogers. Client/server Software Architectures-An Overview. Carnegie Mellon University, 22 September,2000, http://www.sei.cmu.edu/str/descriptions/clientserver_body.html
[Sar93] B. Sarikaya. Principles of Protocol Engineering and Conformance Testing. Ellis Horwood, 1993
[Sat01] M. Satyanarayanan. Pervasive Computing: Vision and Chanllenges. IEEE Personal Communications, August 2001, pp.10-17
[Sch02] F. Schmuck, R. Haskin. GPFS: A Shared-Disk File system for Large Computing Clusters. In Proceedings of the Conference on File and Storage Technologies (FAST’02), 2002, pp.231-244
[Sid89] D. Sidhu, T. Leung. Formal method for protocol testing: A detailed study. IEEE Transactions on Software Engineering, April 1989, Vol.15, No.4, pp.413-426
[Sto01] H. Stockinger, A. Samar, B. Allcock, I. Foster, K. Holtman, B. Tierney. File and Object Replication in Data Grids. In Proceedings of the Tenth International Symposium on High Performance Distributed Computing (HPDC-10), IEEE Press, August 2001
[Tal03] V. Talwar, S. Basu, R. Kumar. An Environment for Enabling Interactive Grids. In proceedings of 12th IEEE International Symposium on High Performance Distributed Computing (HPDC'03), Seattle, Washington, June 22-24, 2003, pp.184-193
[Top03] http://www.top500.org/lists/2003/11/trends.php
[Tan95] A. S. Tanenbaum. Distributed Operating Systems. Prentice Hall, International, Inc., 1995
[Tha99] R. Thakur, W. Gropp, E. Lusk. On Implementing MPI-IO Portably and with High Performance. In Proceedings of the Sixth Workshop on I/O in Parallel and Distributed Systems, May 1999, pp. 23-32
[Tha02] R. Thakur, W. Gropp, E. Lusk. Optimizing Noncontiguous Accesses in MPI-IO. Parallel Computing, January 2002, (28)1, pp83-105
[Tian01] 田军. IPv6 协议一致性测试研究及测试系统实现. 博士学位论文, 中科院计算技术研究所, 2001 年 6 月
[Wang99] 王建勇. 可扩展的单一映象的文件系统. 博士学位论文, 中科院计算技术研究所, 1999 年 6 月
[Wang02] J. Wang, Z. Xu. Cluster File System: A Case Study. Journal of Future Generation Computer Systems, Vol. 18, No.3, Jan. 2002, pp.373-387
[Wang03] Y. Wang, Z. Xu. Research of On-line Expandability of Service Grid. The Second International Workshop on Grid and Cooperative Computing, Shanghai, China, 2003
[Wei91] M. Weiser. The Computer for the 21st Century. Science American, September 1991
[Win90] J. M. Wing. A Specifier's Introduction to Formal Methods. IEEE Computer, September 1990, 23(9), pp.8-24
[Wit93] M. Wittle, B. E. Keith. LADDIS: The Next Generation In NFS File Server Benchmarking. In Proceedings of the USENIX Summer Technical Conference, Cincinnati, Ohio, USA, June 1993
[Wu04] 吴思宁. 可扩展机群文件系统研究. 博士学位论文, 中科院计算技术研究所, 2004 年5 月
[Xio03] J. Xiong, S. Wu, D. Meng, N. Sun, G. Li. Design and Performance of the Dawning Cluster File System. 2003 IEEE International Conference on Cluster Computing (Cluster2003), Hong Kong, December 2003
[Xu02-1] 徐志伟. 织女星网格:关键问题与设计原理. 织女星网格文档 VGD-2,2002 年 11月,pp.1-40
[Xu02-2] 徐志伟,李伟. 织女星网格的体系结构研究. 计算机研究与发展,2002,39(8)pp.923-929
[Xu03-1] 徐志伟. 网程:动机、需求与行为. 织女星网格文档 VGS-3,2003 年 5 月,pp.1-13
[Xu03-2] 徐志伟. 初论人机社会:一种网络计算模式. 织女星网格文档 VGS-4,2003 年 6 月,pp.1-10
[Xug03] 徐光佑,史元春,谢伟凯. 普适计算. 计算机学报,2003,26(9)pp.1042-1050
[Yang03] 杨宁,李晓林,周浩杰,潘高峰. K/G:一种网格的使用模式体系结构及应用. 计算机研究与发展,2003,40(12)pp.1720-1724
[Yu00] H. Yu, A. Vahdat. Design and Evaluation of a Continuous Consistency Model for Replicated Services. In Proceedings of the Fourth Symposium on Operating Systems Design and Implementation (OSDI), October 2000
[Zhao01] 赵瑞莲. 软件测试方法研究. 博士学位论文, 中科院计算技术研究所, 2001 年 6 月
[Zhen92] 郑人杰. 计算机软件测试技术. 清华大学出版社,1992
[All01-1] W. Allcock, A. Chervenak, I. Foster, C. Kesselman, C. Salisbury, S. Tuecke. The Data Grid: Towards An Architecture for the Distributed Management and Analysis of Large Scientific Datasets. Journal of Network and Computer Applications, 2001, Vol23, pp.187-200
[All01-2] W. Allcock, J. Bester, J. Bresnahan, A. Chervenak, I. Foster, C. Kesselman, S. Meder, V. Nefedova, D. Quesnel, and S. Tuecke. Data Management and Transfer in High-Performance Computational Grid Environments. Parallel Computing, 2001
[All02] W. Allcock, J. Bresnahan, I. Foster, L. Liming, J. Link, P. Plaszczac. Technical Report: GridFTP Update. January 2002
[Avr99] D. R. Avresky. Formal Verification and Testing of Protocol. Computer Communications 22, 1999, pp.681-690
[Bar98] J. Barkes, M. R. Barrios, F. Cougard, P. G. Crumley, D. Marin, H. Reddy, T. Thitayanun. GPFS: A Parallel File System. SG24-5165-00, April 1998
[Bar99] M. Barjaktarovic. The State-of-the-art in Formal Methods. AFOSR Summer Research technical report for Rome Research Site, AFRL/IFGB, http://www.wetstonetech.com/fm_quest.html
[Bin94] R. Binder, Object-Oriented Software Testing. Communications of the ACM, Sept. 1994, Vol.37, No.9, pp.28-29
[Bor03] E. B?rger, R. Stark. Abstract State Mahcines-A Method for High-Level System Design and Analysis. Springer-Verlag Berlin Heidelberg, 2003
[Bow95-1] J. P. Bowen, M.G. Hinchey. Ten Commandments of Formal Methods. IEEE Computer, April 1995, 28(4) pp.56-63
[Bow95-2] J. P. Bowen, M. G. Hinchey. Seven More Myths of Formal Methods. IEEE Software, July 1995, 12(4) pp.34-41
[Bra02] P. J. Braam et al. The Lustre Storage Architecture. Cluster File Systems, Inc., Mountain View, CA, 2002
[Bu02] 卜冠英. 计算网格自动机模型及其应用. 博士学位论文,中科院计算技术研究所,2002 年 6 月
[Bur00-1] R. C. Burns, R. M. Rees, and D. D. E. Long. Consistency and Locking for Distributing Updates to Web Servers Using a File System. Performance and Architecture of Web Servers (PAWS), Peformance Evaluation Review , 28(2), ACM, June 2000
[Bur00-2] R. C. Burns. Data Management in a Distributed File System for Storage Area Networks. Ph.D dissertation, University of California, Santa Cruz, March 2000
[Cal00] B. Callaghan. NFS Illustrated. Addison-Wesley. April 2000
[Car95] R. Card, T. Ts'o, S. Tweedie. Design and Implementation of the Second Extended Filesystem. In Proceedings of the First Dutch International Symposium on Linux, 1995
[Car00] P. H. Carns, W. B. Ligon III, R. B. Ross, and R. Thakur. PVFS: A Parallel File System For Linux Clusters. In Proceedings of the 4th Annual Linux Showcase and Conference, Atlanta, GA, October 2000, pp.317-327
[Cla96] E. Clarke, J. Wing. Formal Methods: State of the Art and Future Directions. CMU Computer Science Technical Report CMU-CS-96-178, August 1996
[Dou02] 都志辉,陈渝,刘鹏. 网格计算. 清华大学出版社,2002
[Dijk72] E. W. Dijkstra. Notes on Structured Programming. Structure Programming, Academic Press, 1972
[Feng01] 冯军. 机群文件系统性能优化中的关键问题研究. 硕士学位论文, 中科院计算技术研究所, 2001 年 6 月
[Fos97] I. Foster and C. Kesselman. Globus: A Metacomputing Infrastructure Toolkit. Intl J. Supercomputer Applications, 1997, 11(2) 115-128
[Fos98] I. Foster and C. Kesselman. The Globus Project: A Status Report. In Proceedings of IPPS/SPDP '98 Heterogeneous Computing Workshop, 1998
[Fos99] I. Foster, C. Kesselman. The Grid: Blueprint for a New Computing infrastructure. Morgan Kaufmann Publishers, 1999
[Fos01] I. Foster, C. Kesselman and S. Tuecke. The Anatomy of the Grid: Enabling Scalable Virtual Organizations. International Journal of Supercomputer Applications, 2001,Vol. 15, No. 3
[Fos02-1] I. Foster. The Grid: A New Infrastructure for 21st Century Science. Physics Today, 2002, 55(2), pp.42-47
[Fos02-2] I. Foster, C. Kesselman, J. Nick, S. Tuecke. Grid Services for Distributed Systems Integration. IEEE Computer, 2002, 35 (6), pp.37-46
[Gla01] U. Gl?sser, Y. Gurevich, M. Veanes. Universal Plug and Play Machine Models. Technical Report: MSR-TR-2001-59, Microsoft Research, 2001
[Glo04] Globus Toolkit 3.2 Documentation. http://www-unix.globus.org/toolkit/docs/3.2/index.html
[Goe98] A. Goel, C. Pu and G. J. Popek. View Consistency for Optimistic Replication. In Symposium on Reliable Distributed Systems, 1998, pp.36-42
[Gre01] R. Greenlaw, E. Happ. Inline/Online: Fundamentals of The Internet and The World Wide Web. The McGraw-Hill Companies, Inc., 2001
[Guo01] 郭梯云,杨家玮,李建东. 数字移动通信. 人民邮电出版社,2001
[Gur95] Y. Gurevich. Evolving Algebras 1993: Lipari Guide. Specification and Validation Methods, Oxford University Press, 1995, pp. 266-292
[Gur00] Y. Gurevich. Sequential Abstract-State Machines Capture Sequential Algorithms. ACM Transactions on Computational Logic, July 2000, Vol. 1, No. 1, pp.77–111
[Gut99] W. J. Gutjahr. Partition Testing vs. Random Testing: The Influence of Uncertainty. IEEE Transactions on Software Engineering, september/october 1999, Vol. 25, No. 5
[Hal90] J. A. Hall. Seven Myths of Formal Methods. IEEE Software, September 1990, 7(5) pp.11-19
[Has98] R. L. Haskin. Tiger Shark- a scalable file system for multimedia. IBM Journal of Research and Development, March 1998, Vol.42, No.2, pp.185-197
[He02] 贺劲. 机群文件系统性能与正确性研究. 博士学位论文,中科院计算技术研究所,2002 年 6 月
[He03] J. He, J. Xiong, S. Wu, Y. Lu, D. Men. DCFS: File Service in Commodity Cluster Dawning4000. The 4th International Parallel and Distributed Computing, Applications and Technologies, Cheng Du, China, August 27-29, 2003
[How88] J. H. Howard. A Overview of the Andrew File System. In Proceedings of UESNIX Winter Conference, February 1988(Dallas, Texas), pp.23-26
[Hu96] W. Hu. Correct Event Ordering in Share-Memory Systems. Ph.D. Thesis, Chinese Academy of Sciences: Institute of Computing Technology, 1996
[Hwa98] K. Hwang, Z. Xu. Scalable Parallel Computing Technology, Architecutre, Programming. McGraw-Hill, Inc., 1998
[IBM03] The Era of Grid Computing: A new standard for successful IT strategies. http://www-1.ibm.com/grid/pdf/it_exec_brief.pdf, January 2003
[IEEE83] IEEE Standard Glossary. IEEE Std 729-1983
[IEEE96] IEEE/ANSI Std. 1003.1. Portable Operating System Interface (POSIX)-Part 1: System Application Program Interface (API)
[C Language], 1996 edition
[IEEE04] IEEE POSIX Test Suite. http://www.opengroup.org/testing/testsuites/posix.html
[Mye79] G. J. Myers. The Art of Software Testing. New York: John Wiley & Sons, Inc. 1979
[Kaz90] M. L. Kazar et al. DEcorum file system architectural overview. In Proceedings of the Summer USENIX Conference, Anaheim, CA, June 1990, pp.151-163
[Kre01] H. Kreger. Web Services Conceptual Architecture. IBM Technical Report WCSA 1.0, 2001
[Kun96] A. Kunzmann. Efficient random testing with global weights. Design Automation Conference, 1996, with EURO-VHDL '96 and Exhibition, In Proceedings of EURO-DAC '96, European, September 1996, pp.227-232
[Lib03] 李丙辰,徐志伟. GSML 网格编程语言的一种实现方法. 计算机研究与发展,2003,40(12)pp.1715-1719
[Lig99] W. B. Ligon III and R. B. Ross. An Overview of the Parallel Virtual File System. In Proceedings of the 1999 Extreme Linux Workshop, June 1999
[Liy02] 李艳彬. 网格使用模式关键技术的研究. 硕士学位论文,国防科技大学,2002 年 3月
[Lew95] T. G. Lewis. Where is the Client/Server Software Headed. Computer, April 1995 Vol. 28, No. 4, pp.49-55
[Lu04] 吕毅,马捷,唐荣锋. FSbench: 一个机群文件系统基准程序. 计算机工程,2004,30(2), pp.49-51
[Lyn96] N. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996
[McV96] L. McVoy. lmbench: Portable Tools for Performance Analysis. In Proceedings of the USENIX 1996 Annual Technical Conference, San Diego, California, USA, January 1996
[Moh94] A. Mohindra, M. Devarakonda. Distrubted Token Management in Calypso File System. In Proceedings of the IEEE Symposium on Parallel and Distributed Processing, New York, 1994
[MPI97] Message Passing Interface Forum. MPI-2: Extensions to the Message-Passing Interface. July, 1997, http://www.mpi-forum.org/docs/docs.html
[MPI04] MPI Test Suite. http://www-unix.mcs.anl.gov/mpi/mpi-test/tsuite.html
[Mum94] L. B. Mummert and M. Satyanarayanan. Variable Granularity Cache Coherence. ACM Operating Systems Review, January 1994, Vol.28, No.1, pp.55-60
[Mum96] L. B. Mummert. Exploiting Weak Connectivity in a Distributed File System. Ph.D dissertation. Computer Science Division, School of Computer Science, Carnegie Mellon University, December 1996
[Nem03] Z. Németh, V. Sunderam. Charactering Crids: Attributes, Definitions, and Formalisms. Journal of Grid Computing, 1, 2003, pp.9-23
[NFS89] NFS: Network File System Protocol Specification. RFC 1094, March 1989, http://www.ietf.org/rfc/rfc1094.txt?number=1094
[NFS95] NFS Version 3 Protocol Specification. RFC 1813, June 1995, http://www.ietf.org/rfc/rfc1813.txt?number=1813
[NFS04] NFS Connectathon. http://www.connectathon.org/
[Nor03] W. Norcott, Don Capps. IOzone Filesystem Benchmark. http://www.iozone.org/
[Pre99] K. W. Preslan et al. A 64-bit, Shared Disk File System for Linux. Sixteenth IEEE Mass Storage Systems Symposium, 1999
[Pre00] K. W. Preslan et al. Implementing Journaling in a Linux Shared Disk File System. In Proceedings of the Eighth NASA Goddard Conference on Mass Storage Systems and Technologies, 2000
[Raf90] O. Rafiq, R.Castanet. From Conformance Testing to Interoperability Testing. the 3rd International Workshop on Protocol Test Systems, 1990
[Rob99] D. Robinson. The Advancement of NFS Benchmarking: SFS 2.0. 13th Systems Administration Conference, Seattle, Washington, USA, November 1999
[Rom02] M. Roman, C. Hess et al. A Middleware Infrastructure for Active Spaces. IEEE Pervasive Computing, 2002, Vol. 1, No. 4, pp.74-83
[Sad00] D. Sadoski,F. Rogers. Client/server Software Architectures-An Overview. Carnegie Mellon University, 22 September,2000, http://www.sei.cmu.edu/str/descriptions/clientserver_body.html
[Sar93] B. Sarikaya. Principles of Protocol Engineering and Conformance Testing. Ellis Horwood, 1993
[Sat01] M. Satyanarayanan. Pervasive Computing: Vision and Chanllenges. IEEE Personal Communications, August 2001, pp.10-17
[Sch02] F. Schmuck, R. Haskin. GPFS: A Shared-Disk File system for Large Computing Clusters. In Proceedings of the Conference on File and Storage Technologies (FAST’02), 2002, pp.231-244
[Sid89] D. Sidhu, T. Leung. Formal method for protocol testing: A detailed study. IEEE Transactions on Software Engineering, April 1989, Vol.15, No.4, pp.413-426
[Sto01] H. Stockinger, A. Samar, B. Allcock, I. Foster, K. Holtman, B. Tierney. File and Object Replication in Data Grids. In Proceedings of the Tenth International Symposium on High Performance Distributed Computing (HPDC-10), IEEE Press, August 2001
[Tal03] V. Talwar, S. Basu, R. Kumar. An Environment for Enabling Interactive Grids. In proceedings of 12th IEEE International Symposium on High Performance Distributed Computing (HPDC'03), Seattle, Washington, June 22-24, 2003, pp.184-193
[Top03] http://www.top500.org/lists/2003/11/trends.php
[Tan95] A. S. Tanenbaum. Distributed Operating Systems. Prentice Hall, International, Inc., 1995
[Tha99] R. Thakur, W. Gropp, E. Lusk. On Implementing MPI-IO Portably and with High Performance. In Proceedings of the Sixth Workshop on I/O in Parallel and Distributed Systems, May 1999, pp. 23-32
[Tha02] R. Thakur, W. Gropp, E. Lusk. Optimizing Noncontiguous Accesses in MPI-IO. Parallel Computing, January 2002, (28)1, pp83-105
[Tian01] 田军. IPv6 协议一致性测试研究及测试系统实现. 博士学位论文, 中科院计算技术研究所, 2001 年 6 月
[Wang99] 王建勇. 可扩展的单一映象的文件系统. 博士学位论文, 中科院计算技术研究所, 1999 年 6 月
[Wang02] J. Wang, Z. Xu. Cluster File System: A Case Study. Journal of Future Generation Computer Systems, Vol. 18, No.3, Jan. 2002, pp.373-387
[Wang03] Y. Wang, Z. Xu. Research of On-line Expandability of Service Grid. The Second International Workshop on Grid and Cooperative Computing, Shanghai, China, 2003
[Wei91] M. Weiser. The Computer for the 21st Century. Science American, September 1991
[Win90] J. M. Wing. A Specifier's Introduction to Formal Methods. IEEE Computer, September 1990, 23(9), pp.8-24
[Wit93] M. Wittle, B. E. Keith. LADDIS: The Next Generation In NFS File Server Benchmarking. In Proceedings of the USENIX Summer Technical Conference, Cincinnati, Ohio, USA, June 1993
[Wu04] 吴思宁. 可扩展机群文件系统研究. 博士学位论文, 中科院计算技术研究所, 2004 年5 月
[Xio03] J. Xiong, S. Wu, D. Meng, N. Sun, G. Li. Design and Performance of the Dawning Cluster File System. 2003 IEEE International Conference on Cluster Computing (Cluster2003), Hong Kong, December 2003
[Xu02-1] 徐志伟. 织女星网格:关键问题与设计原理. 织女星网格文档 VGD-2,2002 年 11月,pp.1-40
[Xu02-2] 徐志伟,李伟. 织女星网格的体系结构研究. 计算机研究与发展,2002,39(8)pp.923-929
[Xu03-1] 徐志伟. 网程:动机、需求与行为. 织女星网格文档 VGS-3,2003 年 5 月,pp.1-13
[Xu03-2] 徐志伟. 初论人机社会:一种网络计算模式. 织女星网格文档 VGS-4,2003 年 6 月,pp.1-10
[Xug03] 徐光佑,史元春,谢伟凯. 普适计算. 计算机学报,2003,26(9)pp.1042-1050
[Yang03] 杨宁,李晓林,周浩杰,潘高峰. K/G:一种网格的使用模式体系结构及应用. 计算机研究与发展,2003,40(12)pp.1720-1724
[Yu00] H. Yu, A. Vahdat. Design and Evaluation of a Continuous Consistency Model for Replicated Services. In Proceedings of the Fourth Symposium on Operating Systems Design and Implementation (OSDI), October 2000
[Zhao01] 赵瑞莲. 软件测试方法研究. 博士学位论文, 中科院计算技术研究所, 2001 年 6 月
[Zhen92] 郑人杰. 计算机软件测试技术. 清华大学出版社,1992