基于PSMaude的弹性云系统形式化定量分析" - 沙特国王大学学报

制作和主办：Elsevier沙特国王大学学报基于PSMaude的弹性云系统形式化定量分析Chafia BouanakaRai，Esma Maatougui，Faiza Belala，Nadia ZeghibLIRE实验室，君士坦丁大学2-Abdelhamid Mehri，君士坦丁，阿尔及利亚阿提奇莱因福奥文章历史记录：收到2019年2019年10月23日修订2019年11月14日接受在线发售2019年保留字：云计算弹性形式方法PSMaude定量验证A B S T R A C T云计算及其各种扩展是一种重要的IT演进，旨在提供具有高效资源使用的按需IT服务，但仍确保服务可用性和服务质量（QoS）。资源弹性是一个有效的功能来处理这些问题，它提供了快速调整部署的资源容量，根据时变的工作负载，以满足预期的QoS要求的能力。然而，仅依赖于服务提供商策略作为水平和垂直弹性似乎不足以确保QoS要求，因为弹性云系统（ECS）中的资源使用模式本质上是不确定的。这在选择要相对于QoS参数应用的弹性策略时造成困难在本文中，我们提供了解决方案的挑战任务的管理ECS量化的不确定性的基础上的QoS参数。因此，我们定义了一个正式的模型来指定云系统的结构和它的动态质量驱动的弹性策略。此外，定量分析，以评估所提出的模型的QoS参数的有效性。©2019作者制作和主办：Elsevier B.V.代表沙特国王大学这是一CC BY-NC-ND许可下的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。内容1.导言. 3882.相关工作。........................................................................................................................................................................................................................................................ 3882.1.建模方法3882.2.概率分析方法3892.3.比较研究3893.激励性实例3904.第391条建议4.1.提案概述4.2.用于弹性云系统建模的QoS-Cloud 3915.QoS-Cloud正式建模3925.1.PSMaude：概述3935.2.QoS-云弹性策略编码3935.2.1.服务/虚拟机复制的重写规则*通讯作者。电 子 邮 件 地 址 ： chafia. univ-constantine2.dz （ C.Bouanaka ） ， esma.maatougui@univ-constantine2.dz（E.Maatougui），faiza.belala@univ-constantine2. dz（F. Belala），nadia. univ-constantine2.dz（N. Zeghib）。沙特国王大学负责同行审查https://doi.org/10.1016/j.jksuci.2019.11.0081319-1578/©2019作者。制作和主办：Elsevier B.V.代表沙特国王大学这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。可在ScienceDirect上获得目录列表沙特国王大学学报-杂志首页：www.sciencedirect.com388C. Bouanaka等人/沙特国王大学学报5.2.2.服务/虚拟机整合的重写规则5.2.3.VM迁移的重写规则5.3.弹性策略选择器规范3935.4.创建场景3946.QoS-云定量分析3947.结论395参考文献3971. 介绍云计算及其各种扩展是一种重要的IT发展，倾向于合理利用资源。Johnson等人，在（Johnson等人，2011），考虑到：“云系统最吸引人的特征是它们能够根据资源需求随时间的变化，在细粒度的时间间隔上动态地向上或向下扩展资源”。此功能通过资源弹性的主要概念来确保;根据工作负载的变化来放大或缩小，以保持QoS参数。从资源提供商的角度来看，弹性特征确保更好的资源使用和更多的节能（Shen等人，2011）;它还允许同时为多个用户提供服务（Ai，2016）。因此，它实现了有效的资源利用，降低了服务交付成本。从最终用户的角度来看，弹性特性避免了资源的不充分提供和系统性能的退化（Galante等人，2012年），从而实现成本降低;即按需消费，同时保障资源可用性。虽然云服务所需的资源是有限的，并在设计时静态确定，但工作负载可能会随着时间的推移而变化，有时会以不可预测的方式变化。这通常会导致云基础设施过载或卸载，从而对QoS级别和云服务交付成本造成致命后果。在此背景下，弹性管理机制面临着云系统的有效模型的增长和采用的多重障碍一个主要问题是要应用的弹性策略的非确定性选择，因为云系统结构相对于QoS参数的快速和动态调整并不总是明显的。此外，弹性云系统中的资源使用模式本质上是固有的概率性的，并且涉及潜在的未知或非确定性因素（Johnson等人， 2011年）。因此，非决定论出现在两个不同的层面：- 在给定的上下文中启用各种形式的弹性策略（复制、整合和资源迁移）- 当需要动态重新配置以确保弹性属性时，可以使用相同性质的几个资源。因此，采用定量分析方法来解决弹性云系统（ECS）中出现的不确定性是非常合适的。目前的工作的主要目标是提出一个概率的形式化模型来指定云系统和分析弹性策略的有效性相对于QoS参数。该模型提供了必要的机制来量化的基础上的弹性战略，成本和资源使用的不确定性。具体地说，该模型允许指定云系统的结构和它的动态质量驱动的弹性策略，根据QoS参数变化的连续分析，通过按比例放大/缩小。本文直接建立在Bouanaka等人，2018年，通过三个扩展：(1) 本文对弹性云系统规范和分析的形式化模型进行了比较研究(2) 一种设计方法被定义为模型质量驱动的ECS。(3) 定义了一个概念领域模型来帮助软件设计人员。为了实现上述扩展，我们结合Meta建模技术和形式化方法来设计，指定和分析ECS。PSMaude（Bentea和Olveczky，2012）构成了所提出的方法的语义基础，其中云资源类型被描述为类的层次结构，并且弹性策略被定义为一组概率重写规则。每个重写规则的权重与其适用性概率是动态确定的基础上，相应的弹性策略成本。此外，PSMaude策略被用来量化的非确定性，在选择适当的弹性策略，以确保所需的QoS相对于实际的工作负载表示的资源使用方面。这确保了有效的资源利用率，并通过在实际部署的云资源上对请求进行负载平衡来提高响应时间所提出的模型的有效性进行了验证，通过定量分析的努力进行管理资源弹性。本文的其余部分组织如下。第2节介绍了以前发表的弹性云系统建模和分析的基本研究工作。第3节简要回顾了拟采用的语义基础。第4节通过机票预订示例强调了管理ECS时面临的主要问题。第5节介绍了我们的建模方法的ECSs，连同相关的基于模型的语义。 第6节将正式的基于PSM的语义与ECS相关联。第7节通过定量分析技术来验证所提出的模型的有效性。第8章把纸包2. 相关工作目前，一些研究工作涉及的形式化建模和分析的ECS。它们根据不同的维度彼此不同：支持弹性的形式，弹性动作目标，决策中采用的策略，主要是形式验证目标（验证或分析所提出的模型）。在下文中，我们考虑两类方法：那些只考虑正式建模和验证的ECSs，和那些关心他们的概率分析。2.1. 建模方法作者在（Amziani等人，2013）提出了一个基于Petri网的框架来建模和评估基于服务的业务流程（SBP）的弹性行为。该框架定义了一个控制器，通过监控部署的 该方法在Amziani等人， 2013）来考虑基于有状态服务的业务流程。基于该模型，并使用开放云计算接口（OCCI）标准，C. Bouanaka等人/沙特国王大学学报389迄今为止，在（Amziani等人， 2015年）。Dustdar等人（2015）提出了一种开发ECS的方法，并提出了一种正式的方法，允许云提供商规范其系统的理想/不理想行为。基于时态正则表达式（TRE），他们的方法允许将工作负载波动、性能和资源分配指定为时态表达式。Sahli等人（2017）提出了一种通用和详尽的形式化方法，基于双图反应系统（Milner，2006），简称BRS和Maude（Clavel等人，2016年）。ECS的结构由三种类型的BRS定义：前端、后端和弹性控制器。弹性模式（水平，垂直和迁移）是由一组参数反应规则定义的。通过使用Maude模型检查器验证其响应工作负载变化的放大/缩小能力，对他们的模型进行了2.2. 概率分析方法Naskos等人（2014年）提出了一种具体的方法，在应用弹性策略的同时使用决策的连续定量验证，以使其更加可靠。该方法将聚类和形状变换作为唯一的弹性策略，即，其关注的是动态地修改虚拟机的数量，目的是优化效用函数。它是基于一个可扩展的系统，自动生成和实例化的MDP（马尔可夫决策过程）模型。构造策略的弹性决策是通过概率模型检查PRISM。每个转换或弹性决策由通过修改活动虚拟机的量的可能的放大/缩小组成，并且由MDP模型中的选择的弹性动作概率加权。始终选择权重最大的过渡。Konstanteli等人（2011）考虑了使用概率方法优化云虚拟化物理资源上的弹性服务分配的问题，以减少由于弹性原因而不必要的物理资源的数量，同时仍然保证服务可用性。由此产生的概率优化解决方案旨在建立一个适当的妥协，以实现公司设定的目标。这种验证的输出是一组接受的交付，以及对部署在所选物理主机上的每个服务组件所需的计算量的在通用代数建模系统（GAMS）数学建模软件上对问题进行了跟踪，并对供应商的实际参数进行了求解。作者（Konstanteli等人，2014年）提出了在联合云计算环境中找到最佳服务分布的问题。基于概率方法，重点研究了弹性工作负载，以解决由于弹性原因而分配补充资源的问题。所得到的服务分布旨在保证服务可用性。他们的方法是基于预测模型的存在，能够在监控历史数据的基础上警告云资源的使用。事实上，这些模型以在虚拟化环境中执行服务期间需要满足的资源需求的概率分布的形式产生作者已经开发了一个近似算法，rithm的启发式方法的基础上，产生接近最优的结果。启发式方法的目的是获得每个服务的组件的所有有效组合，并根据已利用资源的总容量和存储分配的成本计算效益此外，该方法确保了资源分配，最大限度地提高效益，降低成本。Bersani等人（2014）提出了一种基于时间约束线性时间逻辑（CLTL）的方法来指定和分析ECS。CLTL特别用于表征云系统中的资源管理、弹性和QoS属性。作者建立了一个初步的评估，以确定是否提出的属性是可验证的执行跟踪使用Zot;验证工具集的基础上SAT（可满足性）和SMT（可满足性模理论）。通过执行跟踪，验证了ECS的三个主要特性：资源破坏、可塑性和冷却时间，并对ECS的资源使用情况（执行时间和内存）进行了评估。Khebbeb等人（2019）提出了一种建模和验证方法来指定和分析弹性云系统。他们的方法是基于双图反应系统来指定系统的结构和弹性行为，Maude来实现和验证模型的正确性，以及排队论来分析弹性策略的性能。2.3. 比较研究本文对弹性云模拟和分析方面的一些重要工作进行了比较研究，总结见表1。四个主要特点被认为是：潜在的形式主义，考虑弹性形式，模型执行，和形式分析的QoS属性。第一类工程涉及的正式建模的ECS与部分或全部支付的弹性模式。验证过程仅限于模型确认，并考虑ECS分析。在（Amziani等人，2013年）仅限于特定云级别的水平缩放方法。此外，基于云的系统的架构细节被忽略，其中涵盖了主动和被动的弹性策略。此外，所提出的模型不是通用的，不能代表与弹性的基于云的系统相关的所有方面在（Dustdar等人，2015）仅考虑了水平弹性，特别是基础设施级别的虚拟机创建/销毁。它缺乏体系结构细节，也没有经过验证。即使在（Sahli et al.，2017）考虑了水平和垂直弹性，基于BRS的规范表1弹性云系模式的比较方法形式主义弹性策略模型执行分析（Amziani等人， 2013年度）Petri网水平--（Dustdar等人，（2015年）TRE水平--（Sahli等人，（2017年）BRS-Maude水平/垂直--（Naskos等人， 2014年度）MDP水平++（Konstanteli等人，（2011年）优化技术水平-+（Konstanteli等人， 2014年度）优化技术资源分配++（Bersani等人， 2014年度）-水平-+（Khebbeb等人， 2019年度）BRS-Maude-BRS理论水平/垂直++390C. Bouanaka等人/沙特国王大学学报由于缺乏用于BRS的工具和模型检查器通过使用Maude语义定义的第二个模型执行模型验证。第二类工作提出了各种形式主义来分析弹性云系统，但追求不同的目标，如（Naskos等人，2014年），其中作者对集群扩张和形状转移感兴趣，并考虑了水平弹性，但仅在基础设施层面。这种方法是特定的，不能推广到所有的弹性模式。此外，部分支持基于云的系统的架构细节。所提出的方法的一个主要缺点是详尽地定义和枚举系统的所有可能状态，这并不总是可行的，特别是在系统包含非常大量的虚拟机的情况下。在（Konstanteli）中提出的方法的主要缺点是例如，2011年，它是不可执行的。此外，通常不容易使用数学公式来表达系统虽然作者在（Konstanteli等人，2014）提出了一种近似算法，该算法定义了资源分配的最优组合以最大化收益和成本，但是启发式方法的许多弱点将被强调。所获得的结果紧密地依赖于所定义的物理学，这些物理学是变化的，并且与定义它们的专家的技能此外，启发式方法的有效性和可靠性有限，深受不赞成。Bersani等人（2014）仅通过在基础结构级别创建/销毁虚拟机实例来考虑水平弹性。该方法没有为弹性云系统提出一个明确的模型。它主要采用模拟技术来观察系统行为并生成执行轨迹，其中转换标记有执行时间和内存。然后，分析生成的执行跟踪，以评估资源垃圾，可塑性和冷却。Khebbeb等人（2019）根据工作量变化评估和分析了弹性策略。通过分析，作者试图识别和选择最有针对性的弹性策略。他们还提出了一种机制来组合不同的跨层弹性策略，以保证不同的高级策略。我们在这里强调，验证所提出的方法是很难理解和实现，因为它结合了三个不同的正式模型。此外，没有考虑模型转换的正确性。我们的工作属于第二类的方法，提出了一个正式的模型来分析环境控制系统的有效性。它以反应方式考虑水平弹性和虚拟机迁移策略。建议的主要优点形式模型的一个重要特点是它是可执行的，因此，允许系统分析。此外，由于基于PSMaude语义的声明式和通用风格，该模型不像基于MDP的模型那样详尽，后者受到云资源量的限制。3. 激励的例子在整个例子中，我们确定遇到的主要问题，同时设计有效的ECS，约束，以适应工作负载的波动，以确保特定的QoS属性。我们考虑一个预订系统（TicketBooking），灵感来自（Rong，2014）。该系统部署在云基础设施上（见图1），由两个服务组成：用于预订机票的 AirTicketBooking 服务（ S1 ）和用于预订船票的BoatTicketBooking服务（S2）我们假设有四个用户A1、A2、A3和B正在使用TicketBooking系统，A1和B通过请求S1预订机票，而A2实际上通过S2预订船票。这两个服务部署在同一个物理服务器（Server1）上，但分别运行在两个不同的虚拟机（VM1和VM2）上。Server2和Server3实际上分别包含VM3和VM4虚拟机我们认为TicketBooking系统表现出三种形式的弹性：资源复制：包括复制资源（服务、虚拟机）以应对工作负载的扩展。如果给定VM的服务S达到它可以同时处理的最大请求数量，则自动创建S的新副本并将其添加到同一VM。每当VM变得饱和并且不再能够承载新服务或其他服务请求时，就会创建新的VM并将其配置在同一服务器上。服务整合：它是复制操作的双重操作，每当工作负载缩减时它包括删除服务和VM的无用副本。服务/虚拟机迁移：这种情况出现在服务器过载但包含未饱和的VM时;它能够执行新请求。因此，可以将VM迁移到负载较低的服务器，以确保负载平衡并缩短服务响应时间。我们假设虚拟机VM1实际上是过载的，并且它不再能够处理对机票服务S1的更多请求。有两种可能的解决方案：图1.一、机票预订系统初始配置。●●●●●C. Bouanaka等人/沙特国王大学学报391复制VM1或在负载较少的虚拟机上重新部署（迁移）请求的服务因此，如果选择迁移策略，则在选择弹性策略和目的地服务器时出现不确定性。此外，从成本和绩效有效性的角度来看，一些弹性策略比其他策略更有针对性。因此，在重新配置机票预订系统时出现了两个主要挑战：(1) 要应用的弹性策略和底层云资源的不确定性选择(2) 在某些条件下，一些弹性策略比其他服务提供QoS参数更可靠。为了解决上述挑战，我们通过将累积成本属性与每个云资源相关联来量化非确定性以获得全概率模型然后，进行弹性策略的动态加权以选择最合适的策略。这种方法能够分析ECS的QoS要求，以衡量系统的有效性。4. 所提出的方法弹性属性的原理是确保提供必要和足够的资源，使得即使工作负载按比例增加或减少，云服务也能继续平稳运行，并避免资源利用不足或过度利用（Galante等人，2012年）。各种形式的弹性属性可以使用三种基本方法来提供：资源复制、资源整合和资源迁移。因此，两个或更多个弹性策略可以同时被候选以管理具有各种成本的工作负载波动，并且因此引起概率性和非确定性行为。在下文中，我们提出了一种结合模型驱动工程（MDE）和形式化方法来管理和分析弹性云系统的方法MDE通过关注软件系统的结构语义和静态另一方面，形式化的方法使信号-对程序行为表征和理解的重要贡献（Ke等人，2012年）。它们提供必要的概念和验证机制来定义软件系统的语义或行为并对其进行分析。4.1. 提案概述所提出的分析ECS的方法由两个主要阶段组成（见图2）：建模阶段和执行/分析阶段。基于元建模技术，建模阶段允许定义弹性云结构及其动态。它由三个步骤组成。第一种方法是通过识别云系统的相关架构元素和相应的相互关系来描述云系统的结构。第二步旨在识别ECS参数（要维护的QoS参数和相应的执行上下文）。第三步定义基础ECS的结构动力学。它规定了重新配置模式，在弹性策略方面，主要是加权它们与QoS参数和定义的上下文参数，帮助选择适当的弹性策略。为了在前三个步骤中帮助设计人员，我们定义了一个概念性的领域模型（见图3），称为QoS云，稍后将详细介绍。基于PSMaude，执行和分析阶段将行为语义与第一阶段中设计的模型相关联，以便执行和分析它们以测量弹性策略的成本效益。它主要定义了加权弹性策略的操作语义，以通过弹性策略选择器的形式化来使所考虑的云系统适应关于QoS参数的工作负载变化。在下文中，详细介绍了我们方法的不同阶段。4.2. 用于弹性云系统建模的我们为质量驱动的ECS定义了一个概念域模型（见图3）。它包括三个主要元素：云结构，弹性策略和弹性参数。图二. 提出的建模方法。392C. Bouanaka等人/沙特国王大学学报图三. QoS云概念域模型。云系统结构是云系统的基础层，它定义了云系统的主要组成部分及其层次关系。它由一组计算资源（例如，服务器、虚拟机、服务等）组成。分布在多个地理分布的计算站点上，称为数据中心。这些不同的资源被提供为客户根据他们的需求而要求的按需服务数据中心是包含服务提供商的组成设备的物理站点。它还配备了负载均衡器;该设备不仅负责在各个服务器之间分配工作负载，还负责分配必要和足够的资源来执行客户请求。每个物理服务器托管一组虚拟机，在这些虚拟机上部署云服务云服务表示由服务提供商提供的各种服务，如文本处理、邮件系统、虚拟服务器、存储等。云系统结构的弹性模式由众所周知的弹性策略（复制、整合和迁移）根据工作负载波动来定义。弹性参数：每个云资源都有一组QoS属性，稍后可以利用这些属性来量化非确定性。我们认为这里的资源管理成本作为QoS参数和资源的实际使用的弹性适用性上下文。我们强调，图2的弹性策略选择器被定义为用已经定义的弹性策略、QoS参数和实际上下文参数化的策略集合。它以通用和系统独立的方式定义。因此，它不需要在概念领域模型中表示。5. QoS-云形式化建模所提出的形式化方法基于一组映射规则（参见表2），其定义了所提出的QoS-云域模型概念与PSMaude概念之间的对应关系弹性云系统的结构方面被映射到一组明智定义的类，弹性策略的概率重写规则和弹性选择器机制的一组PSMaude策略。为了反映QoS-Cloud模型的层次结构，避免代数项的结构扁平化，我们采用了面向对象的方法。将云系统元素识别为对象以及它们的上下文、属性和操作，可以显著促进模型的设计和可理解性。基于PSMaude的操作语义的主要目标是：- 通过弹性策略验证弹性云系统的行为（参见第5.2）。- 获得可执行的规范（参见第5.2）。在介绍所提出的形式化模型之前，我们需要简要回顾一下要采用的语义基础;例如PSMaude。表2QoS云概念与PSMaude之间的对应关系。QoS-云概念PSMaude概念结构部件用户类用户|连接：布尔。服务舱服务|Nbr客户端：Nat，类型：Qid，客户端：OidList，成本：Nat。虚拟机Vm类|Nbr服务：Nat，Nbr请求：Nat，服务：OidList，状态：State，成本：Nat。服务器级服务器|N b r V m ：Nat，NbrReq：Nat，vms：OidList，state：State，Cost：Nat。负载平衡器类LoadBalancer| 连接：布尔。数据中心类DataCentre|负载均衡器：Oid，服务器：OidList。动态部分弹性战略可能重写规则弹性策略选择器PSMaude策略●●●C. Bouanaka等人/沙特国王大学学报3935.1. PSMaude：概述Maude是一种基于重写逻辑（Meseguer，1993）的语言，由于反射特性，它已经使用Maude语法本身在各个方向上扩展;就像完整的Maude （Duran和Meseguer，1999 ），Mobile-Maude（Duran等人，2000），以及最近的PSMaude（Bentea和Olveczky，2012）。PSMaude是Maude的概率扩展，它提供了一种表达概率策略语言来量化概率重写理论中的非确定性。它允许用户在基础模型之上指定不同的概率策略，然后可以模拟和统计模型检查。具体地，该思想包括通过向规则匹配分配权重（基于规则名称、规则适用性上下文和替换）来向非确定性转换分配概率，所述规则匹配稍后被归一化为区间上的值（Johnson等人，2011年）。加权规则的选择和执行由PSMaude策略控制。概率策略由三部分组成：规则策略、上下文定义和替换策略。正式定义见（Bentea和Olveczky，2012年）。规则策略定义了在每个步骤应用某个重写规则的相对可能性，上下文定义使得某些组件比其它组件更可能参与某个规则应用替换策略通过使规则应用中涉及的组件的相对可能性能够根据实际上下文具有不同的角色来指定所选组件的某些角色比其它角色更可能。我们强调，PSMaude扩展Maude通过添加必要的支持指定概率重写规则和概率策略。此外，它还提供了一组概率重写命令和一个统计PCTL模型检查器，用于分析由概率策略控制的概率重写理论。5.2. QoS-云弹性策略编码QoS云的动态部分是通过一组重写规则来指定的，这些规则在资源弹性方面表达了云结构上的本地变化，同时保留了初始架构约束。5.2.1. 服务/虚拟机复制服务复制重写规则允许在给定服务不能处理其他用户请求的情况下添加该服务如果VM未饱和并且包含所请求的服务，则应用此方法Replcation-of-VMrewrite规则定义为在工作负载向上扩展并且实际部署在服务器上的所有VM都饱和时添加新的VM。此重写规则将新VM的成本添加到服务器的实际成本中，创建新VM并将其插入服务器的VM列表中。5.2.2. 重写规则 服务/虚拟机整合服务整合规则允许在工作负载缩减时销毁服务/VM的无用（空）副本。规则的适用性取决于服务的其他副本的存在。此重写规则的效果是减少实际部署在VM上的服务数量并销毁无用的服务。的虚拟机整合重写规则类似于服务整合（Consolidation-of-service），人们期望它在无用的虚拟机上运行而不是服务。5.2.3. VM迁移每当接收到服务请求时都会触发此规则;相关服务和包含它的VM能够处理它，但服务器已饱和。规则执行包括通过累计VM迁移的成本和增加VM数量来更新目标服务器成本。用户将被添加到服务和VM的客户端5.3. 弹性策略选择器规范重写规则将添加服务实例的成本累积到VM的成本中，增加实际部署在该VM中的服务的数量，并将创建的服务添加到VM的服务列表中。在给定上下文中选择和执行弹性重写规则的过程由弹性策略选择器控制。策略选择器的主要作用是解决潜在的不确定性，●●●394C. Bouanaka等人/沙特国王大学学报ð Þ云系统结构它由一组PSMaude参数化策略组成，这些策略使得能够选择在给定上下文中应用的最合适的弹性策略。这些策略用QoS参数（动态评估）和实际上下文（表示资源实际利用率）进行参数化。弹性策略选择准则是基于弹性策略权重来选择合适的弹性策略，解决不确定性问题。每个重写规则，代表一个弹性策略，加权的适用性概率是成反比的累积成本。为了计算云资源的累积使用和成本，相应的类定义扩展了一些属性（表2），如下所示：服务资源在NbrClient和Clients属性中累积其实际使用情况，分别指示实际请求服务的客户的数量和列表。服务成本通过成本属性定义。VM 资 源 ： 资 源 工 作 负 载 通 过 NbrSer- vices 和 Services 来 定 义 ，NbrSer- vices和Services分别表示实际部署在所考虑的VM上的服务的数量和列表。 资源使用通过NbrReq定义，NbrReq累积实际可用服务的请求数量。最后，VM累积成本（成本属性）初始化为在物理服务器上部署新VM的成本，然后累积在VM上部署新服务的成本。服务器资源：通过所有实际部署的VM的NbrReq和Cost属性定义资源使用和成本参数。弹性策略的非确定性选择通过策略RuleStrat（见6.3节）来量化，该策略动态地影响每个重写规则的权重。我们还定义了所有重写规则所共有的上下文和替换策略。我们认为在这里的弹性规则，是受非确定性的复制和迁移规则。我们分配一个权重的上下文策略CtxStrat表示选择和应用复制的服务规则的概率。权重与创建服务的新实例的成本成反比。替换策略SubStrat是一致的，因为存在唯一的对应替换。用于复制VM的上下文和替换策略以类似的方式定义。可以应用Migrate-VM重写规则的上下文取决于与VM迁移成本相关联的概率与VM复制相反，目标服务器的选择是不确定的。因此，替换策略是不统一的，并且负责选择实际上负载较小的服务器，该服务器通过影响替换策略的权重（1/（XY +大小（XCL）来识别，其中XCL是所考虑的服务器，XY是请求的数量。这样的权重与服务器上实际部署的VM的总和和请求的数量上下文和替换的策略对于其余规则是统一的，并且在任何状态下都是随机选择的（随机）5.4. 创建方案对于TicketBooking系统，我们权衡了各种弹性重写规则与相应的弹性策略成本。根据所启用的重写规则中的每个重写规则的重要性来分配权重。通常，频繁请求的重写规则是分配服务，因为云系统散布有大量资源。因此，我们将最高权重（值为100）影响到分配服务重写规则。权重为10会影响到复制服务重写规则，以处理部署新服务或创建现有服务的新实例其余的重写规则很少被请求，因此权重为1。例如，从一个物理服务器到另一个物理服务器的虚拟机迁移很少应用，因为它太昂贵了。对各种弹性重写规则进行加权的策略是应用于实际配置CF的每个可能状态;它量化了要在每个执行阶段应用的规则的不确定性选择。我们认为虚拟机迁移的情况下，突出两个层次的非确定性是如何我们认为客户端A2实际上正在请求部署在VM 1上的AirTicketBooking服务S1;尚未饱和。但是服务器1不再能够处理新请求，因为请求的数量达到了它的阈值，100个同时请求。在这种情况下，VM迁移策略由弹性策略选择，并应用于将VM 1移动到负载较低的服务器。目的地服务器选择机制是不确定的，因为两个服务器（分别具有60个和26个同时请求的服务器2和服务器3）实际上是接收VM 1的潜在候选者;选择服务器3是因为它是负载较轻的一个（参见图2）。 4）.6. QoS-云定量分析定量分析的主要目的是评估所提出的形式化模型的有效性。我们分析在处理客户请求时隐含的资源使用率，或者弹性云系统为满足客户（服务请求）而提供的工作量。工作量是根据虚拟机（VM）的工作负载计算的;实际上包含所需的服务并根据以下公式在给定服务器（S工作量初始工作量虚拟机总和工作量SUMService出于效率原因，不是计算重写引擎要达到的每个中间状态的努力函数，如上面定义的，而是计算累积努力并将努力函数effe作为项包括在系统状态中。然后，在预测模块CLOUD-PRED中定义参数化的预测clustiveCloud。如果累积工作量不超过如下定义的阈值K，则谓词certaintiveCloud在给定状态S●●●C. Bouanaka等人/沙特国王大学学报395≈半]¼ð Þ ð ðÞ图四、服务器选择和VM迁移。以更少的成本获得更多的资源，云服务的QoS。7. 结论效率谓词由K和P参数化;阈值K表示要执行以管理弹性云系统的重写规则的最大量，置信度P表示条件成立的概率。为了确保效率属性，我们倾向于最小化K并最大化P（1）。我们现在可以检查系统是否验证了效率属性，如果云系统的累积工作量在分配服务时从未超过具有置信度P（条件成立的概率）的阈值K，无论何时验证效率属性，它都确保云服务的期望QoS，即，最小化弹性管理工作：努力SUM Service S=SUM 请求虚拟机，降低弹性管理成本甚至工作量。对于TicketBooking系统，深入的分析表明，所提出的模型是有效的，如果阈值K的范围在区间5; 100。在下文中，我们提出了两种情况，对于K = 5和K = 100。情景1：K = 5我们验证系统的有效性进行以下PTCL属性。 分析结果，如图所示。 5，表明TicketBooking系统能够在94%的情况下以K = 5的努力分配服务。使用CloudStrat实现CloudConfj<$P≥0：9½G效果情景2：K = 100现在让我们假设系统达到峰值负载时段，并且实际上落入服务器池不足以提供期望的QoS的状态，并且成本很高。我们尝试检查努力不超过最大阈值100。图6显示了分析结果，其中TicketBooking系统在此峰值负载期间分配服务的工作量超过100，因此需要提供基于云的弹性系统的出现导致了一类新的自主系统，其中资源弹性是关键的设计原则。弹性属性表示基于云的系统能够通过供应和释放资源以使得所提供的资源符合系统需求来动态地适应工作负载波动这种资源消耗的动态自适应特性非常有吸引力，因为它为弹性云系统提供了自主调整资源消耗的能力，以保持所需的服务质量，同时最大限度地降低运营成本。然而，管理云系统，特别是实现弹性策略仍然是一个挑战。一个主要问题是要应用的弹性策略的非确定性选择，因为云系统结构相对于QoS参数的快速和动态调整并不总是明显的。另外，弹性云系统中的资源使用模式本质上是固有概率性的，并且涉及潜在的未知或非确定性因素（Johnson等人，2011年）。针对上述问题，提出了一种弹性云系统管理的概率形式化模型.该模型具有以下特点。首先，它提供了一个正式的框架，基于扩展的Maude，即PSMaude，指定弹性云系统。定义了弹性云系统的PSMaude语义，并建立了基于模型的语义和PSMaude语义之间的对应关系。规范步骤包括通过识别所考虑的系统结构、要执行的弹性策略集和在管理弹性时要满足的质量属性来实例化弹性云系统Meta模型。其次，所提出的模型允许通过量化弹性策略成本和资源使用来解决在选择弹性策略时出现的非确定性问题，以实现将累积成本属性与每个云资源相关联的全概率模型。然后，对弹性策略进行动态加权，我们的模型的第三个有趣的特点是它能够执行弹性云系统的概率分析，以评估396C. Bouanaka等人/沙特国王大学学报图五.评估AirTicketBooking系统的效率。见图6。 QoS参数违规。C. Bouanaka等人/沙特国王大学学报397云系统提供的服务，以确保服务的可用性。对该模型的定量分析表明，弹性云系统的服务质量是可以接受的。分析了资源弹性成本和资源使用随时间的波动，以确保资源使用的最大累积成本不超过预定义的阈值。此外，还考虑了资源负载平衡作为未来的工作，我们计划采用模型转换技术，自动生成正式规范的领域概念模型的实例，并开发一个图形化的工具来实现所提出的框架。该工具将被指定为帮助设计人员建模和分析一般的自适应系统，特别是弹性云系统在这个目标中，我们将利用建模工具，即XText和Xtend，定义一个领域特定的语言，弹性云系统。作为长期目标，我们打算考虑弹性云系统的更多引用Sahli，Hamza，Hameurlain，Nabil，Belala，Faiza，2017.“用于指定基于云的弹性系统及其行为的双图模型”，国际并行杂志。艾默分发。系统（IJPEDS）32（6），593-616。艾，W.，Li，K.，Lan，S.，张福，Mei，J.，Li，K.，Buyya河，2016. ‘‘On ElasticityMeasurement in Cloud Computing”, ScientificAmziani，M.，Belaïd，D.，Tata，S.，Melliti，T.，2015.一种自主的方法来管理云中业务流程的弹性。FUT. Generat. Comput.系统50，49- 61。Amziani，M.，Melliti，T.，Tata，S.，2013.云环境下基于状态服务的业务流程弹性的形式化建模与评估。在OTM Confederated International Conferences“On the Move toMeaningful Internet Systems”中，Springer，2013，pp. 21比38Amziani，M.，Klai K.Melliti，T.，和Tata，S.，2013年。 573-580。Galante，G.，德博纳湖CE，2012.云计算弹性研究综述。第五届IEEE/ACM公用事业和云计算国际会议论文集，第10页。263-270。本泰亚湖Olveczky，P.C.，2012年。概率重写理论的概率策略语言及其在云计算中的应用在：WADT第77-94页。Bersani，M.，Bianculli，D.，Dustdar，S.，Gambi，A.，Ghezzi，A.，Krstic，S.，2014年。基于云的弹性系统性质的形式化。在第六届面向服务和云系统工程原理国际研讨会上，ACM，pp。38比47Bouanaka角，Maatougui，E.，Belala，F.，Zeghib N.，2018.质量驱动的弹性云计算分析方法。在：第三届软件工程高级方面国际会议（ICAASE84比91Clavel，M.，Duran，F.，Eker，S.，Lincoln，P.，Martine-Oliet，N.，2016.参见：Maude手册（版本2.7.1）。SRIInternational.Duran，F