并发对象速率受限通信模型

理论计算机科学电子笔记274（2011）67-81www.elsevier.com/locate/entcs并发对象的速率受限通信模型Rudolf Schlatte、Einar Broch Johnsen、Fatemeh Kazemeyni和S.Lizeth Tapia Tarifa挪威奥斯陆大学信息学系{rudi,einarj,fatemehk,sltarifa}@ifi.uio.no摘要今天的许多软件系统都是为部署在一系列架构上而设计的。然而，在正式模型中，通常假设架构是已知的和固定的;例如，软件是顺序的还是并发的，通信环境是同步的还是异步的，但是是有序的，等等。为了指定和分析在不同的部署场景中的模型，有趣的是，将低级部署可变性的各个方面提升到建模语言的抽象级别。 在本文中，我们提出了一种技术，用于在Creol（一种正式定义的高级面向对象建模语言）的定时扩展中对并发对象引入显式资源约束。该技术证明了对象之间的通信速率限制的例子。这些限制是组合的和非侵入性的：不需要改变模型的功能部分，并且可以选择性地将限制应用于模型的部分。事实上，速率限制由模型中的参数捕获，这允许在不同速率限制的情况下执行定时模拟。我们通过一个案例研究证明了模型中通信速率限制的有效性无线传感器网络在该域中，速率限制可以被理解为对广播数据分组的冲突模式的抽象。不同速率限制的模拟结果显示了到网络中汇聚节点的定时数据吞吐量根据可用速率而变化关键词：带宽建模、仿真、面向对象模型、部署场景1介绍今天的软件系统通常是为一系列不同的部署场景而设计的，这些场景甚至可能随着时间的推移而发展。这样的系统的示例的范围从可以部署在顺序、多核或分布式架构上的操作系统到可以使用各种传感器间通信手段（诸如有线、无线电或甚至声学通信信道）部署的基于传感器的监视系统根据部署场景，分布式系统可能会在提供给其节点的可用处理能力或内存方面有所不同，由欧盟项目FP 7 -231620 HATS部分资助：使用正式模型的高度适应性和值得信赖的软件（http://www.hats-project.eu）。1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.07.00768R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）67以及节点之间的通信信道的可用带宽在云解决方案等现代架构中，虚拟基础架构允许部署场景的各个方面符合软件的需求为了对这种高度可配置的软件系统进行建模和推理，我们不能假设具有给定属性的统一底层架构相反，我们希望在建模语言的抽象层捕获这种部署可变性，然后在不同的部署场景中推理模型在本文中，我们开发了一个通用模型的资源限制之间的可观察的时间间隔，在面向对象的建模语言Creol的执行。这些限制在语言本身内部表达，并用于对Creol中并发对象的通信环境施加速率限制Creol模型的通信环境在其速率限制中是参数化的，这允许在不改变模型的功能部分的情况下Creol是一种基于异步通信并发对象的高级可执行建模语言[14，21]该语言从并发对象内部的特定调度策略以及通信环境的特定属性中抽象出来。Creol在重写逻辑[25]中给出了形式语义，它可以直接用作重写系统Maude [13]中的语言解释器为了观察行为的变化取决于执行中可观察时间间隔之间的速率限制，我们对该语义进行了定时扩展[6]，这允许使用Maude模拟Creol模型的定时行为这使我们能够看到模型中速率限制的时间效应，并比较模型随速率变化的时间行为我们演示的例子如何在克里奥尔模型的速率限制可以用来捕捉基于无线电的消息广播以及点对点的通信信道的属性。基于网络的通信本身涉及两个对象之间的通信，例如建模两个硬件系统之间的低带宽连接基于到达的限制描述了单个组件，其限制是在无线电通信的背景我们进一步展示了我们如何可以模拟系统的行为，范围超过速率限制，使用Maude作为解释器的Creol模型。本文的结构如下：第二节介绍了Timed Creol，它是Creol建模语言的一个时间扩展，并通过一个客户机/服务器通信的例子来说明该语言。第3节提出了一个资源受限行为的建模模式，并为客户机服务器示例介绍了一个速率受限的点对点通信信道第四部分建立了带宽受限的无线传感器网络的Creol第5节讨论了相关工作，第6节总结了本文。R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）6769句法分类。C，I，M在名称ginGuardsinStmtxinVareinExprb在BoolExpr中定义。IF：：=interfaceI[extendsI]{[Sg]}CL：：=classC[（I x）][implementsI]{[I x;]M}Sg=I m（[I x]）M：：=Sg== [I x;]{s}g：：= b |x？| g ∧ gs：：= s; s |x：= rhs|暂停|等待g|回路e| if b then {s}[else {s}]|当b {s} |skipe：：= x |B|这|现在|nullrhs：：=e|新的C（e）|e！m（e）|e.m（e）|X. 得到图1. 核心Timed Creol的语法。诸如e和x之类的术语表示对应句法类别，方括号[ ]表示可选元素。表达式e和守卫g是无边值检验的;布尔表达式b包括通过相等、大于和小于运算符进行的比较。其他数据类型（字符串，数字）的表达式以通常的方式编写，不包含在此图中。2Creol中的并发对象Creol是一种分布式主动对象的抽象行为建模语言，基于异步方法调用和处理器释放点。在Creol中，对象概念上有专用的处理器，并存在于分布式环境中，对象之间进行异步和无序的通信。通信是通过异步方法调用的方式在命名对象之间进行的;这些可以被看作是并发活动的触发器，导致新的活动（所谓的进程）在被调用的对象中。本节简要介绍克里奥尔语（更多详情请参见，例如，[14，21]）。Creol对象是类的动态创建的实例，它们声明的属性被初始化为一些任意类型正确的值。可以使用可选的init方法重新定义属性。由可选的run方法触发的主动行为与由方法调用触发的被动行为交织在一起。因此，一个对象有一组要执行的过程，这些过程源于方法激活。在这些进程中，最多一个进程是活动的，其他进程挂起在进程队列上。进程调度在默认情况下是不确定的，但是由处理器释放点以合作的方式控制。Creol是强类型的：对于良好类型的程序，被调用的方法由被调用的对象支持（当不为null时），这样形式参数和实际参数匹配。本文假设程序是良好类型的。图1给出了Timed Creol的核心子集的语法（省略，例如，类继承）。一个程序由接口和类定义以及一个配置初始状态的main方法组成IF定义一个接口，接口名为I，方法签名为Sg。一个类实现了一个接口列表I，为它的实例指定了类型CL定义了一个类，名为C，接口为I，类参数和状态变量x（类型I）和方法M。(The类的属性包括其参数和状态变量。方法签名Sg声明了一个方法的返回类型I，该方法的名称为m，形参x为类型I。M定义了一个签名为Sg的方法，一个类型为I的局部变量声明x的列表，以及一个语句s。语句可以访问类属性、局部定义的变量和方法报表 赋值x：=rhs，顺序组合s1;s2，如果，跳过，70R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）67while和return结构是标准的。语句suspenduncon通过挂起活动进程来释放处理器。相比之下，警卫g控制处理器释放在声明等待g，并组成布尔条件b和返回测试x？（见下文）。如果g的计算结果为false，则当前进程被挂起，执行线程变为空闲。在这种情况下，可以调度来自挂起进程池的任何启用的进程。因此，显式信令是冗余的。表达式rhs包括声明的变量x、对象标识符o、布尔表达式b以及对象创建newC（e）和null。特别保留的只读变量this引用对象的标识符，现在引用当前时钟值（下面解释）。请注意，纯表达式由e表示，并且不允许远程访问属性。(The全语言包括具有用于诸如字符串、整数、列表、集合、映射和元组的数据类型的标准运算符的函数表达式语言。这些在核心语法中被省略了，并在示例中使用时进行了解释。Creol中的通信基于异步方法调用，表示为o！m（e）和未来变量。（当地电话是这样写的！m（e）.）在进行异步调用x：= o之后！m（e），则调用者可以继续其执行而不阻塞调用。这里x是未来变量，o是对象表达式，e是（数据值或对象）表达式。一个未来变量x指向一个尚未计算的返回值。有两个未来变量的操作，控制外部同步在克里奥尔语。第一，警卫等待x？ 挂起活动进程，除非返回到与x相关联的调用（允许调度对象中的其他进程）。第二，返回值由表达式x检索。get，它阻止对象中的所有执行，直到返回值可用。语句序列x：=o！m（e）;v：=x. get对阻塞调用进行编码，聚焦v：=o.m（e）（通常称为同步调用），而语句序列x：=o！m（e）;waitx？; v：=x。get对非阻塞的、可抢占的调用进行编码。同步自调用this.m（e）在语义中被特殊处理，以避免平凡的死锁情况。时间在本文中，我们使用Creol语言的扩展版本，其中包括一个隐式时间模型[6]，相当于每n毫秒更新一次的系统时钟。在这个扩展中，语言中包含了一个数据类型Time。Time类型的值可以通过计算表达式now来获得，该表达式返回当前时间，即，当前状态下的全局时钟值时间值形成一个总顺序，使用通常的小于运算符。因此，两个时间值可以相互比较，得到一个适合await语句中的保护的布尔值。虽然所有其他时间值都是恒定的，但将现在的表达式与另一个时间值进行比较的结果将随着时间的推移而变化在这个定时行为模型中，从对象 请注意，在 时间模型，但在这项工作中采用，使跨对象的带宽测量成为可能。（即，在我们的例子中，时钟模拟R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）67711接口客户端{1接口服务器{2return（）;2String getData（客户端调用者）;3}3}1类IClient（服务器服务器）1classIServer（）2实现客户端{2实现服务器{3String content =“";3Int count = 0;445public void run（）{5String getData（Client call）{6Int i = 0;6String result =“";7while（i）{7public int findDuplicate（）;8Fut String> packet;8public void run（）{9packet = server！getData（this）;9return int（）;10等待包裹？10packet = packet +111内容=内容+包。get;11}i = i +1;13}14}1512返回结果;13}14}16Bool authenticate（）{returnTrue;}17}图2.客户端和服务器接口和实现时钟会漂移）。这种时间模型的语义，结合Creol2.1示例：基于网络的通信本小节说明如何在Creol中对客户端-服务器通信进行建模。该模型将被扩展到捕获速率受限的通信。3、不改变模型的功能。客户端和服务器的接口如图2（顶部）所示。Server接口的getData方法返回一些数据，Client接口的authenticate方法表示认证握手协议的抽象（在实现中，这将基于例如共享密钥，但在此模型中，我们只关心通信模式）。Client和Server类的实现如图2（下图）所示我们看到IClient类的对象是活动的：创建时，它们将从服务器请求三个数据包，并在客户端组装它们。IServer类的对象是被动的。它们通过挑战调用者对自身进行身份验证来响应getData调用，然后返回一个数据包。使用一个客户端和一个服务器对象运行模拟将导致客户端对象包含字符串“0 1 2”。图5（左）显示了模型的初始状态，可以独立于任何通信约束执行和测试。3建模 资源受限行为本节 介绍了 一种捕获 时间敏 感的资 源约束 型数据库 的技术 。该技 术包括 在TimedCreol中对并发对象施加显式的资源约束这些资源约束由一个模型表示，72R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）671接口MyInterface {2. Unit resourceConsumingMethod（）;（3）45classMyClass（IntresourceLimit）15}16}1718Unit resourceConsumingMethod（）{19等待resourceUsed resourceLimit;6实现MyInterface {20resource = resource +1;7Int count = 0;21...//在这里8... //其他字段22}923}10public void run（）{11while（True）{12时间t =现在;13wait now> t;14return 0;图3.捕获资源限制的建模模式一种模式，它使用一个类扩展给定的模型，该类在每个时间间隔的可用资源中是参数。这个类包含一个活动行为，它在时间推进时重置已消耗的资源，由run方法捕获。在本文的例子中，我们应用这种技术，以便对对象之间的通信施加速率限制（见第二节）。2.1和SEC。4）。图3描述了由建议的建模模式引入的类;参数resourceLimit表示每个时间间隔内受限资源的可用资源数量，变量resourceUsed表示当前时间间隔内消耗的资源后一个变量永远不会超过resourceLimit参数的值，并且当时间推进时，它会被run方法重置为初始值（见图2）。3，第14行）。每个需要约束资源消耗的行为都是通过一种方法来建模的，该方法通过等待语句来检查受约束资源的可用性（图1）。3，行19），并且当其进行时适当地递增时间间隔内消耗的资源的数量（图3，行20）。遵循这种技术，可以直接扩展具有资源约束的给定模型。现在我们来看看SEC的例子。2.1可以使用所提出的技术来扩展，以便添加速率受限的通信信道行为。其基本思想是使用所提出的建模模式对信道进行建模，并使原始客户端和服务器对象保持不变，并且不知道对其通信施加的速率图4给出了使用建议的模式建模的通道类，其中对客户端和服务器之间的所有通信都施加了速率限制Channel接口扩展了Client和Server接口，因为channel对象将同时扮演这两种角色。IChannel类的对象初始化为参数rate，表示这里，run方法在时间前进时重置通道容量（参见图4，第23行）。实现接口的代理方法从第24行开始，如果通道在当前时间间隔内有足够的剩余容量，则传递否则，呼叫必须等待时间推进。 请注意，这里引入了一个代理方法对于受信道限制的每个方法（如上所述）。可能R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）67731接口通道24public void run（）{2extendsClient，Server {25等待客户端！= null;3Unit setClient（Client客户端）;26awaitnMessages速率;4setServer（服务器）;27Fut Bool> fauth5}28客户！return（）;629nMessage = nMessage +1;7I类通道（内部速率）30等待失败？8实现通道{31返回fauth。get;9return null;32}10return null;33String getData（Client call）{11Int n = 0;34等待服务器！null;12public void setClient（）{35awaitnMessages速率;13this.client = client;36Fut String> result14}37服务器！getData（this）;15public void setServer（）{38nMessage = nMessage +1;16this.server = server;39等待结果？17}40返回结果。get;1841}19public void run（）{42}20while（True）{21时间t =现在;22wait now> t;23nMessages = 0; }}图4. 通道接口和实现1、2//无约束模型3服务器服务器;④客户端;returnnew System. out. println（）;6client =new IClient（server）;（七）1、2//约束模型3服务器服务器;④客户端;5通道通道;returnnewIChannel（1）;returnnew System. out. println（）;8client =new IClient（channel）;setClient（client）;10channel.setServer（server）;11}图5.受约束（左）和无约束（右）模型的重叠有时需要微调不同方法的带宽消耗;例如，为了传输数据可能需要比完成认证握手更高的带宽。这可以通过在代理方法中使用所需的值图5（右）显示了如何初始化受约束的模型。请注意，与无约束模型（左）的唯一区别在于对象初始化阶段，其中客户端连接到通道，而不是直接连接到服务器。4示例：无线传感器网络本节提供了一个扩展的案例研究来说明第3节中介绍的技术。通过一个无线传感器网络模型，说明了基于到达的通信限制对模型行为的影响。一个典型的无线传感器网络由许多传感器节点，配备无线发射器，和一个收集数据的汇。传感器记录一些数据并将其发送到水槽。由于无线传感器可能非常小，或者部署在难以到达的地形中，因此并非每个传感器都能够直接到达水槽因此，传感器具有74R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）671intx = Int;2//数据包。格式：（发起人ID，序列号）3dataPacket = Packet（SensorId，Int）;45接口节点{6单元接收（Packet包）;7Unit setNetwork（网络网络）8}910接口网络{11//设置网络拓扑。12单元setTopology（Map Node，List Node>> topology）;13//从'source'广播'packet'14单元广播（节点源、分组包）15}图6.传感器网络模型的接口从其它节点向信宿路由消息的附加职责。无线传感器网络使用调度算法来实现信道接入和带宽管理，使用路由算法来实现消息的功率和带宽高效传输对于信道接入，当在单个共享信道上操作（例如，在相同频率上操作的多个基站）时，存在两种不同的选择：时分多址（TDMA）模型和具有冲突避免（CA）的载波侦听多址（CSMA）模型。对于ad-hoc网络，CSMA/CA方案稍微简单一些，但是不能提供有界的信道接入延迟和保证的公平性，这对于时间关键的应用是不可接受的另一方面，TDMA方案（在初始建立/协商阶段之后）在数据传输期间具有零开销和零冲突，并且可以增加网络的效率[12]。使用TDMA，传感器节点共享相同的频率信道，并连续发送，每个使用自己的时隙。可以以许多不同的方式来完成朝向宿的消息的路由，以优化时间消耗、能量消耗、发送的消息的数量等。本章中的模型使用了一个非常简单的Flooding算法;在[24]中可以找到一个用Creol实现AODV路由算法的更复杂的4.1模型结构在我们的模型中，代表节点的对象并不直接相互连接。相反，每个节点对象都有一个对网络对象的引用，该对象按照TDMA的思想对节点之间的传输介质的行为进行建模。这种结构使得可以通过修改网络对象的行为来对冲突、消息丢失、选择性重传和节点拓扑（可以从每个节点到达哪些节点）进行建模，而无需节点对象内部的拓扑的该对象还实现了第3节中描述的资源限制模式，以便对有限带宽进行建模。图6显示了节点和网络的接口。当节点希望广播数据时，网络的广播方法被节点调用;节点的接收R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）67751类SensorNode（SensorId id，2Int maxSensings）3实现Node {public void run（）{26while（True）{27//发送消息需要4Set Packet> received = EmptySet;28一个时间单位。5List Packet> sendqueue = Nil;29时间t =现在;6return 0;30等待发送队列！= 零;7Network network = null;31网络！广播（832this，head（sendqueue））;9public void run（）{33sendqueue = tail（）;10等待网络！= null;34wait now> t; }}11这个！return（）;3512这个！return（）;36Unit receive（Packet packet）{13}37if（~contains（received，packet））1438{15setNetwork（Network network）{39= insertElement（16this.network = network;40已接收，数据包）;17}41this.store）; }}184219public void run（）{43Unit store（Packet packet）{20while（noSensings maxSensings）{ 44sendqueue = Cons（packet，21this.store（Packet（this.id，22noSensings））;23noSensings = noSensings +1;24暂停; }}send（）; }}图7.传感器节点的实现当 生成 SensorNode 类 的对 象（ 参 见图 7 ） 时， 它的 run方 法触 发两 个 行为senseTask和routeTask。直到传感器完成了它应该完成的传感次数（通过参数maxSensings设置），senseTask才会生成一个要发送的数据包。 传感器数据（为简单起见，它只是一个计数器）与传感器的id一起添加到sendqueue如果sendqueue列表中有元素，传感器当一个传感器从另一个传感器接收到消息时，网络会调用receive方法。如果传感器之前没有看到此消息，则将其添加到接收集，并排队等待重新发送。这种无条件的重新发送实现了一种简单的路由算法：当传感器感知到数据时存在更多涉及的路由算法，其中传感器选择性地重新广播消息取决于它们是否在通往接收器的路径上，但是这个简单的算法可以说明我们的方法。模型的初始化块（未显示）通过首先创建所有传感器对象和一个网络对象来确认传感器网络。 网络拓扑由调用nw.setTopology（...）定义; 它描述了哪些传感器应该能够发送给其他哪些传感器。拓扑结构不一定是对称的;一个传感器可以从另一个传感器接收消息，但不能向另一个传感器发送。最后，节点一旦可以看到初始化的网络（通过调用setNetwork建模），就开始其活动行为。在routeTask方法中对传感器节点的时间行为进行建模当76R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）671classSinkNode实现 Node {8Unit receive（Packet packet）{2return Time（0）;9if（~contains（received，packet））3return 0;10{4Set Packet> received = EmptySet;11int maximum = maximum +1;512= insertElement（6Unit setNetwork（网络网络）13已接收，数据包）;7联系我们14lastReceived =now;15{\fnSimHei\bord1\shad1\pos（200，288）图8.sink节点的实现1类网络（内部带宽）17单位广播（2实现网络{18节点源，数据包数据包）3映射节点、列表节点>>拓扑19{4= EmptyMap;20等待已用带宽;5return 0;21usedbandwidth = usedbandwidth +1622列表节点>目标7public void run（）{23= lookup（topology，source）;8while（True）{24while（~isEmpty（target））{9时间t =现在;25Node target = head（target）;10wait now> t;26目标！receive（packet）;11return 0;27targets = tail（target）;12}28} }个文件夹13}29}1415Unit setTopology（Map Node，List Node>> topology）{16this.topology = topology;}图9.实施网络执行该方法，存储当前时间。该模型假设发送消息需要时间;在广播之后，routeTask会等待一段时间，然后继续执行。图8中给出的SinkNode类实现了与传感器节点相同的接口，但具有不同的行为。主要的区别是接收器没有run方法，因此没有自己的活动。接收器的receive方法计算接收到的唯一消息的数量，并记录接收到最后一条消息的时间图9显示了网络的实现。它的行为是通过broadcast方法实现的。带宽是信道中的时隙数。一般来说，节点在发送消息时是可伸缩的，但是它们受到汇点或网关的带宽的限制此外，发送消息的数量可能会受到关于功率效率的转换策略的由于传输是无线传感器网络中能量消耗的最大来源，因此控制带宽消耗对于节点的有效功耗和寿命非常重要[15]。4.2模拟与分析Creol我们运行了一系列的无线传感器网络的模拟，通过改变消息到达率的限制和拓扑的网络对象。节点的数量是恒定的，有四个传感器节点和一个汇聚节点。这些模拟的结果如图10所示。我们选择了两个R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）6777图10. 消息到达汇聚节点的时间是带宽和网络拓扑的函数连接到接收器，最小化消息传播距离，以及线性拓扑，其中节点形成一端为接收器的链，最大化平均消息传播时间。我们进一步模拟了一系列随机生成的网络拓扑结构，具有恒定的四个传感器节点和六个连接。每个网络包含四个传感器节点，每个节点被初始化为创建和发送三个数据包。正如预期的那样，所有消息到达接收器的时间随着可用带宽（由网络到达速率限制建模）的下降而增加此外，随机网络的性能特征可以被观察到位于两个所选择的极端拓扑结构之间，潜在地允许基于边界情况的行为来推理给定连通性的任意传感器网络的定时行为对于中小型模型（几十个物体），模拟性能令人满意请注意，Creol模型包含的实例比建模系统少，因为对象不用作数据容器，并且Creol对象对系统组件或子系统的功能进行5相关工作由并发对象和基于Actor的计算提供的并发模型（其中具有封装处理器的软件单元异步地通信）由于其直观和组合性质（例如，[1Creol的一个显着特征是异步调用方法之间的协作调度[21]，它允许在对象内组合主动和响应行为以及部分正确性属性的组合验证[2，14]。Creol在本文中，我们使用Timed Creol [6]，线性明星78R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）67克理奥尔语的定时扩展，其中时间的流逝可以通过等待语句来观察。这允许模拟模型行为的时序方面，预测或分析非功能特性的技术和方法基于测量或建模。基于测量的方法适用于现有的实现，使用专用的分析或跟踪工具，如JMeter或LoadRunner。基于模型的方法允许从特定系统的复杂性中抽象出来，但需要领域专家提供的参数[16]。在[5]中给出了基于模型的性能分析技术的综述。实验和模拟是获得分布式网络中非功能行为初步理解的主要来源。在无线传感器网络领域，使用NS-2和Omnet+等仿真器进行了实验。然而，不同的模拟器可能会给出非常不同的结果，即使是简单的协议[8]，因为模拟器对介质访问控制和物理层[4]做出不同的假设相比之下，我们在本文中已经表明，抽象模拟提供了对分布式算法行为的初步了解，而不必考虑有关较低级别层的特定假设此外，形式化模型允许对执行空间进行更系统、更深入的探索，不仅在模型检查和定理证明技术方面，而且在模拟场景的可扩展性方面[27]。使用进程代数、Petri网、博弈论和时间自动机（例如，[7，10，11，17，19]）已应用于嵌入式软件和多媒体领域。在TLA [26]中，已经指定了用于网络扩散协议的路由树发现算法族，其中该规范是可执行的（通过生成执行跟踪），并用于模拟单个运行以及给定参数集的运行。该文件的主要业绩衡量标准是在一个数据间隔期间传播数据在这里，我们使用Maude [13]通过执行Creol的重写逻辑[ 25 ]语义来模拟Creol模型Maude提供了一个高级框架，在这个框架中，可以指定灵活的和特定于领域的通信形式。Maude及其实时扩展已被用于建模和分析广泛的协议（例如，[27，29，31]），但据我们所知，尚未用于捕获参数资源，例如，通信费率。在无线传感器网络领域，Ölveczky和Thorvaldsen已经证明，与使用高级正式模型的NS-2模拟相比，实时Maude中的模拟可以提供相当准确的性能结果，这些模型在定义适当的模拟场景时比传统模拟器提供更大的可扩展性[27]。在资源限制下对面向对象系统建模的工作则更为稀少。使用UML SPT profile的可扩展性，性能和时间，Petriu和Woodside [28]非正式地定义了核心场景模型（CSM），以解决性能模型构建中出现的问题。CSM有一个资源上下文的概念，它反映了一个操作所使用的资源集。CSM旨在弥合UML规范和生成性能模型的技术之间的差距[5]。更接近我们的工作是Hooman和VerhoefR. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）6779嵌入式实时系统的仿真[20]，其中架构使用CPU和总线显式建模对象部署在CPU上，CPU之间的通信通过总线进行，总线对消息传递施加延迟，但对可以并发传递的消息量没有限制。在以前的工作[22，23]中，作者开发了一个基于并发对象组[30]的框架，使用资源受限部署组件的技术，这些组件在时间间隔内允许的并发活动量是参数化的。这里报告的工作是对这项工作的补充，今后将与之6结论和今后的工作在本文中，我们提出了一种建模技术，形式化的时间敏感的资源受限的并发对象的模式，适用于通信速率限制的建模。通过这种技术，低级部署可变性的各个方面被提升到建模语言的抽象级别，如Creol语言所示。这些例子显示了不同形式的速率限制通信可以在Timed Creol内建模，以及如何在Maude重写系统中的Creol仿真环境中使用仿真技术来观察参数速率限制对模型的非功能属性的影响，例如消息到达时间，吞吐量和协作节点网络中的分组冲突抽象。这些例子说明了如何广播和基于信道的通信模型可以建模与参数速率限制，使用所提出的技术。这些示例捕获不同的网络行为，例如，用于广播数据分组的冲突模式，并且允许观察基于无线电的消息广播以及点对点通信信道的高级模型中的定时数据吞吐量为了观察不同部署限制的影响，使用了Creol的时间模型;模拟和测试技术可用于深入了解模型行为以及参数速率限制的效果如何影响模型的非功能属性。在本文中描述的技术允许通信速率的限制，为单个对象，以充分表示定时克里奥尔语本身。然而，用于资源约束的在未来的工作中，我们计划将所提出的技术应用于其他类型的资源，例如，以获取资源可用性。然而，该方法似乎最适合于对单个对象的限制。以自然的方式对对象组的速率受限通信进行建模，需要扩展Creol语言的语义，类似于部署组件[23]。在部署组成部分的框架内彻底调查此外，通过将符号分析与模拟相结合，研究比本文提出的模拟更强的分析技术是有趣的例如，通过使用状态抽象，单个模拟运行可以捕获整个类的具体运行，但逃避完整的模型检查。80R. Schlatte et al. /Electronic Notes in Theoretical Computer Science 274（2011）67引用[1] 居尔啊哈ACTORS：分布式系统中并发计算的模型。 MIT Press，1986.[2] 沃尔夫冈·阿伦特和马克西米利安·迪拉。一个用于异步方法调用的分布式对象的验证系统。在Proc.International Conference on Formal Engineering Methods（ICFEMSpringer，2009年。[3] 乔·阿姆斯特朗。《Programming Erlang：Software for a Concurrent World》Pragmatic Bookshelf，2007.[4] Rena Bakhshi、François Bonnet、Wan Fokkink和Boudewijn R.哈弗科特流言协议的形式化分析技术。Operating Systems Review，41（5）：28[5] Simonetta Balsamo，Antinisca Di Marco，Paola Inverardi，and Marta Simeoni. 软件开发中基于模型的性能预测：一项调查。 IEEE软件工程学报，30（5）：295[6] Joakim Bjørk，Einar Broch Johnsen，Olaf Owe，and Rudolf Schlatte.Timed Creol中的轻量级时间建模Electronic Proceedings in Theoretical Computer Science，36：67-81，2010。第一届实时系统重写技术国际研讨会（RTRTS 2010）。[7] 霍华德·鲍曼杰里米·布莱恩和约翰·德里克使用随机过程代数分析多媒体串流。Computer Journal，44（4）：230[8] 瑞秋·卡德尔-奥利弗为什么在多跳无线网络中，路由不可靠。技术报告UWA-CSSE-04-001，西澳大利亚大学，2004年2月[9] 丹尼斯·卡罗梅尔和卢多维克·亨里奥。 分布式对象理论。 Springer，2005.[10] 放大图片作者：Thomas A. Henzinger，and Mariëlle Stoelinga.资源接口。在Rajeev Mür和Insup Lee编辑的Proc. Thi