SysML组装：考虑非功能需求的成本验证与接口自动机同步

可在www.sciencedirect.com在线获取理论计算机科学电子笔记295（2013）31-47www.elsevier.com/locate/entcs使用SysML组装具有非功能需求的组件Samir Chouali，Ahmed Hammad，Hassan MountassirFEMTO-ST Institute UMR CNRS 617416，routedeGray-25030BesanBesanconconcedex，France摘要构件系统的非功能需求与功能需求一样重要，因此在构件组装时必须考虑非功能需求。 这些属性预先用SysML需求图指定。我们用SysML块定义图描述了基于组件的系统架构，用序列图描述了组件的行为。我们建议正式指定组件接口与接口自动机，从需求和序列图。在这种形式主义中，转换被注释为指定非功能属性的成本。组件之间的兼容性通过同步它们的接口自动机来实现。 该方法被解释为以电动汽车CyCab为例，其中成本与组件动作的能耗相关联。我们的方法验证了一组组件在根据系统架构组成时，是否通过尊重其非功能需求来实现其任务关键词：组件组装，接口自动机，SysML，非功能属性，系统架构。1介绍基于组件的软件工程（CBSE）的思想是通过组装各种库组件而不是从头开始组件是一个组合单元，具有合同指定的接口和显式依赖关系，[19]。接口描述了所需的服务，而不公开组件的实现。它是访问组件信息的唯一接口可以在签名（方法名称及其类型）、行为或协议（方法调用的调度）、语义（前条件和后条件）和服务质量级别上描述组件信息应用基于组件的方法的成功取决于连接组件的互操作性。当组件的接口兼容时，组件之间的互操作性保持不变。1电子邮件：{schouali，ahammad，hmountas}@ femto-st.fr1571-0661© 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.04.00332S. Chouali等人/理论计算机科学电子笔记295（2013）31SysML语言是一种UML profile，它是一种用于记录和图形化指定由硬件和/或软件块组成的系统的所有方面的语言。SysML是由对象管理组织（OMG）[1]提出的，用于定义系统工程的通用建模语言SysML在工业界和学术界都享有前所未有的普及，它用于协调不同的参与者，以实现系统，并确保设计的一致性和质量。它是一种非常适合嵌入式系统建模的语言。在本文中，我们专注于使用SysML图组装第一步指定的组件在第二步中，我们提出了一种形式化的规范和验证方法，以基于第一步的SysML模型来验证组件的组成。 我们的方法利用和适应的接口自动机形式主义，以验证组件的组成。基于接口自动机的方法由L.Alfaro和T.Henzinger提出，[2，3]。它们与自动机有特定的组件接口，这些接口由输入、输出和内部动作标记。这些自动机在签名和协议级别上描述组件信息。还提出了一种有趣的验证方法来检测两个组件接口之间签名和协议级别验证是基于接口的组合，这是通过同步共享操作来实现的在这种情况下，我们建议指定组件为基础的系统（CBS）的体系结构，组件的要求，和组件的行为，与SysML图。我们的目标是利用SysML的图形形式来建模CBS。我们认为，这是一个合适的形式主义，以指定组件和CBS规范和CBS项目的开发人员之间的沟通。另一个目标是处理CBS非功能性（NF）需求，这是通过利用SysML需求图来促进的为了正式验证组件之间的组装，指定与SysML模型，我们建议适应和利用接口自动机方法。我们提出了这种方法的两个适应：（i）第一个是在接口自动机的形式规范和验证中处理SysML指定的系统架构实际上，接口自动机只是用来描述构件的行为，不能描述原始构件与复合构件之间的关系，也不能描述复合构件与其子构件之间的层次关系，这也影响了构件的行为。（ii）第二个是考虑接口自动机形式主义和组件组成验证中的这些NF要求包括组件所提供或要求的每个服务的能耗。因此，我们建议用代价来注释接口自动机中的转换，以获得一种加权自动机，并且我们建议在组件组合的验证中处理这种注释本文的结构如下。 在第2节中，我们给出了 CyCab车辆，我们指定半正式的系统架构，组件的行为和NF的要求，与SysML图。在第3节中，我们描述了一种方法来正式指定SysML架构的组件为基础的系统。S. Chouali等人/理论计算机科学电子笔记295（2013）3133第4节介绍了所提出的方法相结合的SysML和接口自动机，以组装组件，并考虑系统架构和NF的要求，以验证它们的互操作性。相关工作见第5. 我们在第6节中总结我们的工作并追踪一些观点。2使用SysML在本节中，我们提出了一个基于组件的系统的例子，并提出SysML图来描述系统。这些图被认为是基于组件的系统建模的第一步，将在正式规范和验证步骤（第二步）中使用。2.1CyCab非正式描述作为一个例子，我们考虑一个基于CyCab汽车组件的系统（在[6]中）。CyCab汽车是一种新型的电动交通工具，主要用于独立的交通服务，允许用户通过预先安装的车站进行移动。它完全由计算机系统控制，可根据多种模式自动驱动。CyCab的目标是允许客户使用车辆从一个站点移动到另一个站点。为了说明这一概念，我们考虑以下系统约束：(1)一辆CyCab有一条合适的道路，车站配备了传感器 和计算单元。 (2)We建议CyCab的驾驶由从站接收的信息引导，该信息将CyCab与站进行比较。 （3）道路上没有障碍物。 （4）车辆由以下方式启动： 启动器组件。车辆还具有与紧急停止部件相关联的紧急停止按钮。在CyCab移动过程中，可随时激活紧急停机按钮 它通过发送emgcy信号来指定！.CyCab及其环境可以被看作是一个抽象的系统， 由两个组成部分组成：车辆和空间站。车辆也由基本组件组成：车辆核心，启动器和紧急停止（与紧急停止按钮相关联）。该工作站由传感器和计算单元组成。我们还考虑了以下制约因素：• 该站是由一个传感器实现的，该传感器接收来自车辆的信号，给出车辆的位置（spos？）.传感器将此位置转换为地理坐标并发送消息（pos！）到计算单元。在处理车辆位置之后，计算单元因此发送信号（远！或者停下），以显示其是否远离车站。• 车辆也发送一个信号复位！启动紧急停机按钮后，将系统复位34S. Chouali等人/理论计算机科学电子笔记295（2013）312.2模块定义图SysML提供了一个称为块的结构元素。块可以表示系统的任何块在描述系统结构的块定义图（BDDBDD的作用是描述块之间的关系，这些块是旨在指定要建模的系统的层次结构和互连的基本结构元素。还描述了组件所需的接口（关系使用）和操作（关系实现）图1显示了一个Fig. 1. CyCab模块定义图BDD有八个街区。这是CyCab建模的第一个层次。名为CyCabSystem的块代表整个系统。它被分解为两个子块（车辆和车站），并通过组合关系与它们连接。车辆组件分为三个子组件，即起动器、车辆核心（VC）和紧急停止（EH）。将监测站分解为传感器和计算机单元两个子部件。在本文中，我们利用BDD形式化地描述系统的体系结构，S. Chouali等人/理论计算机科学电子笔记295（2013）3135在组件装配中利用此规范2.3内部框图内部框图（IBD）允许设计师细化模型的结构IBD在SysML中相当于UML中的复合结构图。在IBD中，部件是基本元素，它们被组装起来，以定义它们如何协作来实现块结构和/或行为。SysML中的部件对应于UML中的对象。部件表示块while流端口表示块的接口，通过该接口块与其它块通信。图2显示了媒介物的IBD。例如，在图2中，部件Starter、Vehicle Core（VC）和Emergency Halt（EH）协作以实现部件Vehicle的功能。该图显示了组件之间的装配链接，因此我们利用它来推断组件之间的装配顺序。图二、 车辆内部框图2.4需求图要求规定了必须在受试者（目标系统）中提供的能力或条件。能力通常是指系统必须支持的功能，我们称之为功能需求。条件通常意味着系统应该能够在特定的约束下运行或产生结果，我们称之为非功能性需求SysML需求图允许多种方式来表示需求关系。这些关系包括定义需求层次结构、导出需求、满足需求、验证36S. Chouali等人/理论计算机科学电子笔记295（2013）31图三. 需求图要求和细化要求。这种关系可以改进系统的规范，因为它们可以用于对需求进行建模。在图3中，要求GECC，CyCab的全局最大能耗，指示CyCab不得超过能耗限制。该要求包含要求ECS，电站部件的最大能耗和ECV，车辆部件的最大能耗。要求ECS包含要求ECSS（传感器组件的最大能耗）和ECCU（计算单元组件的最大能耗）。要求ECV包含要求ECVC（车辆核心部件的最大能耗）、ECSR（起动机部件的最大能耗）和ECEH（紧急停机部件的最大能耗）。例如，在需求ECSS中，标识符Qpos是由其他组件执行所请求的服务pos所需的能量资源的数量，并且标识符Qspos是组件Sensor可以用于执行所请求的服务spos的能量资源的最大值。S. Chouali等人/理论计算机科学电子笔记295（2013）31372.5序列图序列图用于表示块的结构元素之间的交互，作为消息交换的序列，也称为组件（或块）协议。在CyCab系统中，车辆发送信号spos！以通知即将到来的站关于其位置，并且其作为结果接收信号（远！或停止！）知道它是否在离车站很远的地方。传感器（Ss）和计算单元（Cu）是该站的两个子组件。传感器检测车辆发出的位置信号，并将其转换为地理坐标（pos！）计算单元利用该距离计算车辆与车站之间的距离，并判断车辆与车站之间是否相距较远。车辆由三个基本组件组成：车辆核心（Vc），启动器（Sr）和嵌入式紧急停止（Eh）设备。比如说见图4。计算机单元时序图图4显示了序列图组件ComputingUnit。该图指定了组件协议，展示了组件与其环境之间的交互环境代表系统中的其他组件。因此，计算单元从环境（其是传感器组件）接收消息pos，并且通过将消息发送到远或停止环境（车辆组件）来响应3SysML系统架构在上一节中，我们已经提出了使用BDD和IBDSysML图来指定基于组件的系统BDD图显示了系统的全局结构，以及复合块（复合组件）与其子块（子组件）之间的关系。IBD图显示了块之间的组合链接。在本节中，我们建议将此架构正式指定为一个图，其中节点对应于系统的块，边表示两者38S. Chouali等人/理论计算机科学电子笔记295（2013）31复合块及其子块之间的层次关系。如果只考虑层次关系，图中的节点可以看作树。在CyCab示例中，我们将图5中描述的图关联起来，对BDD和IBDSysML模型描述的系统架构进行形式化建模。连续边表示BDD模型中指定的复合块及其子块之间的层次关系。虚线边缘表示组合块级别上组件之间的连接。此连接链路在IBD模型中指定。当且仅当它们的接口之间至少有一个交互时，这个图的正式定义在定义1中给出。对于SysML系统架构M，我们用CM表示构成M的所有（复合和原始）组件。定义1（架构的图形表示）。系统SysML体系结构M的图表示GM=<$NGM，CpGM，CnGM<$，包括• 表示CM的节点的有限集合NGM;• 表示组合块及其子块的节点之间关系的有限边集CpGM;• 边的有限集合Cn GM，表示表示同一块内的子组件的节点之间的连接。整个系统车辆站图五、CyCab汽车系统图通过遍历该图，我们可以很容易地提取整个系统（组合系统）的组件将被组成的授权顺序，然后我们将这些信息用于验证组件之间的兼容性。例如，与基于图5中描述的 树 的 CyCab 系 统 相 关 联 的 组 成 的 顺 序 是 ： （ Starter ）→VehicleCore→EmergencyHalt）→（Sensor）→ComputingUnit）。事实上，我们可以在图5中看到，Eh、Vc、Sr分别对应于EmergencyHalt、Vehi-Eh Vc Sr铜硫S. Chouali等人/理论计算机科学电子笔记295（2013）3139一cleCore和Starter用虚线链接连接，并且它们还与节点Vehicle相关联，Vehicle对应于复合组件Vehicle。因此，它们可以通过（Starter_VehicleCore_EmergencyHalt）组装在一起，以获得复合车辆。我们对与 节 点 Cu 和 Ss 相 关 联 的 分 量 Sensor 和 ComputingUnit 以 及 由（Sensor_ComputingUnit）获得的复合Station应用相同的过程。我们还可以在同一图中看到，节点Vehicle通过虚线链接与节点Station相关，它们也与整个系统相关。因此，为了获得一个系统，必须组成：（启动器）、车辆核心、紧急停机）、传感器、计算单元。我们认为符号是复合算子。我们注意到合成的操作是结合的，所以合成的顺序对组件之间的兼容性的验证没有影响4非功能性增强的接口自动机与SysML图在这一节中，我们提出了我们的形式化的接口自动机的基础上，正式指定组件接口，根据SysML图，以验证组件的互操作性。4.1基于SysML序列图和NF要求的组件接口我们建议通过考虑由序列图指定的组件协议和由需求图指定的组件非功能（NF）需求来正式指定组件接口。因此，我们建议利用接口自动机的形式主义，我们丰富的NF需求，以正式建模SysML序列图和需求图。接口自动机是由L.Alfaro等人[2]定义的，用于对软件组件接口的时间行为进行建模。它们被认为是有标签的变迁系统，其中变迁被标记为动作的名称，这些动作被分为三类：输入、输出和隐藏动作。每个组件接口都由一个接口自动机描述，其中输入操作用于对可以调用的方法进行建模，以及从通信通道接收消息的结束，以及这些调用的返回值。输出操作用于对方法调用、通过通信通道的消息传输以及在方法执行期间发生的异常进行建模。输出操作描述组件所需的操作（由符号“！”表示），输入动作描述组件的所提供的动作（由符号“？”表示组件内部的内部（或隐藏）操作描述了其本地操作（由符号我们以“我”、“我”、“我”来定义A A在状态%s时启用的输入、输出和内部操作。在本节中，我们将展示如何利用接口自动机形式化，以考虑每个组件40S. Chouali等人/理论计算机科学电子笔记295（2013）31一一一一一一一一一在组件组装的规范和验证中，因此，我们在下面给出了一个界面自动机的定义，它被指定能量消耗的函数所加强。因此，我们定义了一种加权自动机，其中转换用对应于动作能耗的成本进行注释。定义2（接口自动机）。一个接口自动机A = S A，I A，I，δO、 δH、δA、λ A、λA由以下组成：• 一个有限的状态集合SA;• 初始状态的子集IA<$SA;• 三个不交集I、O和H输入、输出和隐藏动作，我们用A=IOH表示;• 状态间跃迁的集合δA<$SA×<$A×SA;• λA：总函数，它将每个动作与执行该动作所需的能量资源的数量相关联λA→N。该函数指定了我们与需求图中指定的每个组件动作的最大能耗相关联的值。当我们组合两个接口自动机时，基于两个自动机的同步产品的合成自动机可能包含非法状态，其中一个自动机发出的输出动作在另一个自动机中不可接受为输入。这些非法状态的存在并不足以决定接口之间的不兼容性。事实上，所提出的接口自动机的方法，也被称为乐观的方法，允许验证接口自动机之间的兼容性复合接口期望环境传递只通向合法状态的转换。两个接口组成的这种法律环境的存在表明，有一种方法可以使组件正确地协同工作。图6和图7显示了CyCab汽车系统的原始组件的接口自动机。在接口自动机中指示能量消耗信息这些自动机正式指定了前一节中描述的因此，图7中描述的组件计算机单元的接口自动机指定了该组件的协议，因此它指定了图4中描述的计算单元的序列图我们还利用图3中的需求图描述的NF需求来注释接口自动机中的转换，其中cot与每个动作的能量消耗相关联例如，在图6中，我们可以在组件Vehicle core的接口自动机中看到，该组件执行了一个远？这需要5个能量单位，并且该组件需要动作SPOS！最多6个能量单位。这些值5和6分别对应于图3中要求ECV中的Qfar和QsposS. Chouali等人/理论计算机科学电子笔记295（2013）3141SPOsspos？/3POS1pos！/62传感器（Ss）停止站住！8POSpos？/312远远！5计算单元（Cu）开始！12开始1初级（高级）埃姆格西emgcy！/6reset1重置？102紧急停机（Eh）图第六章车辆子部件的接口自动机图第七章Station子组件的接口自动机4.2块兼容性验证块（组件C1）和另一个块（组件C2）之间的兼容性验证是通过验证它们的接口自动机A1和A2之间的兼容性来获得的。兼容性的验证步骤如下所示。主要算法输入：SysML建模输出：如果兼容性满足，则为复合组件的接口自动机，否则为空自动机。算法步骤：（i）生成方框定义图和内部方框的对应树，以便正式指定系统架构：通过应用来自BDD和IBD的转换规则来获得树。这些规则是显而易见的。例如，每个块对应于一个树节点，并且分两步处理块之间的链接，以便从BDD中获得块与其子块之间的链接，并且从IBD模型中获得子块之间的链接。（ii）序列图和需求图的形式化规范，其中接口自动机富含非功能属性：此步骤通过应用来自序列图和需求图的转换规则以获得具有能量消耗约束的接口自动机来执行从序列图到接口自动机的规则转换在[10]中给出。本文的创新之处在于考虑了需求图和NF-需求的接口自动机方法。我们利用这些图注释转换与成本接口自动机。（iii）通过处理以下内容来验证接口自动机之间的兼容性开始停止？8埃姆格西复位1 3远SPOs2停止溶剂核心4（Vc）42S. Chouali等人/理论计算机科学电子笔记295（2013）31∩Σ一一一一算法（算法2），并考虑系统结构和NF属性。算法2输入：接口自动机A1，A2.输出：A1~A2.算法步骤：（i）验证A1和A2是可组合的。（2）计算乘积A1→A2。(iii) 计算A1中非法状态的集合A2.（iv）计算A1→A2中的不兼容状态集：通过仅启用内部和输出操作（假设存在有用的环境），可以到达非法状态的状态。（v）通过从自动机A1<$A2中消除非法状态、不兼容状态和初始状态中的不可达状态来计算合成A1<$A2 （vi）如果A1→A2为空，则A1和 A2不兼容，因此C1和C2不能在任何环境中正确组装。否则，A1和A2是兼容的，它们的相应部件可以正确装配.在下文中，我们给出了形式概念的定义（复合条件，同步乘积......）在下面的算法中通过考虑NF性质来利用只有当两个自动机的动作是不相交的，除了它们之间共享的输入和输出动作之外，合成操作才可以生效。当我们组合它们时，共享的动作是同步的，而所有其他的动作是异步交错的。定义3（组成条件）。 两个接口自动机A1和A2是可组合的，如果我我A1A2 =1001O =100021电子邮件*=10002电子邮件* =共享（A1，A2）=（A 1，A 2）∩ΣO)∪(ΣI是一组共享的操作，A1和A2。A1A2A2A1在下文中，我们给出了考虑能耗约束的两个接口自动机之间的同步乘积的定义。以下定义背后的直觉是，两个组件可以在共享动作上同步，无论两个交互组件之一C1需要消耗x个能量单位的动作sa（输出动作），而另一个组件C2需要消耗y个能量单位的动作sa（输入动作），使得x≥y。这是一个明显的条件，因为：首先，通常组件是可重用的，并且由不同的团队和公司开发，因此组件的操作和所需的第二，例如：C1不能使用由C2操作的动作sa，如果这个动作需要比C1分配的更多的能量单位。定义4（考虑能耗的同步产品）。Σ∩ΣS. Chouali等人/理论计算机科学电子笔记295（2013）3143A组A12一一个2∪Σ一的1一个2一个2的1一个2的11一个2112的1一个2112121的112122一个2的1一个2一个2的1的1一个221的1一个21一个22一个2的1一个2的1设A1和A2是两个可组合的界面自动机.乘积A1≠A2定义为：SAA=SA×SAIAA AA=IA×IA=（I1 2 1 21 2 12A1A2A1I）\Shared（A1，A2）;=（0）1 ∪ΣO)\Shared(A1, A2);ZHA1A2=10001H∪ 共享（A1，A2）;（（s1，s2），a，（SJ1，SJ2））∈δA1<$A2若• a/∈Shared（A1，A2）<$（s1，a，sJ1）∈δA1<$s2=sJ2• a/∈Shared（A1，A2）<$（s2，a，sJ2）∈δA2<$s1=sJ1• a∈Shared（A1，A2）<$（s1，a，s1J）∈δA1<$（s2，a，sj2）∈δA2<$（（λA1（a）≤λA2（a）<$a∈<$I（s1）<$a∈<$O（sJ））<$（λA（a）≥λA（a）<$a∈<$O（s1）<$a∈<$I（sJ）））• λA1λA2 ：A1A2→N，使得A1→A2=1A1A2OA1和A2HA1A2，定义λA1<$A2我们考虑以下情况：· a∈<$A<$A <$λA <$A（a）=λA（a）如果a/∈Shared（A1，A2）<$（a∈<$Ia∈O n∈H）;· a∈<$A<$A <$λA <$A（a）=λA（a）如果a/∈Shared（A1，A2）<$（a∈<$Ia∈O n∈H）;·a ∈ A1<$A2 <$λA1<$A2（a）=min（λA1（a），λA2（a））如果a∈Shared（A1，A2）<$（（a∈我a∈在下文中，我们调整非法状态的定义，以考虑能源消耗限制。因此，产品中的状态（s1，s2）在以下情况下被认为是非法的：（i）一个组件需要来自状态s1的共享操作，而另一个组件中的状态s2没有提供该共享操作，反之亦然。(ii) 一个组件提供具有比另一组件所需动作的能耗值大的能耗值的共享动作。定义5（考虑能源消耗的非法国家）。给定两个可组合接口自动机A1和A2，非法状态集Illegal（A1，A2）S A1×S A2 的A1<$A2定义为{（s1，s2）∈S A1×S A2|a∈Shared（A1，A2）.（（a∈<$O（s1）<$a/∈<$I（s2））<$（a∈<$O（s2）<$a/∈<$I（s1））<$（a∈<$O（s1）<$a∈<$I（s2）<$λ A（a）> λ A（a））<$（a∈<$I（s1）<$a∈ <$O（s2）<$λ A（a）> λ A（a）}.定义6（组成）。给定两个相容的接口自动机A1和一台2. 组合A1<$A2是一个接口自动机，定义如下：（i）SA1<$A2=Comp（A1，A2）3，（ii）初始状态为IA<$A=IA1A2A1，A2），(iii) ）A1A2 = δ A1<$A2，（iv）跃迁集为δA1<$A2 =δA1A2（Comp（A1，A2）× Comp（A1，A2））。Σ∪Σ∪ΣΣΣΣ244S. Chouali等人/理论计算机科学电子笔记295（2013）31计算合成A1<$A2的复杂度在时间上是线性的，|和|一个2|[ 2 ]的文件。|[2]. 此方法中的验证步骤与2min是一个返回两个正实数之间的最小值的函数3从非法状态不可到达的兼容状态的集合S. Chouali等人/理论计算机科学电子笔记295（2013）3145在[2]中介绍。然而，在我们的方法中，我们考虑了接口自动机定义中的能量消耗，两个接口自动机的乘积，以及非法状态的定义。因此，我们的方法不会增加验证算法的复杂性。4.3CyCab上的插图读者可以很容易地通过应用一节中描述的算法来验证4.2在车辆和车站组合的界面自动机上（图6和图7），我们得到以下结果。在通过计算Vehicle Core和Emergency Halt组件之间的同步乘积（Vc_Eh）获得的接口自动机（图8）中，所有状态都是非法的，这是由于动作emgcy！/6在Eh自动机，这是不兼容的行动emgcy？/12，因此Vehicle复合中的组件不兼容。然而，Station组合中的组件是兼容的，因为接口自动机中的初始状态不能从非法状态4到达，所以在消除非法和不兼容状态之后，组合Cu_sss不是空的（图9）。远SPOs停止Vc含量见图8。 溶剂组合物中的相容性验证见图9。 在Station组合5相关作品在本节中，我们提出了一个简短的调查现有的工作，非功能属性（NFP）建模和评估的组件为基础的系统。规格停止？8132SPOs铜合金1停止远32pos;/3SPOs1停止远3pos;/324铜合金46S. Chouali等人/理论计算机科学电子笔记295（2013）31对于基于组件的系统，围绕组件组装中的非功能属性的分析、建模和管理已经进行了大量的研究。分析模型和属性理论在[17]中被集成到组件但是，它们需要先进的分析模型和技术，并且主要致力于特定的属性，例如延迟[17]，可靠性[15]，[4]或内存使用[13]。这些模型中的一些还可以在[16]中，作者提出了实时组件的假设保证接口代数在接口规范中，他们考虑了以下属性：每个任务序列的到达率函数和延迟，以及共享资源的容量函数该接口指定组件根据任务到达率和分配的资源容量的假设来保证一定的任务延迟。在接口兼容性验证中考虑这些属性。这些最后的方法处理组件组成中的非功能属性，但不考虑整个系统的体系结构。在[20]中，作者提出了一种在具有用TLA+表示的组件的系统中引入非功能属性的 本文的主要贡献是展示如何这些概念可以正式表示在[9]中，作者提出了资源接口来指定对有限资源有需求的组件接口这种方法允许验证组件的集合在放在一起时是否超过可用资源。这些接口通过输入和输出变量与环境进行通信在[12]中，作者提出了一种扩展的接口自动机方法，以捕获除了组件协议之外的组件接口的时序维度。定时接口被编码为输入和输出玩家之间的定时游戏。提出了一种接口兼容性在[11]中提出了一种接近时间接口的形式主义，作者基于时间输入/输出自动机形式主义提出了一个完整的实时系统规范该方法支持细化、一致性检查和组合。与我们的方法的不同之处在于，在我们的情况下，我们处理一种NF属性，即能量消耗，这种约束只需要利用加权自动机（与转换成本相关），然而在[12]中，[11]他们利用加权时间自动机：与转换相关的成本和[11]中具有时钟变量的值状态，以及[12]中具有时钟变量的值状态。这增加了组件组成验证的复杂性。在我们的方法中，我们还必须尊重SysML图，其中状态变量在组件的描述中是不允许的，而只是动作的顺序和它们的能耗。因此，我们的形式主义是不同的，从这些形式主义，它更适合建模SysML图。在这一节中，我们提出的作品，处理的图形和形式语言的组合模型NFP和验证它们。例如，建议的工作S. Chouali等人/理论计算机科学电子笔记295（2013）3147在[8]中，作者提出了一种新的构件交互规范和验证过程的方法，该方法结合了体系结构描述语言和基于模型的形式化验证的优点。[18]中提出的方法旨在赋予UML组件 以 指 定 组 件 之 间 的 交 互 协 议 。 行 为 描 述 语 言 是 基 于 层 次 自 动 机 的 启 发StateCharts。它支持系统行为的组合和细化机制。在[7]，[14]中，作者提出了将软件性能工程的技术与基于组件的软件工程相结合的工作他们区分两个模型层：软件模型，代表系统的逻辑在文献[5]中，本文重点讨论了一种非功能性质的验证，这是一种截止日期。该系统使用UML活动图的子集以数据流图的形式建模这是映射到分层和模块化的时间Petri网。该检查使用TINA工具执行。与这些相关工作相比，我们方法的贡献和独创性在于使用接口自动机指定组件接口，这些接口自动机是基于丰富符号的更一般的形式主义，可以表达更复杂的组件行为。我们还建议与SysML的连接，以验证组件的组成，考虑到非功能属性和系统架构。6结论和今后的工作在本文中，我们提出了一种方法，结合形式化和半形式化的形式化，组成组件和验证它们的互操作性。该验证根据SysML需求图指定的能耗属性、SysML块定义图指定的系统架构以及序列图指定的组件协议进行该方法采用接口自动机方法来描述组件接口并验证接口兼容性.我们已经调整了这种方法，使其更适合SysML模型的形式化。因此，我们考虑了非功能属性，并利用BDD和IBDSysML模型来指定系统架构。这些模型由树形式化地指定，其中节点对应于块，边指定块之间的连接。从这个树中，我们推导出信息，以适应接口自动机的方法，以验证接口兼容性，考虑整个系统的体系结构。需求和序列图也被利用来注释接口自动机的转换与组件服务的能量消耗相对应的成本在接口自动机方法中引入的自适应并不增加其复杂性。我们建议验证基于组件的系统的能量消耗是否作为未来的工作，我们计划植入本文所描述的算法，并评估所提出的方法更现实的案例研究。48S. Chouali等人/理论计算机科学电子笔记295（2013）31引用[1] http：//www.omg.org。[2] L. Alfaro和T. A.亨辛格接口自动机。在第九届软件工程基础年会上，FSE，第109ACM Press，2001.[3] L. Alfaro和T. A.亨辛格基于界面的设计。软件密集型系统的工程理论，NATO科学系列第195卷：数学，物理和化学，第83-104页。Springer，M.Broy，J.Gruenbauer，D.Harel和C.A.R.霍尔，2005年。[4] R. R. 一个H. 施密特 和I. Poernomo。基于构件的软件体系结构的可靠性预测。Journal ofSystems and Software，65（3），2003.[5] C. 是的，F。 Mallet和M.- A. P. 我靠 使用UML2.0和模型转换的非功能性特性分析。技术报告，INRIA研究报告，RR-5913.，2006年。[6] G. 巴耶山口Garnier，H. Mathieu和R. Pissard-Gi bollet. INRIARh甲羟孕酮-Al pesCyCab. 技术报告，INRIA，1999年。[7] Bertolino和R.一、米兰多拉基于构件的软件性能工程。在ICSE 2003第六届基于代理的软件工程研讨会：自动推理和预测，ACM/IEEE（2003）1？6. ，2003年。[8] L. 布里姆岛 切埃纳山口 Vare kov′a和B. Zimmer ova. Compone nt-i ninteractionautomataasaverification-oriented component-based system specification. SIGSOFT软件Eng. Notes，31（2）：4，2006.[9] A.查克拉巴蒂湖de Alfaro，T. A. Henzinger和M.斯托林加资源接口。在EMSOFT，第117-133页[10] S. Chouali和A.哈马德基于sysml和接口自动机的构件装配形式化验证。ISSE，7（4）：265[11] A. David，K. G.拉森A.莱盖，美国Nyman和A.华斯基时间输入输出自动机：实时系统的完备规范理论在HSCC[12] L. de Alfaro，T.A. Henzinger和M.斯托林加定时接口。在EMSOFT，第108[13] E. Eskenazi，A. Fioukov，D. Hammer和M.肖德龙从源代码组件构建的系统的静态内存消耗估计第九届IEEE计算机系统工程会议和研讨会，2002年。[14] V. Grassi和R.米兰多拉基于构件系统的自动组合性能分析。In Dujmovic，J.阿尔梅达，五，Lea，D.，编辑 ： Proc.4th Intl Workshop on Software andPerformance WOSP 2004 ， pages 59 -63 ，California， USA ， 2004. Press.[15] D. Hamlet，D. Mason和D. 沃特理论 的 软件 可靠性 基于 对 件.在ICSE 2001的会议记录IEEE计算机，2001年。，2001年。[16] T. A.亨辛格实时组件的接口代数。在IEEE实时技术和应用研讨会集，第253北京：社会出版社.[17] S.希萨姆湾Moreno，J. Sta Pasteord，and K.沃尔瑙启用可预测的程序集。Journal of Systems andSoftware，65（3），2003.[18] S. Moisan，A. Ressouche和J. Rigault。构件框架中的行为可替代性：一种形式化方法。见SAVCBS，第22-28页[19] C. Szyperski。组件软件。ACM Press，Addison-Wesley，1999.[20] S.夏勒基于组件的软件系统的非功能属性的形式化规范：语义框架及其应用。SoSyM，9：1612009年