基于类型π-演算的移动分布式系统体系结构描述语言（ADL）及其应用-论文摘要要点总结.

理论计算机科学电子笔记150（2006）51-60www.elsevier.com/locate/entcs基于类型化π-演算VolkerGruhn1，Cl em ens Scha？fer2应用电信/电子商务主席3德国莱比锡大学数学与计算机科学学院摘要本文提出了一种基于类型π演算的移动分布式系统体系结构描述语言（ADL）。与其他方法不同的是，非功能属性，这是必不可少的，当移动架构进行描述，处理在一个灵活的方式，通过插入逻辑公式来表达和检查非功能属性到类型π演算过程。给出了一个正式的例子来说明该方法之前的ADL的组成部分勾勒。保留字：规范，要求，模型检查，移动系统，ADL1动机使用特定领域的体系结构描述语言（ADL）对移动分布式系统的体系结构进行建模被认为是一种有用的方法[2]，因为移动性的影响强调了检查软件体系结构的功能属性以及非功能属性的必要性。这对应于这样一个事实，即“流动性代表着所有稳定性假设的彻底崩溃......与分布式计算相关1Email：gruhn@ebus. 我是为了我自己。你好，我是说你好。De2Email：schaefer@ebus. 我是为了我自己。你好，我是说你好。De3应用电信/电子商务的主席由德国电信公司提供。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.02352诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）51构建移动分布式系统。这些问题的例子是网络结构，不再是固定的，节点可以来来去去，由于无线网络上的链路丢失而导致的通信故障，或由于移动通信链路的低带宽而导致的连接受限。这些都有一个共同点，即它们都关注系统的非功能属性，如性能、鲁棒性、安全性或服务质量。除了非功能属性之外，移动系统的这些固有挑战还可能影响系统的功能方面，因为移动系统可能必须提供额外的功能（如复制设施、缓存机制等）。以确保在出现上述问题的情况下的可用性。我们的ADLCon Moto（意大利语为第二章导言ADL是多年来的研究领域。通常认为，ADL包括三个基本组成部分：组件、连接器和配置[6]。粗略地说，组件对执行计算或存储数据的软件系统的实体进行建模，连接器对组件的交互进行建模，而配置是组件和连接器的连接图。基于这种理解和前面给出的动机，我们可以列出移动分布式系统ADL的要求：• 移动ADL必须能够对系统的动态方面进行建模，例如组件的动态实例化或系统执行期间通信链路的变化。• 移动ADL应该能够对具有非功能属性（如可靠性或带宽）的不同通信信道进行建模。这对于分析系统和发现连接失败时可能出现的问题是必要的。因此，可能需要专门的连接器。• 一个移动ADL应该允许非功能属性的组合，以便能够模拟复杂的依赖关系，这是突出的移动分布式系统。• 一个移动ADL应该是正式的基础上，使模拟和推理的模型是可能的。我们将努力满足这些要求。本文件其余部分的结构如下。在概述了第一节中的相关工作诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）51533中，给出了π-演算的介绍（4.1节），作为4.2节中的正式示例的基础，该示例说明了我们考虑的核心概念。在描述了Con Moto（第5节）中正式模型的使用后，得出结论。3相关工作在过去的几年里，ADL一直是研究的主题。Shaw和Garlan [12]已经认识到在架构描述中对非功能属性建模的必要性。Med-vidovic和Taylor [7]的分类工作对现有ADL的属性进行了合理的汇编。从他们的工作中可以明显看出，没有一个ADLs适合于对移动系统的动态方面进行建模。在过去，这一事实导致最近提出的移动ADL的发展。ArchWare项目及其π-ADL [9]是这些努力的结果之一。另一种移动ADL可以在Issarny等人的作品中找到。[4]。两者都基于Milner的π演算[ 8 ]提出了移动系统的ADL这两个ADL的共同点是它们能够对移动系统的动力学进行建模，这是由于它们在π演算中的理论基础。虽然它们在阐述和工具支持方面有所不同，但从本文的角度来看，根本的区别是对非功能属性的处理，这在π-ADL方法中是不存在的。Issarny等人在他们的工作中解决了非功能属性，但是非功能属性的处理绑定到全局一致性条件，该条件必须适用于分配给组件和连接器的预定义非功能属性集，并且不允许非功能属性的组合，这在我们的方法中是新颖的。目前，在软件系统的非功能属性领域还有其他研究。这项工作主要基于Lamport Zschaler [14]提出了基于组件的系统的时间特性的规范，但是这些以及Aagedal [1]的基础工作，其中提出了将TLA+方法集成到架构描述中，在我们的上下文中没有进一步考虑，因为TLA+中的模型缺乏对移动性的支持4系统模型4.1使用π演算类似于Issarny等人的方法[4]，我们将Con Moto建立在面向服务的交互范例之上，即.组件抽象网络服务54诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）51其调用对等组件的操作并双重执行所调用的操作。过程是掌握体系结构描述的功能方面的基础。由于我们使用Milner[11]第一：π演算中最简单的实体是名字。 这些可以被看作是通信链路的名称，并被进程用于交互。这些过程通过执行操作而发展。行动能力用前缀来表示，我们使用三种前缀4：（1）π：：=x（y） | x（z） | [x=y] π。第一个功能是通过名称x发送名称y，第二个功能是通过x接收名称。第三个是条件能力：如果x和y是相同的名称，则能力为π。π演算的过程和求和由下式给出：(2)P：：= M | P|PJ|！P（三） M：：= 0| π.P | M+MJ|1.一、语义如下。 0表示不行动，前缀π。P表示在π被执行后P可以被执行;和M + M J模拟一个选择，组合P |P J被称为parallelism。P表示复制。1是我们自己的一个扩展，并且具有“虚拟”过程的概念它总是可以被执行，并且不执行任何操作。我们需要这个扩展在我们后面的例子中。5然而，对于非功能属性的建模，仅仅在进程之间交换名称是不够的。因此，我们使用了多元π演算，它扩展了一元π演算，使得元组可以通过动作而不是名称来传递。这将导致以下前缀（4）π：：=x（y）|x（z）|[x=y]π，wherennonamesoccurrmoretthannc e n nceintin 在下面的例子中，我们将使用这个多元π演算和类型来说明我们的核心思想。稍后我们将使用π演算符号中的记录来建模非函数属性。[11]我们使用下面的记录定义。给定一组类型T1，.，T n.然后，记录类型具有以下形式(5){11：T1，.，I n：T n}，[4]为了简短，我们省略了不可观测的作用量τ和名称的结合。[5]虽然1在形式上对于我们的建模目的不是绝对必要的，但它增强了后面示例的形式上，我们为我们的“虚拟”过程定义以下反应诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）5155组分BpublicvoidonlineZbuy（）组分A其中所有的标签L1是不同的。 值的形式为(6){l1= v1，...，ln= v n}，其中每个vi是场i的值。我们现在可以对非功能属性建模，如下所示：（七）defT serviceA={availability：real，resourceConsumption：real}.在这个例子中，定义了一个名为TserviceA的非功能属性的类型，它包括两个元素，可用性和资源消耗;两者都被认为是实数。4.2形式示例在Issarny等人的工作中。[4]，我们使用π演算中给出的过程来表达我们架构的功能属性。现在我们将过程扩展到非功能属性。这种方法背后的核心思想是，我们流程中的每个操作都可以返回其非功能属性，如执行时间，内存消耗，可用性等。我们现在将介绍两个组件及其服务，并将展示如何处理它们的非功能属性。然而，我们只展示了对抽象的非功能属性的处理，因为具体的属性会增加形式的复杂性，但不会有助于核心思想。Fig. 1. 类UML表示法假设下面的场景：如图1所示，我们有两个组件A和B。A操作服务buy（），而B操作服务reserve（）和commit（），它们随后在buy（）的执行过程中被调用。由于reserve（）和commit（）具有一定的非函数属性集，因此直观上很明显，buy（）的非函数属性应该是reserve（）和commit（）属性的组合如果我们抛开所有其他方面，A和B，我们用一元π-演算来写def（八）（九）P B= reserve（x）.reserve（x）. 0 |commit（x）.commit（x）. 0def一 =buy（x）.reserve（x）.reserve（x）.commit（x）.commit（x）.buy（x）. 0流程PB模拟组件B的行为，流程PA模拟组件A的行为。对于服务buy（）的调用（我们假设它是通过buy（x）读取一个值来建模的），P56诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）51组件答：{提供需要{{buy（）publicvoidonline（）nfprop确保αβJγJ：Tα，in→Tα，out：TβJ→bool：TγJ→bool}}}组件乙：{提供{reserve（）nfprop β：Tβ，in→Tβ，outreturn（）nfprop γ：Tγ，输入→Tγ，输出}连接器Z：{需要{}}nfprop ζ：T，in→T，out }图二. 文本符号组件B中的进程，它对reserve（）的调用进行建模。在reserve（）返回（输入操作reserve（x））之后，类似地调用commit（）。最后，buy（）返回。这由输出buy（x）建模。我们现在介绍非功能性的属性。其思想如下：每个服务在终止时返回其非功能属性。在图2的文本表示法中，关键字nfprop表示计算给定服务的非功能属性的函数（例如，α（）求值buy（）的非函数属性。这些函数是为组件提供的所有服务定义的，这些服务列在关键字provides之后。由于在整个执行过程中必须检查的系统（这是指在Issarny等人的工作中的全局一致性条件我们还为组件所需的每个服务引入一个函数（在示例中由关键字requires指示），该函数掌握服务的非功能性需求，因此如果满足这些需求，则这些函数也在关键字ensure之后的示例中给出。在我们的示例中，βJ（）对组件A中的reserve（）的非功能性需求进行建模。 为了完整起见，我们现在还对连接器Z进行建模，通过它调用B的服务。这个连接器也有一个函数functional（）来确定它的非功能属性。对于由关键字nfprop给出的建模非函数属性的函数，输入和输出类型在签名函数名中给出：参数类型→结果类型。对于检查非函数属性的函数（关键字确保），使用结果类型bool，bool={true，false}。布尔值true和false用于π演算过程中的条件表达式。现在我们将计算和检查非函数属性的函数集成到示例8和示例9中：诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）5157PJJPJJγ，输出，输入(10)PJdef reserve（x）.reserve（x，β（））. 0|commit（x）.commit（x，γ（））. 0B=defA =买入（x）。Jreserve（x）. reserve（tx，p：Tβ，o utx）. [β（p：TβJ）]1.commit（x）.commit（x，q：Tγ，out）. [γ（q：TγJ）]1.（11）buy（x，α（p，q：T α，in））. 0现在，reserve（）像以前一样被调用。然而，reserve（）返回一个元组，名称x和前面一样，它的非功能属性p。现在，在buy（）的执行中，检查需求βJ是否对属性p成立。如果是这种情况，则可以通过执行“虚拟”进程来继续该进程1.一、对commit（）执行相同的两个步骤。最后，计算函数α以检索buy（）的组合非函数属性，并在扩展输出语句中返回在图2中，我们将输入类型和输出类型与计算非函数属性的所有函数相关联。为了说明公式中使用了哪些类型，使用了符号v：T，其中v是名称、元组或记录，T是类型。然而，由于式11中的组成，以下类型的等式必须保持一致以全部显示该组成：Tβ，ut=TβJ，Tγ，ut=TγJ，并且Tβ，ut，Tγ，ut=Tα，in。如果我们想对连接器Z的影响进行建模，我们必须使用它的传递函数（）并将其应用于reserve（）和commit（）返回的非函数属性，即我们必须分别用（p）和（q）替换所有出现的p和q因此，我们的过程从11转换为defA =买入（x）。reserve（x）.reserve（x，p：Tβ，out）。[βJ（p：T））] 1.commit（x）.commit（x，q：T）. [γJ（τ（q：T））] 1.（12）buy（x，α（（p：T，in），（q：T，in））. 0除了应用于公式11的类型约束之外，这里在公式12中，为了实现该组合，必须遵守以下类型约束：Tβ ， out=T ，in，Tγ ，out=T ，in，T ， out=TβJ=TγJ Tα，in=Tα，out，Tα，out。比较公式9和公式12，我们可以看到组件A行为的纯函数建模可以演化为一种规范，其中包括抽象的非函数属性，允许它们的组合和检查。这是通过随后应用转换步骤和丰富正式的功能规范来实现的。在58诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）515在Con Moto在下面的部分中，我们将讨论如何在ADL Con Moto中使用所提出的非功能特性建模方法在这里，软件系统的模型需要以文本的形式给出，如图2所示。然而，为了简化系统组合，Con Moto还将提供基于UML 2.0概念的图形表示，图1给出了一个UML风格的架构图的例子。在文本表示中，还需要表达系统的功能属性，因此需要调用过程，这些过程可以编译为我们在示例中使用的π演算过程。这是必须由系统设计人员完成的工作，因为功能方面对于移动系统的建模至关重要。此外，设计者还必须提供计算和检查非功能属性的功能.在我们的示例中，过程的组成可以通过Con Moto环境自动完成，因此对于设计师来说，功能和非功能方面之间有明确的分离，以便将建模复杂性保持在较低水平。在Con Moto环境将函数和非函数属性组合成丰富的π演算规范之后，就有了允许检查的模型。检验π-演算模型的某些特性的一种通用有效方法有相当直接的转换，允许从π演算模型生成模型检查器的输入。在宋和康普顿的工作中提出了一种这种变换。他们提出了一种将π演算模型转换为SPIN模型检查器使用的Promela语言的形式化方法[3]。虽然Song和Compton在他们的论文中把它们的变换限制在一元π-演算上，但对多元π-演算和类型π-演算的推广是可能的。我们对非函数性质的积分条件的方法也可以添加到[13]中提出的方法中。虽然应该标记，但将自由条件映射到Promela使得该语言的限制适用于我们的条件。 但我们有信心，Promela的功能足以满足我们的建模目的。应该强调的是，我们还没有就模型检查对Con Moto模型的复杂性做出任何结论。可以很容易地想象，选择某些非功能性属性定义可能会导致模型检查器中的状态爆炸，从而检查模型诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）5159不可能的然而，由于模型的Promela表示也允许模型的仿真，因此架构的某些方面也可以通过仿真来检查。6结论我们提出了一个形式化的基础，在架构描述的非功能属性建模。对研究的主要贡献是它促进了对非功能属性的一般处理，确保了组合性方面和灵活性检查，这为指定移动动态系统提供了一个强大的工具在激发我们的方法之后，我们证明了在类型化π演算过程中传递非函数属性是可能的。由于我们丰富了这些过程与检查条件，它是可能的，以延长现有的方法与一般治疗的非功能性的特性，从而为我们的ADL Con Moto的基础。目前正在进行的工作是详细说明所选方法的形式基础：该方法必须以合理的形式化方式写下来，并且必须证明ππ演算到Promela的映射，目前已经完成，必须完成以提供工具支持。此外，一个Eclipse插件正在工作，它将允许将Con Moto的架构建模集成到公认的开发过程中。综上所述，我们有信心，这些贡献可以为移动系统设计的早期阶段引用[1] 扬·阿吉达尔。分布式系统开发中的服务质量支持。博士论文，奥斯陆大学，2001年。[2] VolkerGruhnand d Clem ennsS cha？fer。一种用于移动分布式系统的分布式描述语言。第一届欧洲软件架构研讨会论文集（EWSA 2004），第212-218页Springer-Verlag Berlin Heidelberg，2004.[3] 杰拉德·J·霍尔茨曼。《自旋模型》（The Spin Model）：入门与参考手册。艾迪生-韦斯利，2004年。[4] Val'ereI ssar ny，FerdaTart an oglu，Jin sh anLi u，andFranpeculoiseSail h a n. 面向移动分布式计算的SofTwareArchiteture第四届IEEE/IFIP软件架构会议（WICSAIEEE，2004年。[5] 莱斯利·兰波特TLA+语言和工具，硬件和软件工程师。Addison-Wesley，2002年。[6] Nenad Medvidovic和David S.罗森布鲁姆软件体系结构中的关注领域。1997年USENIX领域专用语言会议论文集，1997年。60诉格鲁恩角Schäfer/Electronic Notes in Theoretical Computer Science 150（2006）51[7] 作者声明：Richard N. Taylor.软件体系结构描述语言的分类和比较框架。IEEE软件工程学报，26（1）：70 -93，2000年1月。[8] 罗宾·米尔纳通信和移动系统：π-演算。剑桥大学出版社，1999年。[9] 弗拉维奥·奥肯多π-ADL：一种基于高阶类型π-演算的体系结构描述语言，用于支持动态和移动软件体系结构。ACM Software Engineering Notes，2004年5月29日。[10] Gruia-Catalin Roman，Gian Pietro Picco和Amy L.墨菲移动性软件工程：路线图。软件工程未来会议论文集，第241-258页北京：人民出版社，2000年。[11] 大卫·桑吉奥吉和大卫·沃克。π演算：移动过程理论。剑桥大学出版社，2001年。[12] 玛丽·肖和大卫·加兰软件体系结构中的公式化和形式化。Jan van Leeuwen，编辑，ComputerScience Today：Recent Trends and Developments，计算机科学讲义第1000卷，第307-323页Springer，1995年。[13] 作者声明：John J.由Promela Translation编写的π-演算过程。技术报告CSE-TR-472-03，密歇根大学，2003年。[14] Ste daughen Zschaler.基于组件的软件的非功能属性的形式化规范。摘自Jean-Michel Bruel、GeriGeorg 、 Heinrich Hussmann 、 Ileana Ober 、 Christoph Pohl 、 Jon Whittle 和 Ste EschenZschaler，编辑，2004年UML会议上的基于一致性的软件的非功能方面模型研讨会（NfC