摘要OpenStack作为一个云平台管理项目，因其开放性和高效性而被广泛地应用到公共云和私有云的建设和管理当中。在实际的应用中，需要对云计算服务进行测试，若使用自然语言描述则存在内容二义性，无法准确描述服务的问题。本文介绍OpenStack云计算的计算组件NOVA服务、存储组件SWIFT服务、镜像管理组件GLANCE服务和身份认证服务KEYSTONE，并使用形式化代数规约方法对计算组件NOVA服务进行精确描述。65992

毕业论文关键词：OpenStack ,云计算，形式化方法，代数规约

Abstract

   As a management project，OpenStack cloud platform is widely applied to public and private clouds among the construction and management for its openness and efficiency .In practical applications, there is the need for cloud computing services for testing。If use natural language ，the description of the contents of ambiguity exists, and can not accurately describe the services. This article describes the OpenStack cloud computing components NOVA services, storage components SWIFT services, image management component GLANCE services and authentication services KEYSTONE, and using formal algebraic specification method for accurate calculation component NOVA service description. 

Keywords：OpenStack，cloud computing，formal method，algebraic specification 

目□□录

1.引言

1.1 OpenStack简介

1.2 形式化方法简介

1.3 论文的主要工作

1.4 论文的组织

2.OpenStack概述

2.1 计算组件NOVA

2.2 存储组件SWIFT

2.3 镜像管理组件GLANCE

2.4 身份认证组件KEYSTONE

3.基于代数规约的OpenStack的描述

3.1 代数规约语言

3.2 请求与响应的基本框架

3.3 基于代数规约的NOVA描述

3.4 编辑工具

结束语

致谢

参考文献

附录

1.引言

1.1 OpenStack简介

OpenStack是由美国国家航空航天局和Rackspace合作研发的云平台管理的项目，以Apache许可证授权，并且是一个自由软件和开放源代码项目，由四大部件构成：计算组件NOVA，存储组件SWIFT，镜像管理组件GLANCE和身份认证组件KEYSTONE，这几个项目共同合作完成具体的工作。OpenStack项目的首要任务是简化云的部署过程并为其带来良好的可扩展性。作为一个云平台管理的项目，它的作用旨在为公共及私有云的建设与管理提供软件，帮助服务商和企业内部实现类似于 Amazon EC2 和 S3 的云基础架构服务(Infrastructure as a Service, IaaS)。

OpenStack使用Python编程语言编写，整合Tornado网页服务器、Nebula运算平台，使用Twisted软件框架，遵循Open Virtualization Format、AMQP、SQLAlchemy等标准。OpenStack的虚拟机器软件支援包括：KVM、Xen、VirtualBox、QEMU、 LXC 等。它有两大优点，一是OpenStack自身的优势——开源性。二是众多企业和组织的参与开发，尤其是世界领军企业的加入，推动了OpenStack的高速成长。除了 Rackspace 和 NASA 的大力支持OpenStack外，包括 Dell、Citrix、 Cisco、 Canonical这些重量级公司对其也有贡献和支持，它的社区拥有超过130家企业及1350位开发者，这些机构与个人都将OpenStack作为基础设施即服务（简称IaaS）资源的通用前端。因此它的发展速度非常快，有取代另一个业界领先开源云平台 Eucalyptus 的态势。

1.2 形式化方法简介

    在实际应用中，由于使用自然语言描述不够准确、有二义性，为了准确地描述软件系统而提出了使用形式化方法。形式化方法在逻辑科学中是指分析、研究思维形式结构的方法。它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包含概念之间的联结,推理中则是各个命题之间的联结,抽取出它们共同的形式结构，再引入表达形式结构的符号语言,用符号与符号之间的联系表达命题或推理的形式结构。