中间件行为属性的建模、验证和评估

理论计算机科学电子笔记133（2005）139-157www.elsevier.com/locate/entcs中间件行为特性Jérôme Hugues，Thomas Vergnaud，LaurentPautetGET-Télécom Paris -Yann Thierry-Mieg，Soheib Baarir，FabriceKordon2Université Pierre Marie Curie，Applatoire摘要分发中间件通常集成为COTS，为关键的、嵌入式的或大规模的应用提供分发工具到目前为止，典型的中间件还没有对其行为属性进行完整的分析。在本文中，我们提出了我们的中间件建模和验证其行为属性的工作，这项研究被应用到我们的中间件架构：PolyORB。然后，我们提出的工具和技术部署，实际验证我们的模型的行为属性：Petri网，时序逻辑和先进的算法，以减少状态空间的大小。最后，我们详细介绍了一些属性，我们验证和评估我们的方法。关键词：中间件设计，验证，Petri网，LTL，对称性1介绍：中间件工程分布式中间件作为分布式实时嵌入式系统中的现成组件（COTS）被广泛地集成。必须知道每个构建块的属性，以确保其正确集成到这样的系统[4]，并确保系统作为一个整体的正确性。1电子邮件：{杰罗姆.休斯，thomas.vergnaud，laurent.pautet}@ enst.fr2Email：{yann.thierry-mieg，souheib.baarir，fabrice.kordon}@lip6. fr1571-0661 © 2005 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.062140J. Hugues等人理论计算机科学电子笔记133（2005）139在这种情况下，欧洲空间局（ESA）确定了中间件的几个用例。它们包括与卫星互动的地面站以及合作卫星和无人机的集群。这些应用程序需要多种分发机制来处理通信信道的变化，灵活的资源管理，并确保长期任务的自主性。除了分布需求，这些系统还具有非功能性需求，这些需求继承自实时工程，如可靠性，可用性，可靠性。因此，属性（如确定性，安全性，活性，及时性）必须在设计过程中进行验证，特别是在中间件级别。中间件解决方案现在支持大多数分布式应用程序的要求。它们通常支持一个给定的分发模型：一个或多个机制的组合，以实现分发，例如。消息传递（MP）、远程过程调用（RPC）、分布式对象计算（DOC）或共享内存（SM）。然而，它们通常不解决关键行为属性的验证，例如请求公平性，没有死锁或正确的资源尺寸。这就需要下一代的中间件来解决这些挑战[20]。中间件体系结构应该是通用的，以满足应用需求。此外，它应该遵循一个广泛的基于证据的系统工程方法，以提供强有力的证据，它是正确的应用程序的要求。本文详细介绍了由ENST的CS部门（中间件专家）和SRC/LIP 6（验证专家）领导的中间件验证联合工作。我们首先回顾了现有的著名中间件架构，并表明它们不便于验证;然后，我们引入了精神分裂症中间件架构作为实现验证的解决方案为了验证我们中间件的关键虚拟属性，我们改进了我们的中间件组件，使用Petri网对其进行建模，并组装模型以构建一个中间件配置。由于系统可能非常复杂，我们提出了我们用来解决状态空间爆炸的算法，并将其应用于检查中间件的行为属性。这为构建基于证明的中间件迈出了第一步。2问题陈述在本文中，我们专注于完整的分布式中间件的特征。在本节中，我们将介绍中间件架构的一些背景知识，J. Hugues等人理论计算机科学电子笔记133（2005）139141结构然后，我们讨论了使用形式化的方法来验证中间件的行为属性。形式化建模和中间件工程通常被认为是两个不同的专家领域。例如，它们要么由项目的不同团队考虑，要么在设计过程的不同步骤中考虑。为了有效地实现我们的目标，我们建议协调系统建模和中间件工程，并加入ENST和LIP6的E EQUIPMENT。ENST在中间件实现方面有着长期的经验，包括GLADE，Ada 95的分布式系统附件的唯一工业实现; Ada- Broker一个开源CORBA ORB。LIP 6/SRC部门在将形式化方法应用于分布式系统的算法和工具的开发方面有着长期的经验，它开发了CPN-AMI工具套件来建模，然后使用Petri网分析系统2.1DRE系统DRE系统需要可适应的分布模型和中间件架构：Rajkumar [19]将消息传递作为DRE系统的解决方案，并提出了实时发布者/订阅者服务。Ada分布式系统附件[13，17]集成了几种机制（DOC，RPC，SM）。RT-CORBA为实时系统扩展了CORBA这导致了几个tailable中间件体系结构。例如，可配置的中间件，如TAO [22]，让应用程序选择特定的运行时策略来支持DOC分发模型。它依赖于架构和设计模式[9]来支持大量的策略。自适应和响应中间件[20，3]扩展了中间件配置机制，以适应应用程序上下文中的特定变化。这种架构提供了有前途的属性，以满足QoSappli-阳离子的要求。通用中间件，如Jonathan [26]，定义了抽象的规范组件和架构，它们的实例化提供了一个特定的分发模型。Jonathan为多媒体系统提供了CORBA个性（David）、Java RMI个性（Jeremie）和专门的个性。这些架构可以满足严格的要求。但它们只能部分地确定它们的属性：它们通常依赖于特定场景的测试，例如波音公司然而，当将中间件作为一个整体来考虑时，存在双重组合爆炸：一个中间件配置的可能执行场景的数量随着线程和请求的交织而增加142J. Hugues等人理论计算机科学电子笔记133（2005）139随着中间件的适应性和通用性而增加。因此，我们声称测试不足以评估中间件的行为属性，如没有死锁，请求公平性，或正确的资源尺寸。我们建议使用形式化的方法来建模，然后验证我们的系统。2.2中间件验证本节讨论建模语言的选择及其适用于建模和验证中间件的形式化验证方法目前有两种形式化方法：基于证明的验证（如B [1]或Z [8]）和模型检查（使用工具和语言，如SPIN [11]或LUSTRE [10]）。在基于证明的方法中，模型是通过公理来描述的，属性是使用定理证明器来验证的定理。在模型检查中，模型是用一种语言来表达的，从这种语言中可以计算出穷举执行（这通常需要一个基于数学的定义）。“执行引擎”产生与系统相关联的exhaustive状态空间，作为一个图，其中动作（语言中的然后可以探索图以检查属性是否满足。这两种方法是相辅相成的。基于证明的技术允许分析无限系统。然而，使用定理证明器是一个非常困难和非常技术性的任务，很难自动化。相反，模型检查专用于有限状态系统，但建模和验证可以使用图形工具包完成，并且大多数步骤可以自动化[6]。我们选择了良构Petri网（WN）[5]作为模型检查的输入语言。WN是高级Petri网，其中令牌是类型化的数据持有者。这允许系统的简洁和参数化定义，同时保留其语义。WN的一个主要特征是它们允许自动和高效地构造符号可达图：商状态空间，其中节点是状态的等价类，并且弧是事件的等价类。这个图是通过利用对称性来构建的，产生一个符号状态空间，有时比具体的状态空间呈指数级小，因此更易于管理。最近的工作已经自动分析了系统[25]允许的对称性，以及属性[2]允许的对称性，允许完整的LTL模型检查，同时有效地解决了众所周知的组合状态空间爆炸问题。正如我们在第5.2节和第6.1节中所展示的，使用这些基于熵的约简允许我们验证我们系统的属性J. Hugues等人理论计算机科学电子笔记133（2005）139143而普通状态空间生成对于经典技术是不可行的在本文的其余部分，我们提出了分裂中间件体系结构，并展示了我们如何重新设计它，使中间件的验证。然后，我们详细介绍了我们使用的算法和分析我们的中间件体系结构。3精神分裂的中间件体系结构在本节中，我们将介绍“精神分裂症中间件架构”的关键元素中间件结合了两个互补的方面：（1）使用主机和操作系统资源（例如任务、I/O）实现分布式系统的框架;（2）构建可移植分布式应用程序的一组服务。在[12]中，我们介绍了担忧在[28]中，我们提出了PolyORB，我们实现了这样一个精神分裂的中间件。我们评估了它作为中间件平台的适用性，以支持多种规范（CORBA，Ada分布式系统附件，Web应用程序，Ada消息服务接近Sun从我们的实验中，我们注意到，一个减少的服务集是足够的描述各种分布模型。我们确定了请求处理的七个步骤，每个步骤都被定义为一个基本服务。服务是通用组件，为其提供了通用实现。开发者可以提供替代实现。每个中间件实例都是这些实体的一个一致的集合µBroker组件协调这些不同的服务，它负责在中间件实例中正确传播请求。请求传播µBrokerµBroker图1.一、Schizophrenic中间件体系结构中的请求传播3 PolyORB由 AdaCore（http://libre.act-europe.fr/polyorb）服务器对象客户端144J. Hugues等人理论计算机科学电子笔记133（2005）139图1说明了PolyORB服务如何协作以在位于两个单独节点上的两个应用程序实体之间客户端使用寻址服务（1）查找服务器然后，它使用绑定工厂（2）建立与服务器的连接，使用一个通信信道（例如，套接字、协议栈）。使用表示服务（3）将请求参数映射到适合于通过网络传输的表示上，这是将数据转换成字节流的数学映射（例如CORBA CDR）。协议（4）被实现用于通过传输（5）服务在客户端和服务器节点之间进行传输，传输（5）服务在两个节点之间建立通信信道。两者都可以简化为自动机。然后，请求通过网络发送，并由服务器解组。在接收到请求时，中间件实例使用激活服务（6）来确保具体实体可用于执行请求。最后，执行服务（7）分配执行资源以处理请求。这两项服务依赖于工厂和资源管理-元素设计模式。因此，我们的中间件架构中的服务是管道和过滤器：它们计算一个值并将其传递给另一个组件。我们对PolyORB的实验表明，它们遵循相同的语义，它们只适用于匹配精确的规范。它们可以被简化为众所周知的抽象概念。µBroker处理这些服务的协调：它分配资源并确保通过中间件传播数据。 此外，它是控制整个中间件的唯一组件：它操纵关键资源，如任务和I/O或全局锁。它包含中间件行为特性Schizophrenic Middleware体系结构提供了对中间件的全面此架构将一组专用于请求处理的通用服务与µBroker分离。后者直接负责中间件的行为。因此，我们隔离了系统的控制环，存在于所有中间件实例中：它是首先要验证的关键组件。4µBroker：源代码和正式模型实现我们将µBroker确定为架构的控制回路。我们现在讨论它的体系结构和映射到源代码和正式实现。J. Hugues等人理论计算机科学电子笔记133（2005）1391454.1µBroker架构我们首先提出了µBroker的架构，并详细介绍了其组件。已经定义了几种来源：[18]详细介绍了TAO中实现的不同请求处理策略; CARISM项目[14]允许对通信堆栈进行动态重新配置。因此，µBroker必须具有足够的适应性以支持其中的大多数，并且仍然提供清晰的设计以实现建模和验证。我们为µBroker提出以下架构（图2）：• µBroker Core API处理与其他中间件服务交互的功能部分; 2它提供一个接口来配置中间件实例和助手例程，以执行特定功能，例如管理I/O。该组件直接与中间件绑定、传输、执行和寻址服务交互;• µBroker控制器管理与µBroker关联的状态自动机。它授予对中间件内部（任务、I/O和队列）的访问权限，并调度任务来处理请求。它负责µBroker的行为部分。有几个策略改进了它的行为：异步事件检查策略设置轮询和读取策略来检查I/O源上的事件;请求队列对要处理的请求进行排序（例如FIFO，EDF命令），调度器选择执行请求的线程功能性组件绑定传输执行寻址中间件服务µBroker政策µBroker核心APIµBroker控制器图二. µ Broker的两面行为组件异步事件检查请求请求调度器任务管理µBroker实体由它们的接口和一个通用的高级行为契约定义，这些实体的实例可以细化此行为以支持不同的策略。该架构已在PolyORB中实现。它使用定义良好的实体，并展示了它的适应性，以支持可配置中间件中的经典策略或在RT-CORBA等规范µBroker模式提出了对中间件控制循环的全面描述，并向中间件行为属性的验证迈出了一步。146J. Hugues等人理论计算机科学电子笔记133（2005）1394.2对一个中间件配置进行1. 模型库2. 组装配置3.评估一个配置交流场所图三. µBroker建模步骤我们现在使用Petri网作为系统建模和验证的语言来描述我们的架构建模（图3）。第一步：我们为每个中间件组件的变化制定一个Petri网模型Petri网变迁表示原子动作; Petri网位置是中间件状态或资源。不同模块之间的公共位置定义了Petri网模块之间的交互，它们充当通道位置[24]。步骤2：对于µBroker的一种配置，选择一些Petri网模块来生成完整的模型。通信位置（黑色轮廓）表示到其他µBroker功能或中间件服务的链接。步骤3：合并选定的模块以生成全局模型。此模型和一个初始标记支持中间件属性的验证。函数可以单独验证，然后组合成完整的Petri网模型。多个模型可以从一个通用的模型库中组装。因此，我们可以测试特定条件（策略和设置）。Petri网的初始标记定义了可用资源（例如，线程、I/O）;或设置内部计数器。它的状态空间覆盖了所有可能的原子操作的执行：我们测试所有可能的执行顺序。我们详细介绍了从DRE系统的中间件需求到使用Petri网对一种配置进行建模的步骤。这使我们能够在我们的模型上验证特定的中间件行为属性。5查看µBroker在本节中，我们将介绍µBroker的一些预期属性，以及用于通过模型检查来验证它们的形式化技术。场景的初始标记J. Hugues等人理论计算机科学电子笔记133（2005）1391475.1µBroker配置和模型在本节中，我们将回顾表征µBroker的关键参数，以及此类组件可能具有的一些属性µBroker由一组策略和它使用的资源定义。这些设置对于大量应用程序是通用的。我们考虑一个服务器模式的中间件实例，它处理所有传入的请求。我们研究了µBroker的两种配置：单任务（一个主要的环境任务）和多任务（多个任务，使用[18]中描述的领导者/追随者策略）。后者允许并行请求处理。我们假设中间件资源是预先分配的：我们考虑一个静态的线程池;有限数量的I/O源和一个预先分配的内存池来存储请求。这个假设是可以接受的：它对应于关键系统背景下的典型工程实践。我们的实现和相应的模型由三个参数控制：• Smax是侦听传入数据的I/O源的上限;•Tmax是中间件中可用的线程数;• Bsize是分配给从I/O源读取数据的Buffer的大小Smax和Tmax定义了中间件节点的工作负载配置文件，Bsize定义了µBroker为处理请求而分配的内存的约束。这些参数控制中间件吞吐量和执行正确性。我们列出了我们组件的四个基本属性。它们代表了我们的组件必须验证以完成其角色的关键属性。• P0（对称）：线程和I/O是无序的，类中的元素是等价的;• P1（无死锁）：系统可能总是处理传入的请求;• P2（一致性）：不存在超过临界流量的缓冲器;• P3（公平性）：源上的每个事件都被检测和处理.P0、P1、P3很难通过执行一些测试用例来验证：必须检查所有可能的执行顺序。这可能是不可排序的，甚至是不可能的，因为许多可能的线程和请求交织在一起。此外，对静态资源进行适当的度量以确保一致性（P2）是DRE系统的一个强有力的要求，但这对于诸如中间件之类的开放系统来说是一个难题。因此，我们建议通过模型检查来验证它们。148J. Hugues等人理论计算机科学电子笔记133（2005）1395.2分析方法我们建模的系统是复杂的，使用不同的资源，其状态空间预计是巨大的。 我们在第6.1节中详细介绍了数字：该系统具有对于我们考虑的值，最多10 -11个 因此，我们决定通过对模型进行对称性分析，并使用结果生成一个紧凑的表示的状态空间的系统，适用于模型检查。这种对称性分析是完全自动化的，并且针对我们所考虑的中间件的每个给定配置执行我们还考虑到要检查的属性，通过使用动态适应的on-the-proximity算法抽象掉属性未观察到的行为，允许进一步减少。本节简要解释了工具的工作原理（算法的完整描述可以在[25，2]中找到）。此外，这些技术可以通过简单的接口使用，不需要了解这些内部结构。5.2.1P0：分析模型我们希望证明属性P0（对称性）;第一步是对称性分析，探索模型的结构，以确定哪些数据类型呈现同质行为。给定数据类型的两个元素e1和e2是对称的，如果在系统执行的任何时候交换e1和e2所谓行为，我们的意思是从观察者对于这种分析，我们首先考虑基于行动的观察者的LTL观点，将所有事件视为一个序列。对于这个有点近视的观察者来说，用于触发事件的实际值是模糊的，只有动作发生的序列是可见的。这样一个序列被称为ω-词，其字母表是一个动作的发生。ω-词集系统可以使用事件发生的字母表生成的语言被称为系统的动作语言。由于交错语义，这种语言在看到操作变元的字母表上可能比系统的语言呈指数级小。它可以表示为商状态空间图，从而指数地小于具体状态空间图。为了分析系统的对称性，我们的算法[25]检查系统的每个动作（转换），以找出它区分哪些元素（如果有的话），并得出结论，至少有一个动作区分的任何元素都应该在R中区分。该对称性分析的结果是等价关系R，该等价关系R列出了每个数据类型的对称值，J. Hugues等人理论计算机科学电子笔记133（2005）139149尊重系统行为的语言。这种自动计算确保了在R下被视为等效的任何元素不会被系统的任何动作区分开。R定义了一组允许的置换或旋转[5]，可以应用于系统的对象，而无需确定过渡关系。然后，我们将高级注释转换为以简单且易于分析的形式使用R的符号表示，即格式良好的网的严格语法[5]。最后，我们使用GreatSPN [7]核在R下构造了一个商可达图，其中节点表示R下的一个等价状态类。让我们提到对称性的计算是非常快的，因为它是Petri网的结构属性。因此，它的复杂性与规范的大小（位置和转换的数量）有关，而与状态空间的大小无关。µBroker的对称性分析是根据我们的模型结构计算的。它产生一个等价关系R，该关系表示所有线程（分别为（来源相同）。因此，我们证明了P0（对称性）为真.请注意，此属性在模型的第一个版本上不为真，为了获得它，我们必须调整µBroker组件的一些建模选择。5.2.2P1、P2：双对称性质属性P1表示不存在死锁;这是我们基于动作的LTL观察器可以看到的属性。因此，我们可以在关系式R下产生的商上验证这个性质。商图列出了最多的Smax！Tmax！在COMPAC TMANER中，比具体的状态空间小，允许更快的验证从酒店为了验证P2（一致性），我们检查对内存池的访问是否正确.的地方（DataSlotsi）i∈1. M表示内存池。写操作从这个集合中插入一个标记，读操作从这个集合中取出一个标记。在一个插槽中写入多次时会发生数据不一致。它通过由LTL公式（1）表示的安全属性进行测试，该LTL公式（1）断言这样的状态是不可达的。有意思的是，这个性质是直接在在R下产生的图，因为元素的排列不会改变在P1中测试的位置的基数。因此，如果我们考虑商状态空间的一个节点，因为它的所有元素在R下都是等价的，我们150J. Hugues等人理论计算机科学电子笔记133（2005）139可以直接断言它是否验证卡（d）≤1。 通过分析该属性的对称性，自动证明并使用该属性，无需用户因此，我们通过对Smax和Bsize的不同值进行模型检查，验证了Smax≤Bsize没有数据损坏，但我们注意到数据损坏发生在其他情况下。我们解释这一结果的事实，模型语义不允许超过卡（数据S批）连续写操作，因此不超过缓冲器。5.2.3P3：利用观察到的行为对称性我们已经看到系统R的等价关系，虽然是允许的，但可以允许验证对称性质。然而，为了验证P3（公平性），我们需要评估LTL公式：⎧s∈S（a）（二）它声明给定源上的任何事件最终都将被处理。如果是这样，表示s的令牌应该从通知位置ModifiedSrc（“µ Broker检测到一个挂起的请求”）移动这个属性不能被我们基于动作的LTL观察器可靠地观察到，因为它需要记住动作“the µ Broker detected a pending request from s“中s然而，由于对称性，如果S∈ S，使得P3成立，正如我们所知，如果所有的源都是等价的，我们就证明了性质S∈S。这避免了对每个来源的冗余验证，尽管这也是可能的，因为来源的数量假设是有限的。因此，我们选择一个源s，我们个性化，通过构建一个商图下更严格的关系RJ，使s不能与其他来源。因此，我们的观察者现在可以把与s有关的事件看作与其他来源有关的事件然而，即使是一个单一的源的成本是高达阶乘增加（卡（S）！）的状态空间大小。因此，即使系统在结构上是对称的，该公式不是--因此，商可达图支持一个主要的限制：它不处理部分对称系统或部分对称属性。J. Hugues等人理论计算机科学电子笔记133（2005）139151然而，最近的进展表明，这些部分对称性可以通过符号同步产品（SSP）方法[2]在LTL验证中利用。基本的直觉是使用一个能够放大的观察者（即通过使用一个细化的RJ），只要有一个潜在的问题，缩小（即通过允许RJ中的更多排列），当视觉足以验证属性。例如，属性可以仅在执行运行的部分中区分对象，例如P3.当没有请求挂起时，源可以被置换.只有当place ModifiedSrc包含来自源s的请求时，我们才需要区分源s。这种部分时间不对称可以通过使用Büchi自动机来捕获，LTL财产[27]。为了执行模型检查，我们计算通过属性的否定识别的语言与系统的语言的交集该操作由状态空间和公式的自动机的同步乘积来计算。因此，它通常是LTL公式的自动机的大小和状态空间本身的乘积然而，我们构建了我们的智能系统，bolic Synchronized Product的，我们调整关系RJ（我们的缩放设置），在该设置下，我们构建一个状态的后继者，到LTL自动机的弧，它正在与之同步。考虑对应于、J，v，q`，z\，abJ，，J，，q`，，`，\\，P3的否定表示图4。一个ω字0 1（或事件序列）由该自动机识别，.，真的，一个事件是由一个有限的序列组成的（我们don’t care which, synchronizing with the arc true),followed by an event such that图4：性质P3的否定的自动机真（接受状态Q1）。 这样一个序列与P3相矛盾，从而产生一个反例在SSP构造中，当与弧“true”同步时，没有引入不对称性，因此所有模型对象都是等效的，我们可以缩小;但是与弧“a<$b“的同步迫使单独的模型对象被缩小。对源“s”进行量化（放大），以便进行正确的符号验证。在 当 前 情 况 下 ， 由 于 P3 为 真 ， 因 此 匹 配 “a_b_always_true“ 但 不 匹配”<$b_always_true”的同步产品序列证明P3有效性的SSP的最终大小因此不超过R下允许所有排列的商图的大小，因为SSP中的所有动作最终与arctrue同步。SSP是一种功能强大的技术，也能够处理部分对称系统，其中对象仅在模型的局部部分表现不对称通常，由于基于动作的对称性分析是全局的，因此这些局部对称性152J. Hugues等人理论计算机科学电子笔记133（2005）139不对称将产生限制关系R，并且在R下构建的图可以与具体的状态空间一样大。一个典型的情况是分布式系统，在初始化阶段，特权初始化器扮演不同的角色，但一旦系统运行，所有参与者都表现得像对称对等体。SSP解决了这个问题（通过在运行初始化时放大），但由于µBroker（根据设计）是完全对称的，因此这种特殊的缩减不用于我们的验证。我们计划在进一步的工作中使用这种能力，用于更先进和更复杂的配置。6验证结果和性能在本节中，我们详细说明了µBroker。6.1对µBroker进行Mono-Tasking模型有47个位置，38个过渡和134个弧。多任务模型是两倍大。任务和I/O的数量对模型的大小没有影响（它被编码为Petri网令牌的类型），缓冲器的大小对位置和转换的数量有影响图5总结了Bsize= 5和Smax= 4时的状态空间大小。Petri网模型具有平均的规模，但其状态空间很大，反映了系统的复杂性。它的大小随Tmax和Smax呈指数增长。我们还注意到，符号可达图是小了几个十的权力，这一比例增加T最大。因此，在通常的工作站上，计算可以在可接受的延迟内完成，对于最大的型号，在运行GNU/Linux的2.6GHz Pentium-4计算机上，具有512 MB内存，在10小时从这些不同的数据中，我们声称，由于典型工作站的固有内存限制，如果不使用这些先进的模型检查技术，PolyORB的分析就无法进行。如图5所示。它清楚地表明了具体的状态空间和商可达图之间的指数比。作为一个例子，即使对于常见的中间件配置（7个线程和4个I/O源），系统也会呈现大约1011个状态，但我们可以计算和评估其在具有512MB容量的计算机上的商可达性图上的性质内存没有swap我们还观察到，商图的演变减少。作为示例，从4到5个线程，商图增加80%的因子，并且从5到6，增加57%的因子。在给定阶段，它应该达到渐近线（例如，当添加新线程不影响J. Hugues等人理论计算机科学电子笔记133（2005）1391533、5E+053，0E+052、5E+052，0E+051，5E+051，0E+055，0E+040，0E+00图五、µ Broker的状态空间和商可达性图，S max = 4，B size = 5。见图6。 检查以评估当Tmax = 2和Bsize = 4时，P = 3。系统的符号复杂性）。这是特别感兴趣的，因为状态空间演化保持指数。SSP技术带来了进一步的减少，如图6所示，将其与全局对称方法进行比较。它显示了减少的增益如何随着参数的增加而增加。它相当于一个源的全局对称方法（没有对称性利用），然后在Smax上进行多项式大小缩减。当Smax达到5：B大小是4，属性没有被验证，正如我们在上一节，从而在上的反例产生式算法中断状态空间检查。我们验证了两种配置：我们测试了代表预期属性的LTL公式，我们提取了有助于确定资源规模的场景。我们的模型检查工具克服了µBroker模型的复杂性经验证的物业提供有力证据证明我们的架构是正确的。6.2评估我们的验证工具我们使用的工具在实现核查方面发挥着重要作用。我们的模型是使用CPN-AMI [15]创建的，CPN-AMI是一个集成了结构分析工具和模型检查器的Petri网CASE环境。然后，我们分析数据类型对称性[25]，并使用Great- SPN [7]工具套件和SSP扩展最后，对于LTL模型检查，我们使用模型检查库Spot [16]，结合GreatSPN。所有这些工具都有可用的驱动程序，使它们成为插件，可以从CPN-AMI均匀地访问，并隐藏它们交互的复杂性，1、E+121、E+111、E+101，E+091，E+081，E+071，E+061，E+05状态空间商图比1，E+00象征性SSP154J. Hugues等人理论计算机科学电子笔记133（2005）139最终用户。CPN-AMI和SPOT是在LIP 6/SRC中开发的。GreatSPN由都灵大学的Dipartimento di Informatica开发。GreatSPN和SSP计算的LTL能力是巴黎和都灵之间合作的结果。验证过程的一个重要方面是，系统的全局结构分析和SSP中使用的部分对称分析都是完全自动计算的，这要归功于我们最近对GreatSPN内核的扩展[25，2]。 当我们在广泛的配置和参数值上测试我们的属性时，“手工”对称性分析是不可行的，并且不太可靠，因为它需要人为干预。我们的感知算法可以帮助我们解决状态空间爆炸问题。减少的状态空间比典型算法产生的状态空间小10的幂。这种差异随着参数Smax、Tmax、Bsize而增加。这表明我们的工具可以验证复杂的系统。在µBroker上使用正式验证技术可以纠正一些错误，并为我们提供更高的信心在PolyORB的架构中。7结论在本文中，我们重点讨论了中间件体系结构和验证它们的行为特性。我们概述了中间件工程的当前趋势：存在多种体系结构来支持DRE系统的需求;然而，很少考虑验证。事实上，只要中间件开发没有在设计过程的早期集成分布功能和验证需求，验证分布式基础设施就是一项复杂的任务。我们的目标是提供一个基于证明的中间件。本文提出了分裂型中间件的体系结构，并详细介绍了验证分裂型中间件的步骤，选用Petri网作为建模语言，用LTL来表示并验证分裂型中间件的性质。精神分裂症架构强调中间件的关注点分离：一组基本服务覆盖中间件功能组件，中间件主循环协调它们。可以调整服务以支持可配置性和通用性需求。因此，我们的分裂中间件PolyORB是一个很好的候选人，以建立基于证明的中间件。我们确定了控制整个中间件代理的关键组件，并对其进行了细化，以定义µBroker模式。这个自适应组件提出了中间件主控制回路的完整定义。J. Hugues等人理论计算机科学电子笔记133（2005）139155我们详细介绍了建模的步骤，然后使用Petri网进行验证，Petri网是一个完整的理论框架，用于评估控制系统（如µBroker）的属性然后，我们讨论了µBroker的几种配置的验证。我们引入了工具和算法来实现验证。状态空间爆炸是用Petri网建模系统时遇到的一个典型问题。我们提出了用于克服这个问题的先进技术这些技术允许测试的LTL公式减少状态空间：商状态空间。它充分利用了模型的全局和局部对称性。因此，我们可以评估我们的模型对于传入的请求是公平的，没有死锁;我们详细介绍了如何检查资源的大小是否正确。我们注意到，商图和完全状态空间之间的比率是指数的;状态空间演化保持指数，因为商图趋于渐近线。使用经典的模型检查技术永远无法进行这种分析。因此，我们实现了关键中间件行为属性的完整验证这是朝着构造基于证明的中间件迈出的第一步。为了达到这一目标，我们必须改进精神分裂症的结构，以满足分布函数和行为验证的要求。此外，对中间件特性的分析为使用形式化方法验证复杂系统提供了一个案例研究。我们讨论了先进技术在克服组合爆炸中的应用，以及如何最大限度地利用系统信息来优化验证过程。以后的工作将考虑两个主要方向。第一个是将验证应用于更复杂的配置（更多的任务，更复杂的策略）;但完整的应用程序涉及客户端和服务器节点。第二个方向是增加模型和µBroker实现之间的联系。我们将研究从我们验证过的正式规范中推导出代码模式的方法，以直接为一个中间件配置生成源代码。这将增加中间件作为COTS集成到关键应用程序中的信心。引用[1] Abrial，J.，[2] Baarir，S.，S.哈达德和J. - M. Ilié，Exploiting Partial Symmetries in Well-formed nets for theReachability and the Linear Time Model Checking Problems ， in ： Proceedings of the 7thWorkshop on Discrete Event Systems（WODES[3] 布莱尔，G.，L. Blair，V. Issarny，P. Tuma和A. Zarras，软件体系结构在约束基于组件的中间件平台中的作用，中间件，2000年，第100页。164-184.156J. Hugues等人理论计算机科学电子笔记133（2005）139[4] Budden，T. J.，Decision Point：Will Using a COTS Component Help or Hinder Your DO-178BCertification E.，STSC CrossTalk，The Journal of Defense Software Engineering（2003）。[5] Chiola，G.，C. Dutheillet，G. Franceschini和S. Haddad，关于形式良好的有色网及其符号可达图，高级Petri网。理论与应用，LNCS（1991）。[6] Clarke，E.，O. Grumberg和D. Peled，[7] Informatica，U. T.，03 The Dog（2003）http://www.di.unito.it/~greatspn/index.html网站。[8] Diller，A.，“The B-book,” John Willey[9] 伽马，E.，R.赫尔姆河Johnson和J.Vlissides，[10] Halbwachs，N.，Lustre的教程（1993）。[11] Holzmann ， G. ， “ SPIN Model Checker, The: Primer and Reference Manual,” AddisonWesley[12] Hugues，J.，L. Pautet和F. Kordon，Contributions to middleware architectures to prototypedistribution infrastructures ， in ： Proceedings of the 14th IEEE International Workshop onRapid System Prototyping（RSP[13] ISO，[14] Kaddour，M.和L. Pautet，一种在移动环境中支持断开连接和多网络访问的中间件，在：第二届普适计算会议（Percom）的Perware研讨会论文集，美国佛罗里达州奥兰多，2004年。[15] Kordon，F.和E. 李文，应用CPN-AMI验证一个安全通道协定，在：国际皮氏网路理论与应用研讨会论文集-工具介绍部分，威廉斯堡，美国，1999。[16] LIP 6-SRC，Spot主页（2003年），http://spot.lip6.fr。[17] 穆迪，S。一、使用Ada 95内置分布式能力和新兴实时CORBA能力的混合模型的分布式面向对象实时系统[18] 皮亚拉里岛M.斯皮瓦克河Cytron和D. C. Schmidt，Evaluating and Optimizing Thread PoolStrategies for RT-CORBA，in：Proceedings of the ACM SIGPLAN workshop on Languages，compilers and tools for embedded systems（2001）.[19] Rajkumar河，M. Gagliardi和L.沈文龙，分布式实时系统的实时发布者/订阅者进程间通信模型：设计与实现，第一届IEEE实时技术与应用研讨会论文集，科罗拉多州，美国，1995年。[20] 尚茨河E.和D. C. Schmidt，Research Advances in Middleware for Distributed Systems，in：Proceedings of the IFIP 17th World Computer Congress - TC6 Stream on CommunicationSystems：+The State of the Art（2002），pp