没有合适的资源?快使用搜索试试~ 我知道了~
分布式对象通信服务的可组合重写语义与保障机制
理论计算机科学电子笔记36(2000)网址:http://www.elsevier.nl/locate/entcs/volume36.html21页元对象的重写语义与可组合分布式服务1G. Denker和J. 梅塞盖计算机科学实验室Menlo Park,CA94025 USA电子邮件地址:denker@csl.sri.comC. 塔尔科特斯坦福大学计算机科学系Stanford University,CA94305美国电子邮件地址:clt@cs.stanford.edu摘要分布式对象之间的通信可能必须受到保护,以防止随机故障和恶意攻击;此外,通信的及时性可能是必不可少的或高度期望的。因此,一个分布式应用程序通常需要扩展通信服务,提供某种容错、保密或服务质量保证。理想情况下,这些服务应该以高度模块化和可动态组合的方式定义,以便在某些情况下可以通过组合来实现多个服务的组合保证,并且可以在运行时响应环境的变化而在应用程序中添加或删除要推理这种可组合通信服务的形式属性,首先需要给它们一个精确的语义。本文提出了一种用于分布式对象反射的“洋葱皮”模型的重写逻辑语义由于服务的正确行为取决于服务必须保护应用程序免受的恶意环境的类型,因此重写逻辑也应该用于指定此类恶意环境。服务保证则是对重写理论的联合所指定的行为的保证,这些重写理论指定了基本应用程序、服务和敌对环境。2000年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。梅塞格?塔尔科特?登克尔21介绍在分布式计算和通信软件中,人们对模块化和可组合的方法很感兴趣。特别是,因为安全性或容错性以及用于提高性能的服务实际上可能是跨分布式系统的代码的不同部分“硬连线”的,所以应该以更加模块化的方式来处理这些服务,使得它们可以被动态地添加到系统中,并且使得可以组合几个这样的服务以获得它们的组合益处。除了使系统更容易重用和适应的良好软件工程原因之外,模块化和可组合性在运行时也是至关重要的相反,它们应该在运行时动态地和有选择地安装在分布式系统的那些区域或域中,在这些区域或域中,需要它们来响应一些安全威胁、故障、提高性能的需要等。许多作者,在分布式计算和网络领域(例如,参见Agha的论文(引用如下)和[15,10,17]),以及形式方法的研究者(c.f.[24,26,21])提出了一些概念和解决方案来处理分布式服务的组合所带来的问题。“编织”的概念[14]也是一种可以用来处理其中一些问题的机制。也有一些关于模块化规范和推理的工作(见下文)。为了实现模块化和适应性,这些方法中的一些使用分布式面向对象的反射2,即重新编程通信和对象语义的能力创作所有这些方法都认识到,实现真正的模块化和可组合的分布式服务,并确保这些服务的组合具有良好的属性是非常微妙的目标。首先,一个令人满意的形式语义的意思是什么可组合的分布式服务尚未给出,也没有相应的方面,这样的组合被充分形式化。Chandy和Misra [5]提出了一个“可靠保证”的原则,用于处理 Abadi和Lamport [1]提出了一种使用假设/保证断言描述并发系统开放组件的方法[13]。然而,上述方法解决了可能被称为系统的并行组合的问题。我们不知道任何系统的方法,以正式的语义组成的服务,在一个相对的和分层的方式。本文提出了一种语义化的方法来精确化指称1 支持 通过 DARPA 通过 罗马 实验室 合同 F30602-97-C-0312,由DARPA和NASA通过合同NAS 2 -98073,由海军研究合同N 00014 -99-C-0198的办公室,以及由国家科学基金会资助CCR-9505960和CCR- 9633363和CCR-9900334。2我们将在本文中讨论的分布式面向对象反射的具体特征纸将不需要重写逻辑反射的全部力量[7,8];它们实际上可以在对象级别上表达,而不需要使用重写逻辑元级别特征。梅塞格?塔尔科特?登克尔3§§§§§§§§分布式面向对象系统中可组合服务的概念。我们的方法是基于重写逻辑[19]提供的分布式面向对象系统的可执行形式语义,并显式地解决了具有一个真正模块化的服务概念。我们提出的形式化模型似乎不仅对形式化分析和符号模拟很有前途,而且作为一个语义基础,在此基础上可以开发定理证明方法来形式化地验证服务及其组成的重要属性。Agha和他的合作者[3,12,29,11,2,28,4]提出了一种参与者反射的洋葱皮模型,本文在重写逻辑的框架下对该模型进行了推广和形式化。计划本文的其余部分组织如下。在本节的其余部分,我们非正式地讨论洋葱皮模型(1.1),并用一个简单的例子(1.2)来说明它,以促进本文主体中这些思想的推广和形式化。在第二章中,我们给出了并发元对象的重写语义。我们首先回顾并发对象的重写逻辑在2.2中,我们描述了元对象的表示和塔中元对象层的封装。最后,我们展示了如何将并发对象转换为等价的单对象塔,然后适合安装额外的元层(2.3)。在第三章中,我们提出了一个案例研究来说明我们的元对象语义。我们使用基于重写逻辑的语言Maude来指定我们的例子。该案例研究采用了加密服务和客户端-服务器应用程序,其中服务器可以创建帮助对象并将请求委托给它们。在第4章中,我们解释了我们在可组合服务方面的工作如何包括对安装这些服务的敌对环境的正式规范。结论和未来的工作在§5中讨论。1.1Actor反射的洋葱皮模型洋葱皮模型的目标是反映通信(发送和接收消息)和参与者创建的基本参与者原语,同时保持参与者模型的响应能力和封装属性之间的平衡。在这个模型中,每个参与者都有一个元参与者来定义其原始动作的语义。例如,由基本参与者发送的消息成为对其元参与者的请求,以传输该消息。双重地,传递给参与者的消息由它的元参与者接收,使它能够控制接收语义。如果没有明确的元操作者行为被定义,底层系统语义提供了一个默认的元操作者行为。演员在一起梅塞格?塔尔科特?登克尔4请求一B它的元参与者在环境中看起来像一个普通的参与者,因此可以由另一个元级别参与者控制。这就产生了一层层的元层次,因此就有了“洋葱皮”的类比。一组参与者的分布式服务可以用元参与者层来表示,这些元参与者层进行协调以实现某些总体属性。正如Agha等人所提出的,洋葱皮模型为在开发和(动态地)调整开放分布式系统以满足变化的环境条件和要求中的关注点分离提供了概念基础。例如,应用功能、通信协议和安全要求以及故障/可靠性语义可以被单独地和模块化地视为独立层,从而提供可以以各种方式静态地或动态地组合的服务,以实现期望的整体行为。该模型已被用于支持许多高级声明性编程抽象,如同步器、激活器、实时同步器、参与者空间和抽象交互模式的协议。基于这些思想已经开发了几种原型语言[11,28,25]。1.2组合服务在洋葱皮架构中,服务的实现是通过在组成基本分布式应用程序的每个参与者之上组成一个或多个元参与者来实现的。元行动者通过提供适当的通信服务来调解基本行动者之间如果几个元参与者在一个基本参与者之上分层,则可以实现组合的通信服务(例如,提供安全性和不需要基本参与者本身的组件或修改的知识。但是,当然,为了让元参与者正确地实现服务,可能需要基本参与者满足某些特定的接口或行为需求。为了说明如何使用这些机制,我们绘制了一个示例场景。考虑两个参与者A和B(图1),其中B提供客户端A请求的某些服务。答复图1.一、 A向B发送请求,B回复并可能改变内部状态。然而,假设敏感信息在A和B之间传输,并且通信介质不可信任。然后,为了保护信息,可以通过在A和B上安装加密器元角色来放置加密服务。这些元参与者负责加密传出消息和解密传入消息,而不进行任何更改梅塞格?塔尔科特?登克尔5请求一BB'在A和B中需要(图2)。加密消息请求一B加密器答复加密器图二.A和B之间的所有消息都由加密层加密和解密。这种可组合服务的方法还可以处理参与者创建的动态方面,包括在这样的新参与者上安装适当的Meta参与者。例如,假设上述情况的变体,其中参与者B可以将应答的计算委托给新参与者B',该新参与者B'是由B在接收到来自A的请求时创建的答复图3.第三章。 B将A的请求委托给B当然,如果只有A和B使用加密,而B'不使用加密,则会违反保密性。这个问题的一个简单解决方案是赋予任何加密元参与者在由他们的“基础”参与者创建的任何新参与者上安装另一个加密元参与者的能力。在我们的示例中这意味着B的加密器元动作者将向它从B接收的用于创建B'的对象创建信息添加加密消息请求一BB'加密器答复加密器加密器见图4。B'是在安装了加密服务的情况下创建的。B将A的请求委托给助手梅塞格?塔尔科特?登克尔6∅−→×2并发元对象我们简要介绍了分布式系统配置的重写逻辑模型,作为一个特别地,我们将重写逻辑对象模型[16,18,20]专门用于异步消息传递的情况。然后,我们引入元对象,它可以分层,形成塔,出现在他们的环境,类似于并发对象。2.1重写逻辑中的并发对象我们采用了[19]中重写理论对并发对象的处理。我们称这种理论为并发客体理论。面向对象系统的并发状态,通常称为配置,通常具有由对象和消息组成的多集结构。因此,我们可以将配置视为由二进制多集并运算符建立的,我们可以用空语法表示(即,并置)为:配置配置。(遵循mix-fix表示法的惯例,我们使用下划线““来表示参数位置。 证明了多集并算子对象和消息是单例多集配置(Object,MsgConfiguration),更复杂的配置是通过多集并从它们生成的<一个对象在给定的状态下被表示为一个术语CNOO:C|a1:v1,.,an:v nn,其中O是对象的名称或标识符,C是它的类,a i是对象的属性标识符,v i是对应的值。对象状态的所有属性-值对的集合对象的属性-值对的顺序是无关紧要的。特定的系统通过提供额外的操作和等式来公理化,例如,指定属性值和消息结构的数据操作一个配置的多集结构的结合性和交换性使它非常简洁。我们可以把它想象成一个通常,描述面向对象系统的动态的重写规则可以具有以下形式r(x<$):M1. . . MnO1:F1|att s 1.. . 单位:mm|atts m−→Oi1:FiJ1|att s Ji1.. . Oik:FiJk|atts Jik第一季第1集|attsJ1J. Qp:D p|阿茨JpjM1J.MQJ如果条件梅塞格?塔尔科特?登克尔7其中r是规则的标签,x是规则中的变量M是消息表达式,i1,...,i k是原始1,.,m,Cond是规则的条件3。也就是说,许多对象和消息可以聚集在一起并参与转换,其中可以创建一些新对象,可以销毁其他对象,并且其他对象可以改变它们的状态,并且其中可以创建一些新消息。 如果两个或多个对象出现在左边,我们称之为同步规则,因为它强制这些对象共同参与转换。 如果在左边只有一个对象,我们称之为异步规则。如果规则是异步的,只有一个对象和最多一条消息,则并发对象重写理论称为异步对象理论左手边。 此外,我们假设消息表达式具有O a M的形式,其中O是对象标识符,M是表示要传递的信息的项。我们把这种形式的消息称为消息包。在异步对象重写理论的上下文中,异步对象配置是对象和消息包的多集合2.2元对象和塔元对象是可组合的并发对象,它们实现分层对象的各个层,称为元对象塔。每一层都充当下面分层对象的元对象,解释来自下面一层的请求以发送消息并创建新对象,以及来自上面一层或环境的请求以传递消息。元对象塔的任何两个相邻层之间的通信是同步的。 这通过给予每个元对象四个消息列表来实现:用于向其上层(另一元对象或环境)发送消息和从其上层接收消息的出列表和入列表;以及用于与下层交互的上列表和下所有的元对象都属于MetaObject类的子类,MetaObject是一个具有五个不同属性的对象类:in,down,out,up,base。中的属性是传入消息的列表,表示要从上层或外部传递的消息属性down是要转发到下面一层的消息列表属性out是一个配置请求列表(即多组请求数据包),由用于消息传输和对象创建的传出请求属性up是一个配置请求的列表,这些请求将被转发到上面的层属性库是一个对象标识符,对应于堆栈底部的对象标识我们进一步要求元对象规则不显式地消费或创建配置元素。它们只能从输入和向上列表中删除项目,将项目放入输出和向下列表中,并修改其他属性。要与其他元对象或环境交互,3我们采用Maude约定,即规则中未更改或未使用的属性不需要提及。梅塞格?塔尔科特?登克尔8◦§§§元对象必须是元对象塔的一部分。一个元对象塔是一个结构的形式{\fn方 正 黑 体 简 体\fs18\b1\bord1\shad1\3cH2F2F2F}{\fn方 正 黑 体 简 体\fs18\bord1\shad1\3cH2F2F2F}{\fnarialblack\fs12\bord1\shad1\4cH000000}{\fnarialblack\fs12\bord1\shad1\3cH2F2F}{\fnarialblack\fs12\bord1\shad1\4cH2F2F}{\fnarialblack\fs12\bord1\shad1\3cH2F2F}{\fnarialblack\fs12\bord1\shad1\4cH2F2F2F}{\fn 方 正 黑 体 \fs18\bord1\shad1\3cH2F2F2F}|atts k,base:O0.中国0:MC 0|atts0,base:O0}通过关联堆栈连接操作构建,标识符为nil,其中最右边的对象(标识符为O0)是基础层最左边的对象(标识符为Ok)是堆栈的顶层。每个类MCi都是MetaObject的子类,并且塔的每个元素中的base的值为O0。下面的重写规则解释了元对象塔的一层如何与它上面和下面的层通信,以及在顶层的情况下,元对象塔如何与环境通信。in:O0aM{O k:MCk|base:O0,in:LMOS}−→{O k:MC k|基:O0,in:L·M MOS}输 出 :{\fn方正黑体简体 \fs18\b1\bord1\shad1\3cH2F2F2F}{\fn方正黑体简体\fs18\bord1\shad1\3cH2F2F2F}{\fnarialblack\fs12\bord1\shad1\4cH000000}{\fnarialblack\fs12\bord1\shad1\3cH2F2F}{\fnarialblack\fs12\bord1\shad1\4cH2F2F}{\fnarialblack\fs12\bord1\shad1\3cH2F2F}{\fnarialblack\fs12\bord1\shad1\4cH2F2F2F}{\fn方正黑体\fs18\bord1\shad1\3cH2F2F2F}|输出:cfReq·cL MOS}−→{O k:MC k|输出:cL MOS}配置(cfReq)上一页:联系我们|up:cLJO:MC|输出:cfReq·cL−→ BMOJ:MCJ|上:cLJ·cfReq O:MC|输出:cL下载:联系我们|down:M·LJO:MC|在:L−→ BMOJ:MCJ|down:LJO:MC|在:L·M其中MOS是元对象的可能空列表,L,LJ是消息cL的列表,cLJ是配置请求的列表,M是消息,cfReq是包含用于创建元对象塔的请求的消息配置,并且在“out”规则中例如,1.2中的委托应用程序请求创建自己的克隆,该克隆将响应另一个对象的请求。为了处理元对象塔的创建,我们必须扩展元对象塔的规则。在3.3和3.4中,我们提出了元对象和元对象塔的规则,可以处理元对象塔配置的动态创建。图5示出了具有基本对象O、消息分组OaM从周围环境进入,正在创建配置文件配置(cfReq),消息MJ准备从元对象MO的“down”列表移动请注意,通过说明元对象塔的内部上下通信对外部观察者是不可见的,我们可以将具有基本对象标识符O的元对象塔视为与具有标识符O的对象一样对待外部环境。因此,我们可以查看任何梅塞格?塔尔科特?登克尔9✁❆元对象塔通过异步消息传递相互通信的系统,作为异步对象重写理论的自然推广。我们称这种描述元对象塔异步通信系统的重写理论为元对象重写理论。OaM Conf(cfReq)在美国,✁✁✁out向下倾斜M❆up❆cfReq'在……❚✁✁✁out向下倾斜✁✁起来❆❆在……✁✁✁out图五. 一个元物体塔2.3将异步对象转换为元对象我们定义了一个从异步对象重写理论到元对象重写理论的映射,并证明了这个映射保留了行为。我们假设一个对象理论,其中对象类的属性标识符不同于可区分的元对象属性标识符。对于每个异步对象类OC,我们关联一个元对象类o2m(OC)。o2m(OC)是MetaObject的子类,并具有OC的附加属性。类的异步对象被转换为单层元对象塔,如下所示。 设MOatts(O)=(base:O,up:nil,dwn:nil,in:nil,out:nil)是O的初始元对象属性。然后o2 m(单位:OC |atts)={O:o2m(OC)|atts,MOatts(O)}.通过将o2m定义为消息上的恒等式,将映射同态扩展到异步对象配置(对象和消息的多集)。对于对象类的每个规则,存在如下获得的Meta对象类的对应规则。对象规则r:Oa M中文(简体)|atts− →O:OC|关于我们其中oCf是异步对象配置,被映射到Meta莫O❆❚梅塞格?塔尔科特?登克尔10对象规则o2m(r):O:o2m(OC)|atts,out:cL,in:M·L−→O2O:o2m(OC)|attsJ,out:cL·o2r(oCf),in:L其中o2r(oCf)是创建o2m(oCf)的请求:Conf(o2r(oCf))= o2m(oCf)。定理2.1给定任何异步对象类OC,在类OC和o2m(OC)的重写理论的联合中,中文(简体)|atts100 和o2m(单位:OC|atts)在观测上是等价的更一般地说,让oCf是任何异步对象配置,那么oCf和o2m(oCf)是观测上等价的配置。为了理解上述定理,我们需要说明观测等价的含义。我们说两个异步对象配置在观测上是等价的,如果它们具有相同的观测集。有许多可能的观察选择在这里,我们选择一个简单的,记录传递的消息序列。设γ是一个序列形式的计算(证明项)(从一个对象配置oCf开始),也就是说γ是一个单个重写规则应用r(θ)的序列。在简单的异步对象理论的情况下,如果规则实例具有以下形式,则我们说r(θ)的应用传递消息Oa Mr(θ):Oa M中文(简体)|atts− →O:OC|关于我们在元对象理论的情况下,我们说r(θ)的应用传递了消息Oa M,如果规则实例具有以下形式:r(θ):θO:MC |atts,out:cL,in:M·L−→ CSO:MC |attsJ,out:cL·o2r(oCf),in:L对于重写规则应用r(θ),我们将obs(r(θ))定义为包含传递的消息Oa M的单例序列(如果有的话),否则为空序列。重写计算γ的观测obs(γ)是γ的基本重写的观测的级联,而obs(oCf)是具有源oCf的所有有限计算的观测的集合。如果两个异步对象配置具有相同的观测集,那么它们在观测上是等价的。这种观察的概念类似于[30]中研究的概念,也与[20]中异步对象理论的事件语义的偏序有关。证明草图:想法是通过将r(θ)映射到αin;o2 m(r)(θJ);αout,将o2 m归纳扩展到具有源oCf的顺序计算,其中梅塞格?塔尔科特?登克尔11⊆输入/输出规则实例α in,α out可以很容易地从r(θ)中计算出来,并且其中θJ扩展了替换θ,以适当地匹配元对象类属性。很容易看出obs(γ)=obs(o2m(γ))。因此obs(oCf)obs(o2m(oCf))。对于另一个方向,我们注意到,如果γJ是o2 m(oCf)的任何顺序计算,则存在计算γc,使得obs(γJ)=obs(γc),并且γc具有规范形式,其中内部队列有效地保持为空,并且每个规则应用o2 m(r)(θ)出现在上下文αin;o2 m(r)(θ);αout中,其中αin是r(θ)消耗的消息的交付(如果有的话),并且其中αout发出由r(θ)创建的配置从γc可以得到oCf的计算γ,使得obs(γ)=obs(o2m(γ))。3可组合通信服务示例下面我们将说明§1.2中的加密服务和委托客户端-服务器应用程序是如何在我们的语义中形式化的。由于篇幅所限,我们无法提供完整的Maude规范。但是,我们提供了规范的主要部分。以下模块使用了Maude的一些内置模块和理论,例如作为排序参数理论TRIV,以及模块,BOOL用于布尔值,带有排序Bool,和用于整数的MANINE-INT,带有排序MachineInt,以及Full Maude模块CONFIGURATION带有排序Configuration用于对象和消息的多集我们还假设一个带有MetaObject类的模块METAOBLOG,并对表示元对象和元对象塔的MetaStack和MetaTower(配置的子类别)进行排序,这与§2.2中的演示密切相关。3.1保障服务作为示例(Meta)服务,指定了一个简单的安全服务。下面的Meta对象类EncrService指定了一个可组合的服务,该服务旨在在可能观察、拦截或伪造消息的入侵者存在的情况下提供安全的消息传输。加密服务使用公钥加密。被加密的数据被称为op{ }:FieldPKey ->Field是解密操作符。与另一密钥K2构成密钥对的密钥K1可以用于解密已经使用K2加密的字段。也就是说,以下公理保持ceq{{F}PK}SK=Fif密钥对(PK,SK)。我们假设一个模块MPTO-DT,其中所有的密码运算符,排序和公理都被指定。(omod ENCR是保护变形障碍物。保护PIPTO-DT。类EncrService。子类EncrService=>< X:EncrService|up:cL,out:cL' *(B<| {A,M}pk(B))>。rl [in/Decryption]:< X:EncrService |in:({B,M}PK)* cL,down:c L ' , b a s e : A >=>if keypair(sk(A),PK)然后 else X:EncrService|in:cL > fi。endom)3.2一个简单的客户机-服务器应用程序一个简单的客户机-服务器应用程序被指定为一个普通的异步对象系统模块SIMPLEAPP。在模块SIMPLEAPP中,类SimpleClient建模了一个客户端,该客户端具有一个数据项列表,它将请求其服务器执行一个简单的操作并等待回复。 类SimpleServer通过应用函数f并回复结果数据来回复这样的请求。(数据是排序数据。endoscopy)(查看数据从TRIV到DATA是排序Elt到数据。endv)(omod SIMPLEAPP是inc DATA.保护LIST *(操作至_*_)[数据]。类SimpleClient|tasks:List[Data],ready:Bool,server:Oid.操作回复:数据->消息。操作简单:数据Oid ->消息。vars X Y:Oid. var D:数据。var dL:列表[数据]。 rl[sendSimple]:=>< X:SimpleClient|工作:dL,ready:false>(Y<|simple(D,X))。rl[rcvReply]:(X<|答复(D))=>.SimpleServer类|. opf:Data -> Data。rl[rcvSimple]:(Y <|simple(D,X))=>>(X)<|回复(f(D)。* 创建初始客户端-服务器配置iCf op oA oB:Oid。op d1 d2 d3:数据。opserverO:Oid -> Object。op clientO:Oid List[Data] Oid -> Object.op iCf:配置。梅塞格?塔尔科特?登克尔13§eq serverO(Y)=中。eq clientO(X,dL,Y)=< X:SimpleClient |tasks:dL,ready:true,server:Y>.等式iCf = clientO(oA,(d1 * d2 * d3),oB)serverO(oB)。endom)为 了 使 客 户 端 和 服 务 器 可 组 合 , 我 们 将 2.3 的 o2m 变 换 应 用 于SIMPLEAPP,获得SIMPLEAPPMO。 模块SAMPLECONF将加密服务与客户端-服务器应用程序组合在一起。现在两者之间的通信是安全的。(omod SIMPLEAPPMO是inc DATA。incMETAOBETIC.保护LIST *(操作至_*_)[数据]。SimpleClientMO类|tasks:List[Data],ready:Bool,server:Oid.SubclassSimpleClientMO 消息。操作简单:数据Oid ->消息。vars X Y:Oid.var D:数据。var dL:列表[数据]。var cL:List[ConfReq]. var L:List[Msg].rl[sendSimple]:< X:SimpleClientMO |tasks:(D * dL),ready:true,server:Y,up:cL>=>< X:SimpleClientMO |tasks:dL,ready:false,上:cL *(Y<|简单(D,X))>。rl[rcvReply]:< X:SimpleClientMO |ready:false,in:(X<| reply(D)); L=>< X:SimpleClientMO |ready:true,in:L >.SimpleServerMO类|. op f:Data ->Data。rl[rcvSimple]:=>.OP oA oB:老。op d1 d2 d3:数据。操作serverMO :Oid -> MOStack。op clientMO:Oid List[Data] Oid -> MOStack.eq serverMO(Y)=. eq clientMO(X,dL,Y)=< X:SimpleClientMO |tasks:dL,ready:true,server:Y,moAtts(X)>. endom)(omod SAMPLECONF是inc ENCR。incSIMPLEAPPMO.A motB:MOTower.op moConf:配置。老了。EQmotA ={ o clientMO(oA,(d1 * d2 *d3),oB)}。eq motB ={ oserverMO(oB)}。梅塞格?塔尔科特?登克尔14等式moConf = motAmotB。endom)配置moConf = motA motB对应于图2中的图片。3.3向客户端-服务器应用程序现在,SimpleServer的功能被扩展到处理复杂的请求,方法是创建Helper类的对象来进行计算,从而释放服务器来回答其他请求。SimpleClient类也被扩展以发出复杂的请求。为了以统一的方式处理动态对象(可能创建其他对象的对象),我们引入了ObjectD类和newId操作,用于为新创建的对象本地生成新的对象标识符。ObjectD类的对象有一个属性newCnt:MachineInt,用于跟踪此对象创建的对象数量。(omod TD是ObjectD类|newCnt:MachineInt.op newId:Oid MachineInt -> Oid.endom)客户端类扩展为能够发送复杂请求,服务器类通过添加用于服务复杂请求的规则进行扩展。它是ObjectD的子类,以便创建帮助对象来执行复杂的计算。(omod DELEGATINGAPP是inc SIMPLEAPP。包括TD。ComplexClient类|ctasks:List[Data].Subclass ComplexClient< SimpleClient.操作复合体:数据Oid ->消息。vars X Y Z:Oid.var D:数据。var dL:列表[数据]。 rl[sendComplex]:=>(Y<|复数(D,X))。ComplexServer类|.Subclass ComplexServer< SimpleServer.Subclass ComplexServer< ObjectD.rl[rcvComplex]:< Y:ComplexServer |newCnt:n >(Y<|复数(D,X))=>< Y:ComplexServer |newCnt:n+1>.类助手|任务:数据,客户:旧,完成:布尔。op g:Data -> Data.rl[doComplex]:梅塞格?塔尔科特?登克尔15=>(X <|g(D))。endom)这个对象模块像以前一样被转换成元对象模块3.4将动态对象创建添加到MetaObjects我们用创建请求的语法扩展了METAObjectD模块,并通过继承MetaObject和ObjectD类来定义动态元对象的类MetaObjectD。(omodDYNMETAOBSERVICESisinc METAOBSERVICES.包括TD。MetaObjectD类|.子类MetaObjectD< MetaObject。子类MetaObjectD< ObjectD。* 使用语法扩展塔模型以处理塔创建排序TowerReq。opBaseO:Oid Cid AttributeSet-> TowerReq.opAddMeta:Oid Cid AttributeSet TowerReq-> TowerReq.子排序塔<要求配置要求操作堆栈:TowerReq -> Tower。op baseId:TowerReq -> Oid.varscfR cfR0 cfR1:配置要求var M:Msg.varsX Y:老。var MC:MetaObject.varT:塔要求varATT:AttributeSet。方程式:Conf(M)=M。等式1.Conf(cfR0 * cfR1)= 1.Conf(cfR0)1.Conf(cfR1)。等式Conf(T)={Stack(T)}。eq堆栈(BaseO(X,MC,ATT))=.eq堆栈(AddMeta(X,MC,ATT,T))= o堆栈(T)EQbaseId(BaseO(X,MC,ATT))= X.eq baseId(AddMeta(X,MC,ATT,T))=baseId(T)。endom)3.5使用委托客户端服务器组合我 们 首 先 将 o2m 转 换 应 用 于 模 块 DELEGATINGAPP , 以 获 得 模 块DELEGATINGAPPMO以及相应的可组合客户端和服务器类。模块ENCRD扩展了加密服务,以便在将请求发送到堆栈之前将扩展是通过使用MetaObjectD子类化并为塔请求添加额外规则来完成的。为了简单起见,我们假设出现在上列表中的是梅塞格?塔尔科特?登克尔16单个消息或单个塔创建请求。(Omod DELEGATINGAPPMO是inc SIMPLEAPPMO。inc DYNMETAOBJECTIVE.类ComplexClientMO |ctasks:List[Data].Subclass ComplexClientMO< SimpleClientMO.Subclass ComplexClientMO< MetaObjectD.操作复合体:数据Oid ->消息。vars X Y Z:Oid. varD:数据。var dL:列表[数据]。 var cL:List[ConfReq].var L:List[Msg].rl[sendComplex]:< X:ComplexClientMO |ctasks:D. dL,ready:true,server: Y,out:cL>=>< X:ComplexClientMO |ctasks:dL,ready:false,base:X,输出:cL *(Y <|complex(D,X))>.ComplexServerMO类|.Subclass ComplexServerMO< SimpleServer.Subclass ComplexServerMO< ObjectD. 子类ComplexServerMO< MetaObjectD。rl[rcvComplex]:=> .HelperMO类|.子类HelperMO Data.rl[doComplex]:< Z:HelperMO|任务:D,客户:X,完成:假,输出:cL>=>< Z:HelperMO|任务:D,客户:X,完成:true输出:cL *(X<| g(D))>。endom)(omod ENCRD正在保护ENCR。incDYNMETAOBJECTIVE.类EncrDService。子类EncrDService ==>< MO:EncrDService|newCnt:N+1,上一页:cL,输出:cL '。AddMeta(newId(X,N),EncrDService,newCnt:0,T)>.endom)梅塞格?塔尔科特?登克尔174恶劣环境我们首先需要通信服务的
下载后可阅读完整内容,剩余1页未读,立即下载
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)