服务编排的分析配置-观察界面理论

理论计算机科学电子笔记264（2010）125-139www.elsevier.com/locate/entcs一种分析服务配置的观察-观察界面理论菲利普·迈耶1 安德烈亚斯·施罗德2 塞巴斯蒂安·S 鲍尔3号Lehrstuhlfur？rogrammierungundSoftwar etechnikInstitutfur？rInformatik路德维希-马克西米利安大学，德国摘要面向服务的计算是开发大型分布式软件系统的公认体系结构风格。这种架构的一个特别的承诺是服务编排，即能够组合现有服务以创建更复杂的功能，从而产生新的服务。在本文中，我们讨论了应用程序级的服务编排和服务协议使用模态输入/输出自动机（MIOs）的语义域的协议符合性检查。基于一个实际的例子，我们激励和引入新的概念的细化和兼容性，并证明它们构成一个有效的接口理论。有了这个领域特定的接口理论，我们提供了一个应用程序级分析的框架服务编排的能力，从而补充了现有的兼容性分析工作。我们的理论是通过MIO自动机，模态输入/输出自动机的验证工具关键词：协议遵从性，接口理论，细化，兼容性，模态输入/输出自动机，SOA，服务，服务编排，服务协议，协议违反1介绍随着面向服务的体系结构（SOA）的出现，企业软件环境已经从专有的封闭组件的交互转变为称为服务的独立自描述组件之间的开放和标准化通信。在此上下文中，特别重要的是将各个服务组合成新服务，这被称为服务编排。使用来自模型驱动社区的技术，基于服务的系统可以用UML或其他用户友好的图形或非图形语言建模，然后转换为特定于平台的模型和代码。1电子邮件：mayer@pst.ifi.lmu.de2电子邮件：schroeda@pst.ifi.lmu.de3电子邮件：bauerse@pst.ifi.lmu.de1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.07.009126P. Mayer等人理论计算机科学电子笔记264（2010）125使用模型开辟了在开发过程早期验证系统正确性的可能性，设计问题可以更容易地处理。在本文中，我们对这种验证的一个方面感兴趣，即检查服务编排的协议遵从性我们的目标是通过在以下两个问题上提供帮助来支持最终用户，即SOA系统的开发人员：• 业务流程（实现）是否遵循特定的协议？• 两个协议是否兼容？为了回答这些问题，我们引入了一个正式的框架该理论必须能够满足以下要求：聚焦教育服务编排的特征在于它描述了多个现有服务的交互，从而形成一个或多个新服务。一般来说，编排使用许多现有服务，要求它们中的每一个都满足特定协议，这因此是编排所需的协议;其次，它本身也可以提供多种服务，从而导致提供多种协议一个管弦乐队。 我们感兴趣的是验证一个编排是否单独遵守每个协议，以及两个这样的协议是否兼容。 这与Knapp等人[18]的精神相同，他们在上下文中应用了相同的方法。 基于组件的软件工程。应用层协议漏洞分析在服务编排中正确实现给定的协议并不是一件容易的事情。因此，我们的目标是通过提供应用程序级协议漏洞分析来支持开发人员完成这项任务。这种类型的分析专门关注协议操作，这对应于开发人员感兴趣的抽象层。它明确地不涵盖较低级别的实现问题，如竞争条件。保证组合性第三，服务协议和编排的分析应该为开发人员提供一些切实的结果。面向服务的体系结构的一个要点是能够以最小的开销在不同的服务之间切换。因此，分析应该为我们提供保证，如果一个管弦乐队与某个协议一起工作，它可以与对应于同一协议的任何服务实现一起工作。这个属性被称为独立可实现性。P. Mayer等人理论计算机科学电子笔记264（2010）125127电子办学生<<使用辅导EOffice论文管理学生辅导老师我们在本文中的贡献是定义了一个适当的接口理论，用于检查服务协议和编排的协议符合性，它满足上述所有要求。我们已经成功地将这一理论应用于欧盟项目SENSORIA的几个案例研究[32]。 举个例子， 因此，我们使用了一个场景，从一个案例研究的森索里亚。我们在此展示的场景取自eUniversity领域，并对论文管理进行建模，即协调学生论文（学士，硕士，文凭）的过程图1. 服务编排图1显示了架构草图：编排（ThesisManagement）提供两个服务（Student和Tutor），并需要一个外部服务（EOffice）。其余部分的组织如下。在第2节中，我们回顾了接口理论的基本概念及其最重要的属性，此外，模态I/O自动机作为我们的方法的形式基础。然后，在第3节中，我们概括了弱模态修正的标准定义，它被证明不足以满足我们的需要。 作为一种补救措施，我们定义了一个新的精化概念称为严格观察模态精化，支持服务编排分析（3.1节）。我们以同样的方式（第3.2节）处理协议的兼容性：现有的弱兼容性的概念是不令人满意的，相反，我们定义了一个新的概念的兼容性，这是面向制定应用程序级协议的一致性。然后（3.3节）我们证明了新的精化和相容的概念与一个适当的复合算子一起构成一个有效的界面理论。在第4节中，我们将我们的方法与相关工作进行了比较。我们在第5节结束。2接口理论与模态I/O自动机在本节中，我们回顾了接口理论的基本原理，它们最重要的性质以及模态I/O自动机，它们将作为本文的具体领域。2.1界面理论由于我们的目标是检查服务协议和服务组织的协议遵从性，因此我们需要一种精确的方法来指定两个服务协议是否匹配（协议兼容性）以及实现是否正确地实现了其128P. Mayer等人理论计算机科学电子笔记264（2010）125∼⊗⊗∈A∼ ⊆ A × A ⊗A × A→IA ≤ 100A ≤ 100 × Aprotocol（refinement）.后一种精化概念也用于将抽象的和更具体的协议规范联系起来，即，它允许逐步精化 具体实施的协议。接口理论或接口语言通常用于精确定义这些概念。我们的界面理论的概念是受de Alfaro和Henzinger在[5，6]中的工作的启发接口理论是元组=（ 、、，）由特定域组成一个自反传递的精化关系，一个对称相容关系，以及一个部分复合算子* *如果两个界面是相容的，那么它们的组合被定义，即对于所有的S，T，如果S T，那么S T被定义。此外，界面理论对它们的细化和相容关系提出了以下要求：(1) 精炼时保持相容性对于所有的S，T，TJ∈A，如果S<$T且TJ≤T，则S<$TJ。(2) 组合性：对于所有的S，T，TJ∈A，如果ST被定义且TJ≤T，则STJ被定义且STJ≤ST。这些属性意味着独立的可实现性，这是服务和服务协议自顶向下设计的基础：为了将给定的组合接口S T细化到实现，它必须独立地细化S和T，比如分别细化为SJ和TJ;然后细化SJ和TJ是兼容的，它们的组合（定义）细化了接口ST。2.2模态I/O自动机模态I/O自动机（MIO）首先由Larsen等人引入[19]。 我们 选择了MIO作为我们接口理论的特定领域;它们为我们提供了支持服务协议和服务编排分析的形式化基础。尽管我们的接口规范中的模态 不一定需要在这项工作中，可能和必须模式的过渡建模允许和要求的行为，分别是有用的，代表标准化的合同，在我们的理论。定 义2.1 [ 模 态I/O 转 换 系统 [19]] 模 态 I/O 转 换 系 统 （ MIO ） S= （ statesS ，startS，（inS，outS，intS），−−·S，−→S）由一组状态statesS，一个初始状态startS∈statesS，输入、输出和内部转换的不相交集inS，outS，intS组成，其中extS=inSoutS表示外部动作集，actS=extSintS表示所有动作集;此外，可能转换关系−−·SstatesS×actS×statesS，必须转换关系−→Sstates S×actS×statesS，使得两个转换关系满足−→S−·S（语法一致性）。S被称为实现，如果−→S= −−·S。P. Mayer等人理论计算机科学电子笔记264（2010）125129MIOS的外部字母表（或签名）表示为αext（S）=（inS，outS）。两个给定的MIOS和T的字母相等和包含分别由分量相等和包含定义。模态I/O转换系统是一种特殊的模态转换系统，它在Larsen和Schmidt [21]介绍的原始形式中，不区分输入、输出和内部动作。两个应该相互通信的MIO的语法要求是，操作的重叠只发生在互补类型上。定义2.2 [可组合性[19]]两个MIO S和T被称为可组合的，如果（inSin tS）（inTin tT）=和（outSin tS）（out tTin tT）=。两个可组合的MIOS和T的共享标签集定义为：shared（S，T）=（outSinT）（inSoutT）。现有的界面理论，使用MIO作为规范域，包括各种细化和兼容性的概念[2，19，20，11]。 然而，正如我们在下一节中指出的，这些都不足以满足上面列出的要求。因此，我们补充这些现有的概念与一个新的接口理论，适用于检查服务编排。3一种检验服务协议一致性在这一节中，我们将介绍现有的模态精化和相容性概念，并给出严格观察模态精化和相容性的新定义。我们通过上面介绍的eUniversity领域的运行示例再次激发了这一点，这次建模为MIO，如图2所示。输入标签后加问号（？ ）和输出带有感叹号（！）的。图2. eUniversity的例子在图的中间偏右，显示了编排ThesisManagement，它提供了两个服务（左），每个服务都有自己的协议（Tutor和130P. Mayer等人理论计算机科学电子笔记264（2010）125SS ssSS学生），并需要一个外部服务EOffice（右;考试办公室）。工作流程如下。一个学生在写论文，提供最新情况。一旦她完成了，论文就被标记为完成，导师会对其进行评估不过，有一个在这种情况下，学生被告知问题。请注意，EOffice协议还指定了一个在编排中未实现的呼叫-这是协议赋予的3.1非观测模态修正我们首先尝试用现有的模态I/O自动机接口理论来分析这种服务编排。最接近我们自己对MIO的细化和兼容性的定义是弱细化和兼容性，并辅以隐藏的概念。在讨论界面理论之前，我们现在先介绍这些。[21]通常以一种逆变的方式定义模态加细。 模态细化的基本思想是，抽象规范中的任何必要（必须）转换也必须发生在具体规范中。相反，任何在具体规范中被允许的（可能的）转变，都必须被抽象规范所允许。此外，在这两种情况下，目标状 态 必 须 彼 此 一 致 。 模 态 细 化 有 以 下 后 果 ： 具 体 的 具 体 化 可 以 省 略 may-transitions，但需要保留所有must-transitions，而且不允许执行比抽象具体化所允许的更多的transitions。模态修正的基本形式要求，必须立即模拟所考虑的每一个过渡。 在许多应用领域，这种定义过于强烈[17]。它可以通过区分外部行为和内部行为，并允许外部行为被内部行为所包围而被削弱。在这种情况下，我们称之为弱跃迁。a为了表示弱转移，给定MIOS和作用a∈extS，我们写s−→sJi <$存在状态s1，s2∈状态S使得s（−τ→）<$s1−a→s2（−τ→）<$sJ其中t（−τ→）<$tJ代表无限多个跃迁，标记为内部作用，不导致从t到tJ;可能没有动作，并且在这种情况下t=tJ。在这里和以后，作用量τ总是表示任意的内部作用量。此外，我们写道s−a→nsJi）的J。这两种符号都类似地用于may转换。利用弱跃迁的概念，我们可以定义弱模态加细。44.我们将弱模态修正的定义[17]应用于MIO;此外，我们通过允许所考虑的MIO在其内部动作集合方面有所不同，略微概括了定义。SP. Mayer等人理论计算机科学电子笔记264（2010）125131S不S不S ssS定义3.1 [弱模态修正，改编自[17]]设S和T是MIO，使得αext（S）=αext（T）。S弱模态约束T，记为S≤mT，其中存在关系R→状态sS×状态sT，满足（S，T）使得对于所有（s，t）∈R，对于所有a∈actS<$actT，(i) 若t−a→tJ，则存在sJ∈状态sSsuch使得s−a→t∈sJ且（sJ，tJ）∈R，(ii) 若s− −a·sJ，则存在tJ∈状态such，使得t− −a∈·tJ且（sJ，tJ）∈R。不现在，让我们考虑检查我们的eUniversity系统：我们想评估编排是否真正遵守所有指定的协议。由于字母不兼容，第一次尝试检查细化失败-实现多个服务的编排总是比正在检查的服务协议有更多的操作。 这个问题的一个可能的解决方案是隐藏（参见，例如，[28]），即将不属于所审议议定书的所有行动内部化。然而，这仍然没有抓住我们应用程序级验证的意图。而不是检测可能导致死锁的错误，“non-relevant” actions, we are interested in protocol breaches that 业务流程无法遵循协议的情况因此，我们正在寻找的界面理论必须不同于上面讨论的界面理论。这在例子中可以看出：在弱精化下，编配不精化学生协议，即使隐藏，作为s.完成？ e.取消后不再可能？- 与学生协议无关的操作-已收到。细化分析将报告此问题，并隐藏更重要的错误，如灰色虚线/点线所示：第二个s.complete？消息在实现中是违反应用程序级协议的，作为s.完成？在s之后不允许。abort！在学生协议中，即使忽略“不相关”的行为。如果没有第二个s，完成？ 调用，我们想考虑编排学生协议的细化上述初始问题（s.完成？在E之后不可能取消？）不会被我们的精化概念检测到，这使我们能够专注于发现协议违规。这个问题可以使用其他分析技术来处理，例如建立在弱加强上的界面理论[2]。为了捕捉我们对应用程序级协议违规的想法，我们首先定义了弱动作转换的概念。给定一个MIOS，一组动作L表示S，aa（L）a若a∈actS，则记s−→sJi <$s−→SsJ或存在n≥1，s1，...，s n∈状态S，动作b1，...，b n∈（act S\L）使得s−b→1s1. . . sn−1−b→n sn−a→sJ。动作弱转移的直觉是执行单个相关动作，其之前可能是不在L中的不相关动作。此外，我们写道s−a→asJ，以表示s−a→a（extS）sJ。 同样的概念也被类似地用于S S可能的过渡。132P. Mayer等人理论计算机科学电子笔记264（2010）125不SS不S不我们现在调整弱模态精化来满足我们的需要，即我们只想要考虑在细化管理层指令时采取相关行动。我们改进的基本思想是跳过与正在研究的协议无关的前导操作。首先，细化的MIO可能比细化的MIO有更多的动作，其次，在定义的两个方向上，我们都关注更抽象的MIO的外部动作，因为这些动作是相关的。定义3.2 [非观测模态修正]设S和T是MIO，使得αext（S）<$αext（T）。 S严格观测地约束T，记为S≤soT，i ≠存在一个关系R∈状态S×状态T，包含（开始S，开始T），使得对所有（s，t）∈R，对所有作用a∈extT，(i) 如果t−a→atJ，则存在sJ∈态su ch使得s-a→a（extT）SJ且（SJ，TJ）∈R，(ii) 如果s− −a·a（extT）sJ，则存在tJ∈状态su ch，使得t− −a·atJ和（sJ，tJ）∈R。注意，严格观测精化仅使用MIO的模态方面，因此也可以定义为原始形式的模态转换系统（参见：[21]，不区分输入/输出/内部动作）。非观测模态加细可以被证明是MIO上的一个预序即它是自反的和传递的。引理3.3非观测模态加细≤ so是自反且传递的。这个引理的证明和所有随后的引理和定理可以在[27]中找到。回到我们的例子，我们有一个问题，在弱精化下，s.完备？呼叫被报告为错误，因为它在e.cancel之后不再被接受。. 通过严格的观察细化，e.取消？不再与学生协议和编配之间的细化检查相关。 因此，报告的唯一问题是由于s.complete？在图1B的编排中以虚线/点灰色二、3.2非观测I/O兼容性现在我们关注第二个目标，它涉及兼容性检查。 考虑图3，其是图2的复制品，然而这次具有之前给出的协议的补充。问题是协议是否与它们的补充兼容，以及协议是否与编排兼容。首先，让我们正式定义兼容性的概念。 作为与我们的方法最接近的匹配，我们引入了弱兼容性[2]，它通过要求输出（由可能或必须转换发出）必须与相应的输入（由必须转换发出）一起接受来缓和通常的强兼容性概念[19过渡），但这可能是内部行动之前5[5]由于技术原因，弱相容性的定义与[2]中的定义略有不同，但实际上是P. Mayer等人理论计算机科学电子笔记264（2010）125133需方案学生s.update！s.abort?s.完成！S不S一不编排论文管理s.update?e.cancel?s.complete?s.中t.assessment！兼容兼容兼容提供的方案EOfficee.取消！需方案辅导老师t.assessThesis?图3. 电子大学的例子（2）定义3.4 [弱模态相容性，改编自[2]]设S和T是可组合的MIO。 S和T称为弱模态相容，记为S<$wcT，i <$i存在关系R<$states S×statesT包含（startS，startT）使得对所有（s，t）∈R，aaa(i) 对于所有a∈（outS<$inT），如果s−−·sJ则<$tJ∈状态T.t−→tJ且（sJ，tJ）∈R，aaa(ii) 对于所有的a∈（outT<$inS），如果t−−·tJ则<$s j∈状态S.s−→sJ且（sJ，tJ）∈R，(iii) 对于所有的a∈（intS<$extS\shared（S，T）），如果s−−· SsJ则（sJ，t）∈R，(iv) 对于所有的a∈（intT<$ex tT\shar ed（S，T）），如果t− −a·TtJ则（s，tJ）∈R。使用弱模态兼容性，很容易看出我们示例中的协议及其补充（图1和图2）。2和3）是兼容的。然而，我们的目标是在细化下保持兼容性-不幸的是，使用弱模态兼容性检查Student协议与编排产生了类似的违规行为，正如我们之前在讨论细化时所观察到的那样：在采取e.cancel之后？transition，它在业务流程的外部，但不与协议共享，即s.update？协 议 的 转换不能再进行。这个问题不能通过隐藏来缓解，因为隐藏不会以任何相关的方式消除弱模态兼容性（将外部标签移动到内部，参见定义3.4，（iii）和（iv））。相反，这个想法是减少在兼容性检查期间考虑的状态对的集合。同样，我们希望考虑所有三个协议都与orchetration兼容，在每种情况下只考虑协议可观察的动作。我们定义了严格的观测I/O兼容性来实现这一目标。定义3.5 [可观察I/O兼容性]设S和T是可组合的MIO，设L是S和T的共享标签的集合shared（S，T），T. S和T被称为严格观测I/O兼容的，记为S<$soT，i <$存在关系R<$states S×statesT包含（startS，startT）使得对于所有（s，t）∈R，134P. Mayer等人理论计算机科学电子笔记264（2010）125S不不SIMIO≤10000⊗1S1S11S112S2S22S1 S212121S112S2S22S22S1 S21212TSaa（L）(i) 对于所有的a∈（outS∈inT），如果s−−· sJ，则存在tJ∈态使得t−a→a（L）tJ且（sJ，tJ）∈R，(ii) 对于所有的a∈（out_in），如果t−−a·a（L）tJ，则存在sJ∈状态使得s-a→a（L）SJ且（SJ，TJ）∈R.再次考虑编排和学生协议之间的兼容性的例子，严格观察I/O兼容性对待e.cancel？和t.assessThesis！不同的是，这两个动作都没有在学生协议中定义。只作为终止的前缀！，而t. assessesis！ 根本不被考虑。因此，正如预期的那样，我们在ThesisManagement和Student引理3.6非观测I/O相容性3.3界面理论有了严格的观测模型细化和兼容性，我们现在可以回到我们最初的目标，即定义一个特定于领域的接口理论，旨在检查SOA系统中的协议遵从性为了证明MIO与严格观测模态精化和严格观测I/O相容性一起形成了一个界面理论，我们需要一个适合于我们严格观测观点的MIO复合概念，称为严格观测复合，用so表示。 然后我们 事实上，所以=（，所 以，所 以， 所以），其中是所有模态I/O自动机的域，满足兼容性和组合性的保持。定义3.7 [可观察组合]两个可组合的MIOS1和S2可以在严格观测上组成MIOS1和S2，定义为：• 状态S1→S2=状态S1×状态S2，• 开始S1→S2=（开始S1，开始S2），• inS1soS2=（inS1\outS2）（inS2\outS1），• outS1soS2=（outS1\inS2）（outS2\inS1），• 在测试中，S1= 0，S2=0。过渡关系由下式给出：(i) 对所有ai∈ashared（S1，S2），1≤i≤n，若存在c∈（extS1shared（S1，S2））a a a a，则s−a→1 . −a→nsJ−→csJ J，且s−a→1。 . −a→nsJ，则（s1，s2）−→c（sJJ，sJ）（如果n=0，则s1=sJ并且s2=SJ），(ii) 对所有ai∈ashared（S1，S2），1≤i≤n，若存在c∈（extS2shared（S1，S2））一，则s−a→1 . −a→nsJ，且s−a→1a. . . −a→nasJ−→cASJJ，则（s1，s2）−→c（sJ，sJJ）（如果n=0则s1=sJ并且s2=SJ），(iii) 和（iv），两个类似的五月转移规则（−−·）。S1不SP. Mayer等人理论计算机科学电子笔记264（2010）125135⊗这个复合运算符的直观含义是捕获非共享外部动作c，它可以由多个共享动作a1..a n（或根本没有）：任何只涉及具有共享标签的转换的路径在组合中不会显示为同步动作;事实上，组合S1和S2根本不包含任何内部动作。特别地，不兼容的两个组成的MIO的任何通信故障（即，未接收到共享输出）不会出现在组成的MIO中。非观测复合满足结合性和交换性，这是任何合理复合算子的基本要求6引理3.8非观测合成是交换的和结合的。首先，我们证明了严格观测相容性在严格观测模态修正下是保持的。定理3.9 [相容性的保持]设S，T，TJ是MIO，且S，T和S，TJ是可组合的. 如果S ≠soT，T J≤soT且shared（S，T）= shared（S，T J），则S≠soTJ。组合性是服务的独立可实现性及其模块化验证的先决条件。7定理3.10 [组合性]设S，T，TJ是MIO，且S，T和S，TJ是可组合的。 若TJ≤soT且shared（S，T）= shared（S，T J），则S <$soT J≤soS <$soT。独立可实现性是在细化和细化组合下保持兼容性的直接结果。与传统的软件架构相比，SOA系统从这一属性中获益更多，因为在基于服务的应用环境中，服务和编排是固有的分布。推论3.11 [独立可实现性]设S，T，TJ是MIO，且S，T和SJ，TJ是可组合的。若S<$soT，TJ≤soT，SJ≤soS且shared（S，T）= shared（SJ，T J），则SJ<$soT J和SJ<$soT J≤so S <$soT都跟随。首先，可以很容易地证明，shared（S，T）= shared（S，T J）= shared（SJ，T J）。通过Thm。3.9，它遵循SoTJ，并由莱姆。3.6，T.又是Thm。3.9和莱姆3.6，它遵循SJsoTJ。其次，我们证明了SJ<$soTJ≤soS<$soT。我们应用Thm。3.10得到SsoTJ≤soSsoT。此外，由Thm。3.10，它遵循TJ<$soSJ≤soTJ<$soS。因为Because3.8）和≤sotransitive（Lem.3.3），则SJ<$soTJ≤soS<$soT.Q6为了保持交换性，我们假设两个MIO被认为是相等的，如果它们具有相同的（内部和外部）字母表，并且在状态空间之间存在双射，使得可以和必须保持转移关系。7有趣的是，请注意，如果αext（T）=αext（TJ），则SsoTJ≤soSsoT等价于SsoTJ≤m其中≤m是强模态修正[21]。136P. Mayer等人理论计算机科学电子笔记264（2010）125IMIO≤100这结束了我们的工作，形成一个适当的接口理论的服务编排的协议符合性检查。正如我们用实际例子所说明的，so=（，so，so，so）确实是用于检查服务协议和编排的细化和兼容性的合适的语义框架。严格观察接口理论为SOA开发人员提供了一种工具，用于检查应用程序级别上的协议实现和兼容性，可以在现有接口理论之外使用，例如构建在弱细化和兼容性上。我们已经在MIO表示[2]中实现了严格的观察细化、兼容性和组合，这是一个基于验证的工具，包括一个MIO编辑器，能够直接在图形化的MIO表示上描述关系和有问题的路径。工作台还实现了细化和兼容性的标准概念（强、弱和可能弱的细化以及强、弱和友好的环境兼容性，参见。[2，19]），这允许直接比较各个接口理论。MIO工作台可以从http://www.miowb.net/。4相关工作界面理论的一般研究是由de Alfaro和Henzinger在[5，9]中开始的。他们著名的接口理论称为接口自动机，基本上建立在输入/输出自动机的形式上[24，25，14]，伴随着精化（由交替模拟定义）和兼容性的概念[4]。 该理论最近被推广到基于模态输入/输出转换系统[19，20]的界面理论，该理论使用模态自动机[21，17]来建模界面行为。然而，较少关注具有不同字母表的接口之间的细化。最近，[29，30]中提出的方法通过将新动作的自循环添加到自动机的所有状态来处理字母表扩展。 很容易看出（与3.1节中给出的论点相同），不足以应付我们的情况在[11]中，Fischbein等人提出了模态转换系统的分支字母表精化，以解决弱模态精化所允许的非直观实现问题。然而，它们的细化是经典的，因为它考虑了前提条件中的单个转换，这对我们的应用领域来说太严格了动作细化[15]是一个灵活的细化概念，它基于在改变抽象级别时细化动作：抽象规范的动作可以分解为一系列更详细地指定系统的低级别动作我们与这个概念不同，因为我们所有的动作都驻留在同一个抽象层上，但我们只考虑其中的一些，这取决于当前的观点。还有一个关于语义的广泛的知识体系，以及基于行业标准（如XML）的Web服务编排分析; [31]提供了一个不错的概述。然而，据我们所知，到目前为止，还没有一种方法将早期应用程序级验证视为现有方法的先驱。 相反，重点在于分析服务编排的特定方面[22]和P. Mayer等人理论计算机科学电子笔记264（2010）125137[26]通过向Petri网的转换来分析网络的组成。他们的组合分析假设了[4]意义上的友好环境，但并不适合服务编排的应用程序级分析。 Fu等人[13]目前将一个编译过程的组合翻译成Promela（输入语言）SPIN模型检查器[16]。然而，由于翻译的交互语义，应用程序级验证是不可行的。另外两种更接近我们的方法使用演算来指定底层的标记转换系统：[3]明确地关注于遵从性和兼容性的强概念。对于像[10]这样的基于计算的模型检查方法，与[13]的方法相同的推理适用：应用程序级验证被语言的组合语义所禁止。关于工具支持，MIO通过明确考虑MIO的模态和输入/输出方面，从现有工具（如MTSA [7，8]，TICC [1]或Tempo [23]）中分离。与SOA验证工具（如WS-Engineer [12]）相比，MIO验证工具更具实验性：基于直接作为MIO给出的输入，它允许应用不同的（可插入的）接口理论来研究模型和理论本身。5结论大型分布式软件系统的开发越来越多地进行 通过使用面向服务的体系结构，其中服务形成系统的基本构建块，以组成新的服务，这是一个称为编排的过程。 通过使用模型驱动的方法进行SOA开发，服务和服务编排在开发过程的早期就可用，在那里可以对它们进行分析和验证，以提高整体系统质量。在本文中，我们研究了服务编排的协议一致性检查。我们特别关注检测协议违规，允许服务工程师直接在应用程序级别上使用他们的模型。我们的方法是基于模态I/O自动机的语义域，并支持一个新的接口理论，我们称之为严格观察，因为它的重点是从某个协议的角度来看外部可见的行为。 我们已经给出了这个理论的形式化定义，并证明了它确实构成了面向服务系统的特定领域形式化分析的有效接口理论我们成功地使用了严格的观察细化和兼容性，检查欧盟项目SENSORIA的案例研究。一组例子，以及通过MIO服务器提供的完整工具支持，http://www.miowb.net网站。作为将来的工作，我们打算把严格观测理论纳入我们在[2]中已经讨论过的界面理论的更大框架138P. Mayer等人理论计算机科学电子笔记264（2010）125确认本研究得到了德国联邦教育和研究部赞助的GLOWA-Danube项目01 LW 0602 A2和EC项目SENSORIA，IST-2005-016004的部分支持。我们感谢罗尔夫·亨尼克和斯蒂芬·贾尼施提供的宝贵提示富有成效的讨论。此外，我们也感谢匿名评论者的有益评论。引用[1] B. Thomas Adler 、 Luca de Alfaro 、 Leandro Dias da Silva 、 Marco Faella 、 Axel Legay 、 VishwanathRaman和Pritam Roy。 Ticc：一个界面兼容性和组合工具。 托马斯·鲍尔和Robert B. Jones编辑，第18届国际计算机辅助验证会议，CAV 2006，第4144卷 LNCS，第59Springer，2006.[2] 塞巴斯蒂安·S Bauer，Philip Mayer，Andreas Schroeder，and Rolf Hennicker.论弱模态相容性、再细化和MIO矩阵。 第16届国际会议，系统构建和分析的工具和算法，TACAS 2010，2010。出现。[3] 马里奥·布拉维蒂和吉安路易吉·扎瓦塔罗。 一个强大的服务合规理论。 在艾米湖，墨菲和Jan Vitek，编辑，第9届国际会议协调模型和语言，协调2007，LNCS第4467卷，第96Springer，2007年。[4] Luca de Alfaro和Thomas A.亨辛格接口自动机。软件工程笔记，第109-120页[5] Luca de Alfaro和Thomas A.亨辛格界面理论为基础的设计。在Thomas A. Henzinger和Christoph M.Kirsch编辑，第一国际研讨会嵌入式软件，EMSOFT 2001，LNCS第2211卷，第148施普林格，2001年。[6] Luca de Alfaro和Thomas A.亨辛格基于界面的设计。在Manfred Broy，JohannesGruünbauer，D avidHarel和C.A. R. Hoare，编辑，软件密集型系统的工程理论，NATO科学系列的第195卷：数学，物理和化学，第83-104页。Springer，2005.[7] Nicol'asD'Ip polito，Dario Fis c h b ein，Marsha Che c hik，and Sebasti' an U c hitel.MTSA：模态转换系统分析器。第23届国际自动化软件工程会议，ASE 2008，第475-476页。IEEE计算机学会，2008年。[8] Nicol'asD'Ip polito，Dario Fis c h b ein，H o ward Foster，and Sebasti' an U c hitel. MTSA：Eclipse支持模态转换系统的构建、分析和细化。Li-Te Cheng，Alessandro Orso和Martin P. Robillard，编辑，OOPSLAWorkshop Eclipse Technology eXchange，ETX 2007，第6-10页。ACM Press，2007.[9] 放大图片作者：Thomas A. Henzinger，Barbara Jobstmann，and Tatjana Petrov. 接口理论与构件重用。在 Luca de Alfaro 和 Jens Palsberg 编 辑 的 第 8 届 国 际 嵌 入 式 软 件 会 议 上 ， EMSOFT 2008 ， 第 79ACMPress，2008.[10] Alessandro Fantechi，Stefania Gnesi，Alessandro Lapadula，Franco Mazzanti，Rosario Pugliese，andFrancesco Tiezzi.用于验证COWS规范的模型检查方法在j.L. 菲亚代罗和P. Inverardi，编辑，11th Int. Conf. 软件工程的基本方法，FASE 2008，LNCS第4961卷，第230-245页。Springer，2008.[11] 达里奥·费斯是个好人维克多·A。 Bra berman和Sebasti'anU chitel。模态转换系统的一种可靠的观测语义学。Martin Leucker和Carroll Morgan编辑，第6届国际学术讨论会计算理论方面，ICTAC 2009，LNCS第5684卷，第215Springer，2009年。[12] 霍沃德·福斯特、塞巴斯蒂安·乌奇特尔、杰·马吉和杰·克莱默。WS-Engineer：AModel-Based Approachto Engineering Web Service Compositions and Choreography.在Luciano Baresi和Elisabetta Di Nitto编辑的Web服务测试和分析中，第87Springer，2007年。[13] Xian Fu，Tev fik Bultan，and Jianwen Su.交互式Web服务分析。在第三届Web服务国际会议上，ICWS2004，第621IEEE计算机学会，2004年。[14] 斯蒂芬·J·加兰和南希·林奇。 使用I/O自动机开发分布式系统。 在在加里·T。 Leavens和MuraliSitaraman，编辑，基于代理的系统的基础，第285-312页。剑桥大学出版社，2000年。P. Mayer等人理论计算机科学电子笔记264（2010）125139[15] 罗伯托·戈列里和阿伦德·伦辛克。动作精炼。在J.A. Bergstra，A. Ponse和S. A. Smolka，编辑，Handbookof Process Algebra，第16章，第1047Elsevier，2001年。[16] 杰 拉 德 ·J· 霍 尔 茨 曼 。 SPIN Model EQUIPMENT ： Primer and Reference Manual （ SPIN ModelEQUIPMENT：Primer and Reference Manual）Addison-Wesley Professional，2003年。[17] HansHüttel和KimGuldstrandLarsen。静态结构在现代过程逻辑中的应用。在阿尔伯特河Meyer和MichaelA.Taitslin，编辑，Symp。计算机科学的逻辑基础，Logic at Botik 1989，LNCS第363卷，第163-180页。Springer，1989年。[18] Alexander Knapp 、 Stephan Janisch 、 Rolf Hennicker 、 Allan Clark 、 Stephen Gilmore 、 FlorianHacklinger、Hubert Baum