使用断言提高Kmelia组件的规格和开发

理论计算机科学电子笔记263（2010）5-30www.elsevier.com/locate/entcs使用断言来提高Kmelia组件及其组件Pascal André，Gilles Ardourel，ChristianAttiogbé，Arnaud LanoixLINA CNRS UMR 6241 -南特大学2，rue de laHoussinièreF-44322 Nantes Cedex，France电子邮件：{FirstName.LastName}@univ-nantes.fr摘要Kmelia构件模型是一种基于服务的抽象形式化构件模型。 它致力于正确组件的规格和开发。这项工作丰富了Kmelia语言，允许在指定组件和服务时描述数据，表达式和断言。 我们的目标是使断言在Kmelia中的使用，以支持富有表现力的服务描述，支持客户/供应商合同的前/后条件，并加强基于组件的系统的正式分析。断言用于执行服务、组件组装和服务组合的分析。此外，我们能够定义所需服务的虚拟上下文以及提供服务的组件的相应可扩展状态空间。 我们说明的工作与验证的一致性属性，涉及数据在组件和组件级别。保留字：组件、程序集、数据类型、断言、属性验证1介绍在基于服务和构件的软件系统设计中，形式化模型有助于对构件和系统进行描述和文档化，根据形式化搜索要求在库中查找构件和服务，检查构件的各种属性（正确性、活性、安全性）以进行构件认证，细化模型并生成可执行构件。正式模型是构建可信组件的强制性要求[24]。在[9]中，我们提出了一个正式的组件模型，称为Kmelia，其中i）服务不仅仅是简单的操作;它们包括合同，通信交互，动态演化规则和组合，ii）组件通过设置配置独立于其环境而设计，iii）组件组装由严格的服务可组合性规则管理，iv）组合组件由封装和提升策略管理。1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.05.0026P. André等人理论计算机科学电子笔记263（2010）5Kmelia模型[9]是一个抽象的正式组件模型，致力于规范和开发正确的组件;抽象意味着组件和程序集独立于执行平台。它们可以稍后在集中式或分布式执行平台中实现概念的形式定义对于表达和确保系统特定属性的验证是必要的Kmelia的一个关键特征是服务的核心作用。服务规范描述了与某些所需功能相对应的行为组装两个组件包括将它们所需的服务和所提供的服务连接起来。通过组件中的服务链接组件，可以建立到面向服务的体系结构的桥梁。在[9]中，我们介绍了核心模型和语言的语法和语义。它后来逐渐丰富起来。我们关注组合的动态方面：[9]中的交互兼容性，[7]中遵循这种增量方法，我们在本文中考虑Kmelia中数据和表达式的丰富及其对语言语法，语义和属性验证的影响。我们的目标有两个：• 启用断言的定义（使用不变、前置/后置条件以及服务、组件和组合的属性），• 增加行动陈述的表现力，以便处理实际规模的案例研究。断言是有用的i）定义关于服务的契约1（具有前/后条件）;契约增加组装正确性的置信度（通过约束所涉及的服务的前/后条件），并且在库中搜索组件时启用丰富的查询表达式，ii）确保组件关于不变量的一致性。这些操作实现了服务的一个功能部分，然后应该证明它与合同是一致的。因此，Kmelia模型的正确性验证方面通过断言的使用得到了增强。动机。对真实生活系统建模需要涵盖组件的静态和动态方面（结构、链接、动作、交互）。 我们希望尽早验证开发步骤，程序集是否是格式良好的;重要的是要涵盖系统的结构，动态和功能方面，以解决各种问题。的应用程序。现有技术表明，大多数抽象组件模型[4，15，28，14]支持交互正确性的各种验证，但它们缺乏对数据类型的表达;它们不提供断言和相关的验证规则。例如，在Wright中，基于CSP的动态部分非常详细（具体化和验证），而数据部分处理得不太好[4]。在[26]的建议中，数据类型是使用代数规范定义的，这便于使用状态转换系统的符号模型检查，但该建议不处理契约和断言。贡献在这项工作中，我们用数据和断言丰富了Kmelia模型，以便覆盖整个静态和动态方面，从而处理安全的1我们的合同定义与工程成果有关，如按合同设计[23]。P. André等人理论计算机科学电子笔记263（2010）57服务、一致的组件和正确的基于契约的程序集。首先，Kmelia语言被数据和断言丰富，以便以同构的方式覆盖关于断言的结构、动态和功能正确性其次，我们通过嵌套组件的不同级别来处理状态空间的可见性和访问;除了服务提升之外，我们还定义了组件组合中组件状态的变量提升和相关访问规则。最后，介绍了利用断言证明构件正确性的可行性。我们展示了如何验证结构的正确性，以及如何用新的数据语言表达相关的属性。文章的结构如下。第2节概述了Kmelia抽象模型，并介绍了它的新特性。在第3节中，将介绍一个工作示例来说明数据和断言的使用。 形式分析在第4节中讨论;我们提出了要执行的各种分析，这些分析是当前实现的，我们专注于组件一致性和检查组装链接。第5节总结了文章，并提出了讨论和观点。这项工作得到了COSTO工具的支持，COSTO工具在会议的工具演示会议上展示;在附录A中，我们提取了关于新数据部分的KmeliaCOSTO的概况见附录B。2Kmelia模型及其新特征Kmelia的主要概念是：组件、服务、组装和组合。组件是服务的容器。服务是一个复杂的实体：它有一个状态和一个动态行为;服务也可以声明所需和所提供的子服务。服务行为定义了服务执行其操作的顺序通信动作是服务之间同步交互的原语在组件组装中，组件通过服务成对链接：所需的服务由它链接到的所提供的服务实现复合组件封装组件程序集。在本节中，我们重新讨论了[9]的Kmelia模型，该模型得到了扩充和重构。具体而言，引入了以下特征：(i) 可观察性的概念类似于编程中的只读可见性，它允许提供者组件的状态信息对客户端或复合组件可用(ii) ·对所需服务的精确定义，允许对虚拟状态空间的约束，即对设计服务时未知的提供者组件的假设;(iii) 更灵活的消息命名规则，现在两个通信服务可以使用不同的服务名，这与提供者和客户端的独立设计一致(iv) 组装链接中的状态和消息映射，以处理提供者组件和所需服务上下文之间的这些新特性与服务操作、断言和契约有关我们8P. André等人理论计算机科学电子笔记263（2010）5→CW一WWIDD我我我伊贺恩设计了一种小型但富有表现力的数据语言，用于描述数据库、表达式和谓词（附录A中的快速概述）。在下文中，我们使用一个受Z符号启发的数学工具包。 X参与者Y表示从X到Y的关系（x→y表示关系的对（x，y）X1X2表示集合的不交并;X→Y表示来自X到Y;X→Y表示从X到Y的部分一对一函数;id表示当r是关系（r：XParticipateY）时，dom（r）和ran（r）分别表示r的定义域和值域，EDr和rDF分别表示关系r的定义域和值域限制，其中E<$X和F<$Y.定义2.1状态空间定义了一组受不变式和初始化约束的变量：=T，V，type，Inv，Init其中T是一组类型，V是一组变量，type：V T是将变量映射到类型的函数，Inv是定义在V上的不变量，Init是V的变量的初始化。状态空间概念用于组件和服务。在以下N是一个有限的名称集合，令M是消息名称的集合，M ≠ N。2.1组件[9]中的组件定义已经被重新构造：动作集被推迟到Kmelia表达式，约束S现在由服务属性实现，就像[7]中的协议一样。一个组件（类型）C是一个元组W，I，D，V，其中：•状态空间（参见定义2.1）。•组件接口，分成两个不相交的有限集合=P R，其中P代表提供，R代表需要。•是服务描述的集合，如第2.2节所述。就像，沿着所提供/所要求的标准划分：D=DPDR。• ν是一个将服务名称映射到服务描述的部分函数（ν：N>→D）。清单1：组件结构组件接口必须与服务描述一致：（1）提供的服务和要求的服务有不同的名称：dom（νDDP）dom（νDDR）=;（2）组件接口中的服务是组件中描述的服务的子集：IPdom（νDDP）IRdom（νDDR）。组件状态的可观察性。为了保持组件的抽象和封装，组件的状态只能通过其组件C1接口提供：需要：// components t a t e 空间类型<类型定义>变量不变<同品种器械>初始化. . .//变种作业// component服务中心服务. . .//作为描述下面结束_服务P. André等人理论计算机科学电子笔记263（2010）59⊂→我W⟨⟩B⟨⟩提供服务。然而，为了理解服务的具体化（即它的契约），我们可能需要观察它的上下文（它的组件状态空间的一部分）。类似地，复合组件需要从其组件中观察信息。因此，我们区分状态变量的可观察部分VO（VO V），不变量的可观察部分（InvO）（InvO定义在VO上），并相应地编写前/后条件（根据第2.2节的规则）。2.2服务组件的行为依赖于其服务的行为。服务使用与标记转换系统相结合的动作来描述功能和行为。服务在被调用时启动（由客户端服务调用），然后被称为激活并应该发展，直到它达到最终状态。服务与同一组件的其他服务共享其组件的状态空间。在其演进过程中，服务s可以调用其他服务或使用消息与它们通信。s的所有交互服务都在s的接口中定义。由于服务之间的依赖性和交互，若干激活的服务的动作交错或同步，但是一次只能观察到激活的服务。形式上，组件C的服务s由元组定义σ，IS，Cont，WL，B• σ=s，param，ptype，Tres是服务 签 名 ， 其 中 s 是 服 务 名 称 ，param 是 一 组 参 数 ， ptype ：param T是将参数映射到类型的函数，Tres∈T是服务结果类型;•服务接口如下所述;• Cont=Pre，Post服务合同，其中Pre为前置条件，Post为后置条件;•L是仅在服务行为B中使用的局部状态空间（定义2.1）;•服务行为;它是一个扩展标记转换系统（eLTS），定义如下。清单2：服务结构服务接口IS由元组DI，μ，WVI定义，其中P r o v i d e daService_1（param>）：结果<类型>接口subprovides ：Servlist>calrequires ：Servlist>extrequires ：Servlist>intrequires： Serv l i s t>. . .预同品种器械>变量#罗克阿勒空间 In i t i a l i z a t i o n. . .//变种作业行为Init i n i t i a l s t a t e><最终<最终 国家>//eLTS{<过渡l i s t>}邮政同品种器械>端需a服务_2（）下一页. . .//i n的相同方式10P. André等人理论计算机科学电子笔记263（2010）5DB⊆ ∈→W∈× →∈B.B.• DI是服务依赖关系;它由当前服务所依赖的服务组成。DI由四个不相交的集合组 成 ， 其 中 sub_sub （ vDDP ） （ 分 别 为 cal_dom （ vDDR ） ） 、 req_dom（vDDP）、int_dom（vDP））包含所提供的服务名称（分别为从调用者、从任何组件或从组件本身需要的那些）。• μ=μmname， mparam ， mptypeμ是 一组 消 息 签名 ， 其 中 mname∈ M，mparam和mptype与服务签名相同• WV 是根据定义2.1的虚拟状态空间;服务s的行为是一个标签转换系统（LTS），通过使用嵌套状态（通过状态注释函数）和嵌套转换（通过特定标签）进行扩展因此，是由元组=S，L，δ，Φ，S0，SF定义的eLTS，其中S是s的状态的集合;L是转换标签的集合（可能是动作的保护组合[保护]动作 *），并且δ是转换函数（δSLS）; S0是初始状态（S0S）;SF是最终状态的有限集合Φ是状态注释函数（ΦSsub s）。 现在采取行动一种克梅利亚的表情基本操作（例如分配）不涉及其他服务，也不使用通信信道。通信动作是服务调用/响应或消息通信。定义和验证服务行为的全部细节在参考文献[9，7]中提供。以下新特性是组件可观测性服务的结果特别地，所提供的服务可以在其前置条件中使用可观察变量（例如，当可观察组件变量isFull被评估为true时，不应该调用服务addElement因此，所需的服务可以定义一个虚拟上下文来设置关于什么应该是提供者组件的假设虚拟状态空间。组件的必需服务是另一个组件提供的服务的抽象。由于在指定所需服务时该组件是未知的，因此有必要“想象”其状态，我们称之为虚拟状态空间（即V）。对于提供的服务，此虚拟上下文始终为空。可观察性与服务断言。让s成为组件C的服务。组件状态空间的可观测变量和不可观测变量之间的区别根据下表重新讨论2第一个表指示服务的可访问状态空间。服务状态空间变量不变可观测部分不可观测部分可观测部分不可观测部分如果sVOVInvOInv需sVVV第五卷Inv第二个表指出了服务断言是如何划分为可观察/不可观察部分的，并精确说明了每个部分中哪些变量是可访问的。2.由于param和result中的补充变量，这里不是分区。P. André等人理论计算机科学电子笔记263（2010）511服务断言范围先决条件后置条件可观察O前不可观测前NO可观察O后不可观测员额编号如果sVOparam没有一VOparam {result}Vparam {result}需sVVparamVparamVVparam {result}没有一可观察性服务调用图1.一、状态变量作用域和断言作用域图1总结了状态空间、可观测性和服务契约之间的关系。方框表示组分a：A。灰色（resp）白色）“漏斗”表示提供（或服务）。可观察到的服务前/后条件分别为：reqA）是指a（resp.请求A的虚拟状态VV）。所需服务请求A的不可观察的前置条件给出了a的（调用者）组件状态变量V上的调用条件。服务provA的不可观察后置条件局部地引用a的整个状态V，并且应该建立a的不变量的不可观察部分。2.3组装和复合组件是通过其引用、组件程序集中的程序集链接或复合组件中的升级链接组成的链路是连接两个不同服务的抽象通信通道。子链接是根据服务依赖结构（cal和sub）在另一个链接的上下文中定义的链接。组件引用是组件（类型）的一个元素。组件引用由c：C表示，其中C是组件。对c的状态变量v的访问记为c。v. 通过谋杀语言，我们将使用术语设C是一个分支集ck：Ck，k ∈ 1. n和C k=<$Wk，Ik，Dk，ν k<$.BaseLink（ C × N× C × N）是一组四元组，使得：(1)（ci，n1，cj，n2）：BaseLink·n1∈domνi<$n2∈domνj(2)ci：C，n1：domνi·（ci，n1，ci，n1）∈/BaseLinkSubLink：BaseLinkParticipateBaseLink(3)<$（l1，l2）∈SubLink·（l2，l1）∈/SubLink<$其中domνi是组件Ci的服务名称集合，SubLink是关系SubLink的传递闭包。（1）表示任何基本链接都与a：O前O前vVO后V OC_V前NOre前体AO后 邮政 没QAintA12P. André等人理论计算机科学电子笔记263（2010）5一个组件的服务名到另一个组件的服务名;（2）表示服务名不能链接到自身;（3）链接中没有循环2.3.1部件组件程序集是一组通过其服务链接（水平组合）的组件组装链接将所需的服务关联到所提供的服务。在组装组件时，在交互服务之间建立通信通道通道定义了服务行为的通信动作的上下文。由于行为是在不知道它将与之通信的组件的情况下编写的通道通常以表示上下文的所需服务命名。占位符关键字CALLER是一个特殊的通道，代表为服务调用打开的通道。从提供的服务p的角度来看，CALLER是当p被调用时打开的通道从调用p的服务的角度来看，这个通道是以它所需的服务之一命名的，这个服务可能被命名为p。占位符关键字SELF是一个特殊通道，代表为内部服务调用打开的通道。在这种情况下，所需的服务也是所提供的服务。新特性是我们在链接中引入的映射。程序集链接中的上下文和消息映射。 最终目标是将定义在其虚拟上下文中的所需服务连接到定义在其可观察上下文（其组件的可观察状态空间签名匹配和依赖映射（通过子链接）在[9]中介绍。这里我们添加一个上下文映射和一个消息映射。 前者是虚拟语境概念引入的结果。组件cr：CR的虚拟状态空间变量sr必须后者允许不同的消息名称，因为所需的服务通信动作是独立于所提供的服务通信动作而设计的目前，sr的每个消息名都映射到sp的消息名。如果需要更多的灵活性，例如参数重新排序，可以使用自适应机制[6]。图2延伸图。1至组件和复合部件。方框表示组分（a、b）和复合物（c）。图中给出的条件1是检查组装链接和促销链接支持的合同的基础。特别地，reqB的虚拟状态VV应该与a的子集V映射。不可观察的先决条件（分别为：后置条件）对于所提供的服务是无意义的（相应地，所需的服务），因为他们阻止安全组装和促销合同。在形式上，程序集类型A是一个元组C，alinks，subs，vmap，mmap，其中• C是一组分量引用c k，使得c k：C k，k ∈ 1。n，P. André等人理论计算机科学电子笔记263（2010）513⟨⟩v（n2）我CiJ我J请求C：C一Ra：AV OC_V方程式AO前O邮政vmapprovA没有O前vVO后B：BV OC_V前NOreB区箴映射可观测性B服务调用函数调用组件链接推广链接图二、程序集中的状态变量范围和断言范围• alinks是一组C服务之间的汇编链接，alinks基本链接(1)（n（ci，n1，cj，n2）：alinks·ci∈ C <$cj∈ C <$（2）（（n1∈ IP<$n2∈ IR）<$（n1∈ IR<$n2∈ IP）也就是说：链接组件是程序集的那些组件（1）;链接的服务具有对称的需要-提供性质（2）。• subs表示包含在其他链接中的链接：SubsSubLink(3)（domsubs− ransubs）(4)（<$（（ci，n1，cj，n2）<$→（ck，n3，cl，n4））∈subs·ci=ck<$cj=cl）<$(5)（n（ci，n1，cj，n2）：ransubs·（（vi（n1）∈ DPi）xor（vj（n2）∈ DPj）也就是说：子链接依赖于相同组件（4）的其他链接（3）;所需服务链接到所提供的服务（2）、（5）。• vmap=vmapV ar，vmapExp是与链路相关联的上下文映射函数，使得vmapV ar：BaseLinkParticipVvmapExp：（BaseLink×V）→exp（V）(6)domvmap（alinkssubs）domvmapExp =vmap(7)（1）（1）（2）（3）（4）（5）（|（c i，n1，c j，n2）|）= VV(8)var（vmapExp（ci，n1，cj，n2））VO）其中exp（V）表示V的变量上的表达式，并且var（exp（V））=V。这些公式表示上下文映射的链接是组件的链接（7）。 映射的变量是虚拟状态空间变量的变量所需的服务N2。映射表达式是使用n1（8）的可观测变量构建的。intAqB邮14P. André等人理论计算机科学电子笔记263（2010）5−组件部件cp： CP;cr： CR链接// −assembly l i n k s−−@la：p−rCP. provServ克河 reqServc o n t e x t 映射CR. var1 = expr（cp. varA，CP. varB. . . ）的情况下，CR. var2 = expr（cp. varA，CP. varB. . . ）的情况下，消息映射provServ。msg1 = reqServ。msgAprovServ. msg2 = reqServ。 msgB子链接：{lasub}//−子链接 −. . .端//组件@lasub：r−pCP. subReq克河 箴• mmap是与链路相关联的消息映射函数，mmap：BaseLinkParticipM× M(9)dommmap<$（alinks<$subs）<$（<$（ci，n1，cj，n2）∈dommmap·(10)（1）m = 0，m=0|（c i，n1，c j，n2）|）·m1∈ μ s1<$m2∈μ s2））消息映射的链接是程序集（9）的链接。映射的消息是链接的服务s1和s2（10）的消息清单3：程序集链接作为说明，让我们考虑清单3的程序集示例。两个组件cp：CP和cr：CR由一个名为@la的组装链接组装;该链接表示cr所需的服务reqServ由cp所提供的服务provServ实现。 的p r前缀表示链接方向（从提供的R要求）。上下文映射关联基于可观察变量varA、varB构建的表达式。. .将分量CP的值转换为var1、var2。. . reqServ的虚拟上下文的变量。消息映射将provServ的msg1关联到reqServ的msgA。子链接必须与服务依赖项一致。例如，如果所提供的服务provServ在其calrequires依赖关系中需要服务subReq，则子链接必须与组件cr提供的服务prov相关联，或者与服务reqServ的subprovides依赖关系相关联。2.3.2复合组合是封装程序集或其他组件的组件。嵌套子组件的某些功能（变量和服务）可以在复合级别上进行升级。在以前的版本中[9]，我们定义了推广链接来推广服务，并可能对服务进行重命名。推广在这里扩展到状态变量推广，它允许前条件弱化和后条件加强状态变量推广。我们目前对组装客户端或复合客户端应用相同的可观察性模式，只是可观察变量可以在复合级别提升。状态变量提升。 来自子分量的可观测变量voc：C可以提升为复合组件的变量vp（语法P. André等人理论计算机科学电子笔记263（2010）515我的世界∈C ∈I·∈CiJJ这就是：vp FROM c。vo）。升级后的变量将保留其类型，并在有效上下文中使用拥有这些变量的子组件的服务进行访问。这保证了封装原则。形式上，复合类型是元组CC=C，A，plinks，pvars，其中• C=，v是一个在2.1节中定义的分量类型。默认的预定义复合组件是SELF：C。• A=C，alinks，subs，vmap，mmap是一个程序集定义，如2.3.1节所述。• plinks是在alinks中未使用的A的服务之间的一组促销链接：plinksBaseLink（（ci，n1，cj，n2）：plinks·(1)ci∈ C <$cj=SELF<$(2)（（n1∈ IR<$n2∈domνR）<$（n1∈ IP<$n2∈domνP））<$(3)（ck，n3k（ci，n1，ck，n3）/alink （ck，n3，ci，n1）/alink）(4)v（n2）=rename（v（n1），n2））其中domν是组合的服务名称的集合，rename（s，n）是返回由n重命名的服务s的函数。• pvars是升级映射函数，pvars：（C ×V）ParticipV（5）（n（ci，vp）：dompvars·vp∈VOn=type（pvars（ci，vp）升级链接将SELF组件关联到其中一个组件（1）。提升的服务保持其性质（提供或要求）（2）。在程序集中未链接提升的服务（3）。提升的服务定义是服务重命名之前的子组件之一（4）。提升变量是其所有者子组件中的可观察变量，并且在复合中具有相同的类型（5）。新引入的特征（数据语言，可观察性，虚拟上下文）是描述合同的表达手段。第3节说明了它们。3一个工作示例在本节中，我们通过指定一个简化的库存管理系统来说明Kmelia语言;还讨论了Kmelia的新特性。该系统管理产品参考（目录）和产品存储（库存）。主服务对自动售货过程进行建模。系统管理员拥有特定的权限，他们可以根据某些业务规则添加或删除引用，例如：“新引用不在目录中”或“可移动引用必须具有空库存水平”。该系统被设计为可重用组件StockSystem，提供（促销）自动售货服务并需要授权服务。 它封装了两个组件的组装： sm ：StockManager 和ve ：Vendor，如图所示3 .第三章。前者是管理产品引用和存储的核心业务组件。后者为供应商用户界面建模利用自动售货服务，用户可以16P. André等人理论计算机科学电子笔记263（2010）5DD类型产品分类* *struct{i d：（c）描述：字符串;数量：};常数maxRef：整数 * =100;emptyString：字符串 ：=“的”;noQuantity：整数* =−1noReference：整数：= −1;库存系统sm：StockManagernewReference询问码代码添加ve：供应商授权授权显示...deleteReference去除号试验自动售货自动售货库存增加号试验服务调用函数调用秩序减少号试验组件链接推广链接图3.第三章。简化库存装配案例研究使用所需的服务addItem在库存管理中添加一个新项目。所需的服务addItem由所提供的服务newReference填充，它获取一个新引用，并在有可用的新引用时执行系统更新（请参见清单5）。链接和子链接在复合组件中显式定义，如清单7所示。图3中的嵌套服务表示服务依赖性I.例如，所需的服务addItem提供了一个名为code的子服务。这将在清单4中详细说明。不同的箭头表示各种类型的调用：函数调用（没有副作用）或服务调用（根据服务依赖性I）。 服务newReference调用一个显示函数（在预定义的Kmelia库中声明），一个内部需要的服务getNewReference（来自同一个组件），一个来自其调用者的服务ask_code和一个外部需要的服务授权Kmelia中的数据类型 数据类型在共享库（预定义或用户定义）中的TYPES下面的库（名为Stocklib）声明了一些特定的类型，函数和常量。 这一部分的数据类型相当具体;更抽象的数据类型正在被包含在预定义的库中。A Kmelia 分 量 和 可 观 测 状 态 。清 单 4 显 示 了 StockManager 组 件 的KmeliaStockManager的状态声明了一个可观察的变量catalog，它将可用于上下文映射。两个数组（plabels和pstock）用于存储当前参考标签和可用数量。不变量是一组命名谓词[obs] [@name]：pred_expr>，其中断言前面的标签是（可选）MgetNew引用P. André等人理论计算机科学电子笔记263（2010）517组件库存管理器界面规定：{newReference，removeReference，storeItem，orderItem}需要：{授权}使用{STOCKLIB}类型参考：：范围1. . maxRef变量vendorCodes：s t Of（c）//授权A d m i n i s t r a t o r sOBS目录：s t Of参考文献;//产品I d =第十届外来资产arrays普拉贝尔：阿雷阿雷[参考资料]外来资产字符串;// product描述普斯托克：阿雷阿雷[参考资料]外来资产I n t e g e r//产品数量不变OBS@borned：size（ c a t a l o g）= maxRef，@引用：为所有人r e f：参考|i includes（c a t a l o g，r e f）implies（plabels [ ref ]<>emptyString and pstock [ r e f ]<>noQuantity），@notreferenced：为所有人r e f：参考|e x c l u d e s（catalog，r e f）i mplies（p labels [ ref ]=emptyString and pstock [ r e f ]=noQuantity）初始化目录：=emptySet;vendorCodes ：=emptySet;//文件i l e d通过一需ser r v i c eplabel s：=int n = nums（nums，nums）;// consistent与. .普斯托克 ：=arrayInit（p s to ck，noQuantity）;//. . 空加塔洛P r o v i d e dnewReference（）下一页：整数//返回结果=productId或noReference接口卡尔内雷斯：{ask_code}#必填从的c a l l e rintrequires：联系我们预OBS尺寸（c a t a l o g） =1和结果<= maxRef）o r（结果=无参考）），obs@resultValue：（结果<>noReference）i mplies（not I n（ ol d（ catalog）， Result）和catalog= add（ ol d（ catalog）， Result）），OBS@noresultValue：（结果=noReference）i mplies不变{c a t a l o g}，@refAndQuantity：（结果）<>noReference）i mplies谓词名称。前缀obs意味着谓词属于InvO。例如，@borned表示目录有一个上限 ;@referenced 表 示 目 录 中 的 所 有 引 用 都 有 一 个 标 签 和 一 个 数量;@notreferences表示未知引用没有标签和数量。清单4：StockManager State的Kmelia规范一个 Kmelia服务 与它的 断言。 清单5 显示了newReference 的规范，它是StockManager提供的服务之一。它的前提条件是目录没有达到最大规模。前缀obs意味着谓词@resultRange属于PostO。可观察到的后置条件表明，我们可能会得到范围为1的结果。maxRef或noReference;在后一种情况下，目录保持不变。不可观察的后置条件（没有前缀obs）表示不可观察的状态变量plabels和pstock将如何演变。清单5：newReference服务的Kmelia规范18P. André等人理论计算机科学电子笔记263（2010）5required add Item（）：接口次提供：联系我们虚拟的变量产品目录：布尔值;（p s to ck [结果] =0和p l a b e l s [结果] <>emptyString及（对于所有者：参考文献|（i<>结果）i m p lies（p stock [ i ] =o l d（p s to ck）[ i ]和plabels [ i ] =o l d（plabels）[ i ] ）），@NorefAndQuantity：（结果）=noReference）i mplies未更改{ p s to ck， plabels }结束我c：=##C$LL R11 ask #codee1[vendorCodes中的c] ##C$LL R（）sg（d）e2[d-. e）pt*/tring]res：=##/L011get2ewReferencee4[d = e）pt*/字符串][not（c in vendorCodes）]不允许添加引用+不允许添加 *（+addingga n&）pt*/e tdescri ptio n isno tallowed+）{catalog：= including（catalog，res）; pstock[res]：= 0;plabels[res]：= d}en##C$LL R11newReference（res）F图四、COSTO工具导出的newReference服务的行为服务newReference的行为没有以文本形式呈现，但其图形表示如图4所示。它是通过COSTO工具的点翻译器获得的（专用于Kmelia模型，Sec.4）。请记住，转换标签是受保护的操作组合。通信动作被标记为信道（comOp）消息（param*），其中通信运营商comOp被发送（！）或接收（？）留言，打电话（！！）或结果（？？）一种服务。信道_CALLER用于调用者服务，_SELF用于相同组件的服务（内部调用），_rs代表所需服务。在图4中，newReference的行为包括询问供应商代码，如果返回的代码被引用到vendorCodes中，则获得产品描述d并将其添加到目录中。在任何情况下，服务都会将操作状态返回给调用者。所需服务的虚拟状态空间 清单6显示了组件Vendor的所需服务addItem的规范。所需的服务通过设置虚拟状态空间（第6页）对其提供者在清单6中，addItem的虚拟变量表示目录的Vendor相应地编写前/后条件。清单6：addItem的KmeliaP. André等人理论计算机科学电子笔记263（2010）519组件库存系统接口提供：{vending}需要：{授权}组成组件部件SM ：StockManager;ve：供应商链接////////////组件友情链接//C o n t e x t映射l r e f： p−rSM. newReference，ve. AddItemve. 目录空==空（sm. 目录），ve. catalogFull == size（sm. catalog）=MaxInt子链接：{lc o d e}. . .lcode：r−pSM. ask_code，ve. 代码端//assembly促进链接////////////促进友情链接//lvend：p−pve. 贩卖，SELF. 自动售货END_COMPOSITIONlaut ：r−rSM. 授权 、SELF.授权目录空：布 尔 值// p o s i b l y catalogSize 虚 拟不变not（目录为空和产品目录 ）Pre not catalogFull//没有LTS邮政 （结果）<>noReference）i mplies（不目录空）结束在清单7中，我们描述了复合StockSystem，它是图3的文本表示的摘录。复合StockSystem定义为一个包含子组件sm：StockManager和ve：Vendor的程序集。组装链接和子链接连接子组件服务。促销链接在复合层设置服务售卖和授权清单7：StockSystem的Kmelia上下文和消息映射。上下文和消息映射（参见第2.3.1节）被指定到汇编链接中。在清单7中，所需服务addItem的虚拟状态空间的变量与所提供的服务newReference的上下文变量的表达式相关联，即组件sm的可观察状态变量。在本例中，没有消息映射，因为两个服务使用相同的msg消息（在默认的Kmelia库中声明）。这个例子用于下一节中描述的形式分析的实验。4形式分析与实验Kmelia规范的形式分析包括检查Kmelia模型的各种性质。验证的目标是检测规范错误：违规政策推迟到实现问题。一些分析直接在支持Kmelia的COSTO工具中执行，其他分析则委托给适当的外部工具。在本节中，我们将讨论这些方面20P. André等人理论计算机科学电子笔记263（2010）5与Sect.