软件组件动态适应的安全协调规则研究: Petri网的应用

理论计算机科学电子笔记189（2007）69-85www.elsevier.com/locate/entcs组件协调的安全适配Christophe Sibertin-Blanc1Institut de Recherche en Informatique de Toulouse，UMR CNRS5505Universit'eToulouse1，1PlaceAnatoleFrance，F-31042ToulouseCedex菲利普·P·莫朗，杰拉德·P·迪奥·U2Institut de Recherche en Informatique de Toulouse，UMR CNRS5505 ENSEEIHT，2 rue Camichel，BP 7122，F-31071 Toulousecedex 7摘要在软件工程领域，软件组件的使用现在是一种成熟的方法。然而，它提出的问题，这些组件的动态适应特定的用户需求。事实上，这些组件的开发目的是为了具有广泛的用途，因此它们实现的功能可能无法精确地满足特定用户的需求因此，我们通过所谓的调制器来解决组件之间的协调的适应。一个Moderator本身就是一个协调组件，管理使用Petri网描述和形式化的交互。更确切地说，我们研究的协调规则的动态适应的方式，用于描述一个主持人的Petri网的具体变换必须强制执行安全属性，以保持参与者之间关于协调规则的所请求的演进的一致合作。特别是，如果参与者无法检测到，则可以认为调节器的适应是安全的。我们提出了一个可计算的标准，使检查这样的satefy属性自动。我们说明了我们的方法在计算机辅助学习系统的背景下，通过调整协调规则，在考试期间控制访问文件保留字：协调，适应，软件组件，Petri网，有限自动机，安全准则。1介绍软件复用是软件工程领域中一个古老而重要的问题。在这种探索中，接口和模块化的概念逐渐出现，导致了当前的软件组件概念[9，11]。组件的组合和组装是软件体系结构的核心。组件模型基于两个关键特性：1电子邮件：sibertin@univ-tlse1.fr2电子邮件：mauran@enseeiht.fr，padiou@enseeiht.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.05.04870C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）69• 组合机制或连接器的具体化[16，1]：在这种情况下，除了结构方面之外，行为方面也起着重要作用[8，20]。• 重用的能力，因此有必要调整现有的组件[5，12]。由于组件要被广泛地重用，所以该组件的设计者不能预先考虑该组件的每个可能的使用上下文。组件方法的基本思想是提供适应和定制“标准”代码的方法当组件要与其他组件组合时，换句话说，当组件要与其他组件交互时，出现这种间隙。因此，这种不匹配可以通过改变组件本身或交互来减少，该协议定义了组件与其当前环境的组成。 软件适配领域的大部分工作[6]都集中在组合的结构方面，并使用组件的接口作为定义和实现适配的基础。 在这种方法中考虑的交互模式是基本的，即（同步）过程调用和（异步）事件发布/订阅。然而，一些作品确实专注于适应交互而不是组件，从而探索行为方面，以及对弥补和适应更复杂交互的支持这种非侵入性的方法似乎适合于将组件作为黑匣子处理。在这种情况下，相互作用及其适应可以通过描述（可能的）参与组件来定义，如[2，18]或通过更具体地关注相互作用协议本身来定义，如[6，19]和本文。此外，对实施适应措施的支持主要有两个方面：• 要么（半）自动· 来自参与者行为规范的适配器· 参与者• 或者为程序员提供支持适配正确性检查的工具。 这种方法在编排领域中得到了说明Web服务[2]。我们的方法属于后一种方法，并侧重于相互作用的适应：我们考虑允许适应[10]中提出的一般框架中规定的协调的可能性。在这个框架中，协调是通过一个特定的组件来实现的，称为主持人，它控制着顺序和条件，即编排[4]，其中执行交互。协调的规范是从设计者的角度考虑的本文的主要贡献是定义了一个可计算的安全标准，它允许确定一个适配是否正确，而不必干预协议或参与者的语义。这在开放系统的上下文中显得很有趣，在开放系统中，程序是由C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）6971组装预先存在的组件。通过使用和维护组装的零部件之间的不变关系，可以实现这种组装。因此，接口的概念允许抽象和封装组件的实现。协调的适应性（特别是我们的方法）扩展了这一过程，旨在改变一组协调组件的实际行为，同时保持将这些组件完全绑定在一起的契约（协调的规范）不变。更确切地说，参与者可以要求对话的主持人偏离协议的（预设）行为规则，以适应特定的运行时上下文。为了安全起见，这样的调整应该保证每个参与者都能参加对话， 谈话的目的就能达到。在下面的章节中，我们首先描述了功能和正确的- 协调各组成部分的联系。然后，我们定义适应性，与这些适应性相关的安全性以及如何证明它。最后，我们通过一个电子学习案例研究来说明这种适应方法2协调协议协议旨在确保系统实体之间的协调。协议被定义为一组规则，它被实例化为过程，我们称之为对话，在此过程中，实体遵循这些规则来协调各自的行为。 这些规则决定了哪些参与者可以参加一个对话，以及每个人如何能够或必须有助于其良好的处理。换句话说，会话是根据由以下项定义的协议进行的过程[10]：• 在对话过程中需要处理的数据• 会话的初始状态，即必须满足的条件，以便会话可以开始，• 谈话结束的最后状态• 参与者在对话中可以扮演的角色，即对实现协议的具体贡献，• 对角色的归属施加约束，这些约束确定要满足的条件，以便参与者可以在给定的对话中扮演某个角色• 参与者可以采取的干预措施类型，以参与对话，使其取得进展，• 决定对话控制结构的行为约束，即在何种情况下扮演某种角色的参与者可以进行给定的干预，以及这种干预的效果下一节和案例研究（第4节）提供了协调协议的两个示例。72C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）692.1作为协调组成部分的主持人协议协调的主要好处是确保参与者之间在完成某些任务方面的互动的效率和可预测性。然而，无论一项议定书的规则是什么，每一个参与者都必须确保这些规则将得到其他参与者的尊重;否则，就不能保证议定书的共同目标将得到实现。这可以通过一方面分离参与者执行的对话中的干预来实现，另一方面检查这些干预是否遵守协议规则，这是由称为对话主持人的特定组件执行的[10]。主持人负责执行协议规则，使参与者在物理上不可能违反协议规则[7]。更准确地说，一个版主：• 在创建时检查协议的初始状态是否• 将所需数据记录到变量或数据库中• 当参与者请求在对话中扮演某个角色时，根据强制转换约束的有效性返回肯定（或否定）答案;• 确保会话过程满足协议的行为约束。为此，主持人集中了对话中参与者之间的所有通信：参与者的任何干预都指向主持人，并且如果它与对话的当前状态和协议的规则一致，则主持人通过向其他参与者发送适当的消息来• 在检测到到达最终状态或会话由于某种原因被阻止（例如，其贡献对于结束会话至关重要的参与者的离开）之后，为了实现协议的行为约束，在[10]中提出了通过Petri网形式主义[13]来建模Moderator的控制结构。一个仲裁者的Petri网（简称PN）包括通信场所：接收参与者发送给仲裁者的消息的输入场所，以及从仲裁者到参与者的消息的输出场所。这个网络的初始标记对应于协议的任何会话的初始状态，其终端（死锁）标记对应于最终状态。图1展示了一个简单的在线拍卖网站。图中阴影部分（中间部分）的主持人调解和控制两种参与者之间的互动：客户（代表PN的右侧部分）和供应商（PN的左侧部分基本场景如下：客户从网站订购商品（由Moderator实现），然后将付款发送到网站。最后，他们向网站确认收到了他们的货物。Moderator将收到的订单和付款转发给供应商，并记录付款。供应商接受订单（从C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）6973供应商接受发送订单_vm优秀支付虚拟机初始T1T2order_cm付款_cm客户秩序支付接收（一）收集记录交易ack_cm（b）第（1）款承认（c）第（1）款Fig. 1. 在线拍卖网站版主），发送商品，然后收款3. 供应商和客户的行为由有限自动机描述：供应商只接收消息，客户只发送消息。该PN包括5个通信位置（order vm、payment vm、order cm、payment cm和ack cm），其对应于在主持人和参与者之间交换的消息的类型使用高级Petri网形式主义，以处理令牌携带的数据[17]。值得注意的是，通信场所中的每个消息令牌包括已经发送或将接收该令牌的参与者的身份。以这种方式，主持人能够为每个参与者管理专用的控制线程， 以跟踪其关于对话的状态协议主持人的PN是协议行为约束的正式定义，因为它决定了，对于对话中的任何参与者， 在这种情况下，主持人可以处理从该参与者接收的消息或向其发送消息。使用PN形式主义来定义协议的行为规则允许使用PN理论的技术和工具来分析行为特性。 我们不详细说明版主的其他方面（例如数据管理，会话管理，控制线程管理，或向参与者授予角色），因为我们只关心他们的行为。2.2角色的行为一个Moderator的内部Petri网（IPN）是从它的PN通过删除所有的通信库所。中启用的转换序列3我们不代表超出版主范围的交互， 即 货 物 的 （ 物 理 ） 传 输 ： 一 个 完 整 的 系 统 应 该 有 一 个 连 接 供 应 商 发送 和 客 户 接 收 转 换 的 地 方 ， 但 这 与 我 们 的 目 的 无 关 ， 因 为 这 不 是 由 版 主 管 理 的 。Init购买端Init端！付款_cm什么？订单_vm！order_cm？支付虚拟机！ack_cm74C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）69→× →{}× →{}→在初始状态下的主持人的IPN正是会话过程中可能发生的转换序列，在会话过程中，每个参与者根据其角色进行行为。特别是，这个网络假设发送的每一条消息都被使用，并且任何预期的消息最终都会被发出。我们假设Moderator的IPN具有适当的终止属性[13]：最终状态是唯一的死锁状态，并且它总是可以从 从初始状态可到达的任何状态。 该属性表明，在任何情况下，协议的行为规则有效地使协调的组件能够达到协议的目标。 这个属性是可判定的，因为它可以表示为 作为最终过渡的活力我们还假设一个协议的IPN是一个有界Petri网，即存在是任何标记中可从最初的标记。这个约束并不阻止组件发送任意数量的消息，但它意味着Moderator只能同时处理有限数量的消息。这也意味着我们不考虑可以同时协调无限数量的组件的协议。对于由主持人协调的对话中的参与者，我们假设它们有连续的行为。特别是，这适用于我们示例中的Vendor和Customer角色（见图1），因为它们的PN是一个状态机（如果删除通信位置，则网络的每个转换都有一个输入位置和一个输出位置）。因此，扮演这个角色的组件的行为可以用一个确定性自动机来描述，该自动机的转换被标记为以下类型的事件！消息，对应于发送或者是类似的事件消息，对应于接收留言该图1（a）和1（c）显示了与供应商和客户角色相对应的自动机。对于每个角色R，可以从主持人的IPN自动构建自动机TSR，以描述扮演该角色的参与者在协议会话过程中可以执行的所有事件序列[18]。为了将主持人的Petri网与其角色的转移系统联系起来，我们引入了一些定义。定义2.1标记Petri网是一个结构N=（P，T，Pre，Post，l），其中：• P是位置的有限集合，T是变迁的有限集合• 上一篇：P不0、 1个和P ost：TP0、 1个是定义从位置到过渡和从过渡到位置的弧的• l：T E是定义在发生转变时执行的事件的标记函数。发送或接收消息m1的转换的标签分别为！m1和？m1，而其他跃迁由零事件τ标记。一系列的转换s=t1.t2. t n∈T∞记作l（s）= l（t1）.l（t2）. l（t n）∈ E.• 一个标记是一个函数M：PN，它定义了停留在 网的每一个地方C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）6975→∈||∀ ∈−||• 在标记M下，当且仅当：则Pre（p，t）≤M（p）.• 在标记M下使能的转变的发生产生新的标记MJ，使得P P，MJ（p）=M（p）Pre（p，t）+P ost（t，p）。 一系列的转换s=t1.t2. t n可能出现在标记M1下，如果存在标记M2，.，M n+1，使得每个t i可以出现在M i之下，并且它的出现产生M i+1，对于i=1. n.• 对于网N的一个标记M，从M到N的语言是集合L（N，M）={l（s）：s可能发生在M下}。 当初始标记没有歧义时对于网的Minit，我们记为L（N）而不是L（N，Minit）。定义2.2一个标号跃迁系统是一个结构A=（Q，T，q0，F，l）其中：• Q是状态的集合。• T<$Q×Q是跃迁的集合。• l：T E是定义在发生转变时执行的事件的标记函数。• q0∈Q是初始状态，F<$Q是其最终状态的集合• 从状态q1开始的路径是一系列状态p = q1.q2. q n使得（q i，q i+1）T. 这样一条路径或由这条路径实现的事件集合的标号是序列l（p）= l（（q1，q2））.l（（q2，q3））. l（（q n−1，q n）），A的语言从状态q是集合L（A，q）={l（p）：p是从q的路}。• A的路径是从初始状态q0开始的路径，并且L（A）=L（A，q0）。对于会话中的任何参与者C和会话期间可能发生的主持人IPN的转换序列s此外，（sC）−1表示序列s上的对偶视点：（sC）−1表示C执行发送的事件序列（resp.”（《说文》）：“信之者，信之者也。发送）由s|C.性能设IPN是协议的仲裁者的内部Petri网，TSR是角色R的标号转移系统，C是执行角色R的参与者。以下属性将主持人的IPN与角色的自动机关联起来(i) TSR是一个有限态确定性的标号跃迁系统。(ii) 对于在IPN的初始标记处启用的IPN的任何转换序列，在TS R中存在从初始状态开始的路径，该路径实现|C）−1：s∈ L（IP N）：（s|C）−1∈ L（T S R）(iii) 相反，对于任何角色R和TSR中从其初始状态开始的任何路径sR，存在在IPN的初始状态处启用的IPN的转换序列s。76C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）69标记，使得由sR发送和接收的消息的序列恰好是由s接收和发送的消息的序列：sR∈L（TSR）：sR∈L（IPN）：sR=（s|C）−1(iv) IPN处于其最终状态，而R也处于其最终状态。3的适应方法适应是参与的组件的协调的变化，一次谈话我们考虑不修改协议签名的适应性，即会话的主持人和组件之间交换的消息类型。 我们将协议的适应定义为对话主持人状态的未指定变化，例如，在发生这种适配之后，版主可以发送和接收的内容可以与此事件发生之前的内容不同。现在，问题出现了，对话是否可以在不改变组件行为的情况下由于协调规则的使用涉及合同方面，通过对参与者的调查，可以预期参与者同意对这些规则进行调整。然而，在本文中，我们将不讨论参与者如何能够达成共识的相关性的适应，或者，相反，一些参与者如何可以引入适应没有其他参与者知道它。首先，我们在这种情况下更精确地定义适应。然后，我们考虑的属性，适应应满足，以保持会话consistent相对于初始协调规则。最后，我们概述了如何管理和实施这些动态适应3.1适应的定义我们将适应定义为不符合协调规则的Moderator状态的变化这种变化被实现为一个新的过渡，它被添加到主持人因此，自适应可以从网络的任何标记发生，在该标记下，该转换被启用，并且状态改变是由转换发生引起的。我们要求，在任何发生的适应过渡，IPN是有界的，并有适当的terminaison属性，即其最终状态总是可达的。由于IPN是从其初始标记有界的，因此需要考虑有限数量的情况，并且可以确定这些属性例如，图2显示了在线拍卖网站的改编：已向Moderator添加了一个转换（TA），以便供应商仅在确认收到货物后才收到付款4。当需要时，我们将区分适应的发生与类型一种适应。 前者表示状态变化对应的执行4.此外，为了使适应有效，在适应的调节者中必须抑制T2。C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）6977AAP PP一客户供应商订单_vmInitT1秩序order_cm接受优秀支付虚拟机支付发送付款_cm接收收款交易不是ack_cm承认记录图二. 在线拍卖网站从一个特定的点到整个会话过程的适应，而后者的特点是新的过渡。3.2适应在作用方面的透明度对话中的每个参与者都扮演着某种角色。此角色定义了它可以发送给Moderator和从Moderator接收的消息序列。从会话中的参与者的观点来看，如果参与者不能检测到这种适配的发生，则适配是透明的。实际上，参与者在适配发生之后接收的消息序列是以下序列之一它可能已经收到的消息，如果适配没有发生。但是这个条件要求Moderator能够从它的新状态接收参与者可以发送的任何消息。这导致了以下透明度的定义：定义3.1[透明度]让是协调协议，R是的角色，IPN是的内部Petri网，，而t是过渡在IPN中实现。 适应对于角色R是透明的，当且仅当，对于在t发生之后刚刚到达的IPN的任何标记M，以及当IPN处于状态M时执行角色R的参与者C的任何可能状态q：(i) 对于在M处启用的IPN的任何转变序列s，在T S R中存在从q开始的路径，其实现（s|C）−1：s∈ L（IP N，M）：（s|C）−1∈ L（T S R，q）(ii) 相反，对于TSR中从q开始的任何路径sR，存在在M处启用的IPN的转换序列s，使得由sR发送和接收的消息序列恰好是由s接收和发送的消息序列：sR∈L（TSR，q），s∈L（IPN，M）：sR=（s|C）−1图2中的适配是透明的，因为它既不改变序列，78C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）69L仲裁员从客户处收到的消息的顺序，以及仲裁员发送给供应商的顺序，前提是客户和供应商按照各自的角色行事。由于IPN从其初始标记有界，因此需要考虑有限个标记M，并且TSR也有有限个状态。（IPN，M）是一个正规的语言，因为IPN是有界的标记M，因此透明性是一个可判定的属性。3.3安全适应协调协议的修改是安全的，如果它不阻止主持人协调参与者，尽管每个人都保持其角色的行为：主持人总是向每个参与者发送属于其角色定义的消息序列，并且它能够处理接收到的消息。即使由于适应，对话在某些时候偏离了协调规则，这种定义3.2 [安全性]方案的调整在以下情况下是安全的：在遵循该协议的会话过程中发生任何事件之后，如果会话中每个参与者的行为遵循其角色的协调规则，则总是可以到达会话的最终状态。因此，适配的安全性包括，一方面，对主持人的结果状态的约束，其必须允许到达会话的最终状态，并且另一方面，对主持人和参与者之间的交互序列的约束，其必须能够相对于他们的角色一致地参与会话。特别地，适配不应将对话引入这样的状态，其中主持人被阻止，并且因此不能再同步参与者，或者其中一个参与者被阻止，因为它没有接收到它需要的消息，以便根据其角色继续进行。 当当前的 主持人或参与者的状态是这样的，它既不接收一个它需要继续的消息，也不能发送一个预期的消息安全的概念可以与更一般的一致性概念（即，关于模拟的可替代性和无卡性）在标记的转换系统[15]中在以下意义上：如果整个适配系统（即适配的调节器加上参与者）符合非适配系统，则协调协议的适配换句话说，安全似乎是一致性的一个特例，旨在描述特定组件（即调节器）本地的一致性适应定理3.3（安全自适应）设A是协调协议P的自适应. 如果A对它的每个角色都是透明的，那么它是一个安全的适应。证据我们必须证明，除了在最后状态，决不会发生Moderator和所有组件C既不能发送也不能接收消息的情况。让我们C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）6979LL注意，如果适配对于C的角色是透明的，则定义3.1的性质i）和ii）对于在适配发生之后可达到的IPN的任何标记和C的任何状态保持因此，我们只需要证明在自适应发生后没有死锁。设M为IPN的标志，q为C的状态.根据自适应的定义，（IPN，M）不是空的。如果它包含以发送动作开始的序列，则由该动作标记的转换可能发生在IPN中。否则，（IPN，M）中的每个序列以接收动作开始，并且从定义3.1的i），C能够发送相应的消息。根据定义3.1的ii），我们可以断言C不能发送IPN不期望的消息，因此不能处理。反向推理表明，如果C被阻塞等待来自IPN的消息，则它必然会收到这些消息之一。因此，当IPN有效地与协调的组件交互时，所得到的系统是无死锁的。它仍然表明，系统没有活锁，也就是说，如果IPN和组件进入一个循环，他们总是有可能退出。如果IPN处于具有发送消息出口的循环中，则它可以触发此转换。否则，如果所有的退出都是接收动作，那么从定义3.1的i）开始，总是存在一个可以发送预期消息的参与者。Q3.4表演改编可在两种不同的设置中使用自适应• 也可以是：Moderator的设计者负责提供一组可供未来用户使用的适配方案。因此，原始设计包括初始协调及其调整，可根据要求启动。在这种情况下，根据定理3.3，这些修改的安全性可以（也应该）在执行之前得到验证;• 或者在运行时：然后，所请求的适配的安全属性应该由特定的适配服务按需验证。然后可以注册并激活安全适配，如前所述。在这种情况下，检查透明度条件（定义3.1）比前面的情况更简单，因为我们只需要考虑Moderator安全适应可以由主持人临时或永久激活。在前一种情况下，适配将仅发生一次，而在后一种情况下，它将保持启用，直到用户明确请求其移除，或者直到当前会话结束。为了执行所请求的安全适配，我们可以研究两种不同的实现：• 或者，仲裁器具有监视服务，该监视服务阻止由适配抑制的转换，一旦其发生的条件为真就执行适配状态改变，然后解除阻止被抑制的转换。• 或者，主持人然后，A的激活将被实施80C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）69ECS学生P3Init主管文件存取初始化P12T31T5T6P9P11T8P10第一次禁止访问文档T7第1次访问P13警告警告T10T9T33P35P14T24T32P16T12文件存取（警告后警告P18P15T11P24T13P19第二次禁止访问文档T16第二次访问P21P26判罚点球T28T15T27P34T29T30P27返回检查T17惩罚T18T18T21P31端端T23P22通过临时将T的优先级从负级别（即，T未被启用）设置为最高级别（即，T将在任何其它启用的转换之前被触发），并且相反地，对于被禁止的转换，将T的优先级4为例我们说明了我们的方法与一个案例研究有关的访问文件的学生在网上考试期间的控制。图3描述了电子学习计算机系统（ECS），助理和任何学生之间的交互。要参加考试，学生必须首先登录ECS。根据学生的个人资料，ECS确定的文件清单，这个学生被允许进入。这份授权文件清单在考试开始时提供给每个学生。然而，无论是否有意，学生都可以访问未经授权的文件。图3.第三章。关于控制文件获取方面合作的全面说明电子学习计算机系统（ECS）充当考试C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）6981过程，其中单个参与者扮演监督者角色，而学生角色可以由多个参与者扮演ECS执行PN，这是图3的中心部分。在考试开始时，初始位置P8包含每个学生的一个彩色标记图3的左边部分显示了主管角色的行为，而右边部分显示了任何学生的行为访问文件检查由ECS执行。为此，每个学生的工作站通知ECS任何文档访问（转换T6，或转换T11，如果学生已经收到警告）。然后，ECS检查此文件是否属于学生授权的文件列表（转换T5或T12）。 如果文档被授权，则发生转换T31（或T32）。 如果 否则，系统通知监督检查的助理（转换T7或T16）。错误访问可以通过三种方式处理(i) 访问违规是第一个，但也是主要的。助理立即对学生施加惩罚（转换序列T8→T24→T27）。(ii) 这是学生第一次未经授权的访问，而且这种访问并不严重。助手警告学生不要重复此操作（序列T8→T9）。(iii) 这是学生的第二次未经授权的访问。无论访问的严重性如何，学生都会受到惩罚（顺序T16→T 13→T 27）。当学生必须承担处罚时，处罚由ECS记录（过渡T27，然后T28，或T30），学生必须停止考试（过渡T29，如果是在第一次未经授权的访问之后，或T15，如果是在第二次之后），并将其工作发送到计算机系统（过渡T18）。转换T17，T23和T21记录学生4.1文件存取控制政策图4（a）给出了学生的行为，其中转换是接收或发送。当允许访问时，自动机的当前状态始终保持其初始状态。禁止访问会导致警告或惩罚。图4（b）描述了管理程序的行为。从其初始状态开始，禁止访问被发出信号，并导致警告或惩罚消息。4.2适配示例当前版主报告对助理的未授权访问。 第一次，助手可以选择警告学生或指定惩罚（见图3中的位置P13和转换T9或T24）。第二次，助手指定一个惩罚（参见转换T13）.更严格或更宽容的态度可以通过适应来实现82C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）69P12(a)学生自动机（b）监督自动机见图4。 自动机图更严格的适应：图5（a）说明了一种更严格的态度，即在第一次禁止访问发生时立即分配惩罚。在这种情况下，当令牌进入P11时，引入新的转换T35。这个转换删除了这个令牌，并将一个令牌放入P24.对于Moderator，文档访问（doc-accessplace）现在直接解释为警告后的文档访问（doc-access（after warning）place）。ECS的这种新行为与学生行为和请求角色（即助理）行为保持在这种情况下，必须防止版主向主管发出第一个禁止访问的信号。如3.4节所述，这可以通过给予自适应转换（T35）比转换T7更高的优先级或通过禁止转换T7来实现。这种适应是安全的，因为根据定理3.3，这种适应对于监督者和学生角色是透明的：监督者自动机的可访问状态变为（Init，第二次访问），并且对于学生自动机，直接路径（Init→P unished→End）保持使用。更宽容的适应：图5（b）示出了更宽容的态度，其包括向监管器隐藏警报发生。 在这种情况下，当令牌存在于P10中时， P36，一个新的转换，T34删除这些标记并将一个新的标记放入P8.因此，PN状态返回到先前的标记。由于角色的透明属性，这种适配也是安全的。在这种情况下，学生自动机的可访问状态变为（初始化，第一次访问），而监督自动机保持在初始状态。一个反例：助理可以允许学生进行两次以上未经授权的访问。 这种适配将通过将令牌从P15（文档访问（警告后））向P9（文档访问）移动的转换来实现。但这种适应！回访P3？处罚InitP27！回访惩罚结束？警告P31？处罚！文件存取警告P18！回访！文件存取！处罚第二次访问P21？第二次禁止访问文档Init！警告？第一次禁止访问文档P13！处罚第一次访问C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）6983主管ECS文件存取P11第一次禁止访问文档doc-access（警告后）第二次禁止访问文档P24T35ECS主管文件-访问essss第一次禁止访问文档P10P36T34不符合我们的安全标准。事实上，令牌到达P9可能会导致令牌被放入P14（警告），而学生不再能够处理此令牌：转换T10未启用，因为学生在这种状态下，学生的网络中不会发生任何转换(a)更严谨的态度（b）更宽容的态度图五. PN的局部适应性5结论我们提出了一个框架，用于指定组件之间的协调，处理和检查这种协调的适应。特别是，我们定义了一个可计算的安全标准，它允许自动确定适应是否正确。此外，我们提出了一种用于检查和处理（动态）适配请求的模式，该模式进入了[14]中提出的更通用的框架。将我们的建议付诸实践需要考虑运营模式领域固有的限制和问题，即：• 适配安全性的验证涉及成本，因为必须对PN进行验证。这种验证是基于详尽的系统状态空间探索，其限制，一般来说，是那些模型检查。 适配的安全性验证可以从一致性检查的工作中受益[15]。 这可能会限制PN修改使得该分析根据PN大小保持可缩放• 缺乏模块化，这使得无法在比原始转换系统更高的抽象级别上设计适应性。 在实践的基础上，我们的方法是明智的，因为我们只考虑适应性的验证，84C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）69它是由程序员发现的，但它不如生成一组正确适应的方法吸引人。安全（适应）的概念既涉及复杂性，也涉及模块性，因为它旨在描述和验证本地化适应的影响，复合系统的一个组件（即Moderator）。本着这一精神，我们的做法可以几种方式延长• 通过定义一个更强的安全标准来表征安全适应，独立于角色，从而独立于透明度。该标准基于初始调节器和适应调节器之间的可替代性，将使得能够在本地检查本地适应。• 透明度可以用来检查参与者的适应（状态的任意改变）是否与现有的协调协议保持一致： 如果主持人的IPN相对于适应的角色是透明的，则新的（全局）系统符合初始系统。同样，我们有一种方法可以在本地检查本地适应。如果想要实现复杂的自适应，自适应的组成是另一个重要的问题：自适应可以在协调规则的初始定义中是安全的，并且在执行另一个自适应之后变得不安全。因此，必须通过比较主持人的“改编语言”（即协调加上已经整合的改编所产生的语言）与额外改编所产生的语言来检查安全性从软件工程的角度来看，我们的方法必须得到一套工具的支持，以便于检查设计的正确性，协调议定书的调整• 我们提供了一个从主持人的IPN生成角色自动机的工具• 出于可用性目的，应向程控仪提供安全分析的结果，以允许调试适配请求。• 更一般地说，程序员应该提供工具，使他能够评估适应对整体性能的影响[3]。最后，这一建议开辟了一条方法论途径;设计者可以指定一个基本方案，确保安全性能的核心， 一系列丰富的行为然后，可以以增量的方式引入特定的规则，作为适应。这可以提供一个平滑和灵活的设计过程。确认我们谨此感谢匿名评审人提出的建设性意见，这些意见对改进文件的内容大有帮助。此外，我们非常感谢Pascal Poizat在本文最后修订阶段的帮助C. Sibertin-Blanc等人/理论计算机科学电子笔记189（2007）6985引用[1] 艾伦河，巴西-地和D. Garlan，A Formal Basis for Architectural Connection，ACM Transactions onSoftware Engineering and Methodology6（1997），pp.213-249[2] Baldoni，M.，C. Baroglio，A. Martelli、V.Patti和C. Schifanella，《Web服务与全局交互协议的结合：第一 步 》 ， M 。 Bravetti 和 G. Zavattaro ， editors ， European Performance Engineering Workshop ，EPEW 2005 and International Workshop on Web Services and Formal Methods，WS-FM 2005，LNCS3670（2005），pp.257-271。[3] 贝克尔，S。和R. H. Reussner，软件组件适配器对服务质量属性的影响，在：C。Canal，J. - M. Murillo和P. Poizat，编辑，第一届软件实体协调和适应技术国际研讨会（WCAT105-125.[4] Burdett，D.和N.Kavantzas，WS编排模型概述，工作草案，W3C（2004）。网址http://www.w3.org/TR/ws-chor-model/[5] 运河角，J. M. Murillo和P. Poizat，Software Adaptation，9URLhttp://www.ibisc.univ-evry.fr/pub/basilic/OUT/Publications/2006/CMP06[6] 运河角，P. 波伊扎和G。 Sal au？n，Synchronizing Behaviour RMismatchinSoftwar re Composition，in ：Eighth IFIP International Conference on Formal Methods for Open Object-Based DistributedSystems（FMOODS'06 ） ，LN CS 4037 （ 2006） ， pp . 63比77[7] Castelfranchi，C. 社会秩序工程，在：A。A.奥米奇尼河Tolksdorf和F. Zambonelli，编辑，第一届国际工程学会在代理世界（ESAW 2000），LNCS1972（2000），页。1-18号。[8] 德 阿 尔 法 罗 湖 和 T.A. Henzinger ， Interface Automata ， in ： Proceedings of the Ninth AnnualSymposium on Foundations of Software Engineering，ACM Press，2001，pp.109比120网址http://www.gigascale.org/pubs/239.html[9] 戈顿岛G. T.海涅曼岛Crnkonic，H. W.施密特和J.A. Sta Baud，[10] 哈纳奇角和C. Sibertin-Blanc，Protocol Moderators as Active Middle-Agents in Multi-AgentSystems，Autonomous Agents and Multi-Agent Systems8（2004），pp.131-164。[11] Heineman，G. T.和W. T. Councill，[12] Issarny，V.，C. Kloukinas和A. Zarras，Systematic Aid for Developing Middleware Architectures，ACM Communications45（2002），pp.53比58[13] Murata，T.，Petri Nets：Properties，Analysis and Applications，Proceedings ot the IEEE77（1989），pp. 541-580[14] 波伊扎，P.，G. Sal auén和M. Tivoli，OnDynamicReconfigurationofBehavioralAdaptations，in：S.贝克尔角Carlos，N. Diakov，J. M. Murillo，P. Poizat和M. Tivoli，编辑，第三届软件实体协调和适应技术国际研讨会（WCAT61-69.[15] Rajamani，Sriram K.和Jakob的Conclusion Checking for Models of Asynchronous Message PassingSoftware。第14