B方法应用于组件接口互操作性的形式化描述和证明

理论计算机科学电子笔记160（2006）157-172www.elsevier.com/locate/entcs使用B精化证明组件互操作性Samir Chouali1LORIA - University Nancy 2，Campus ScientiFiqueBP239，F54506Vandoeuvre-l`es-NancyCedex，FranceMaritta Heisel2UniversitaütDuisburg-Essen，FachbereichIngenieurissenschaftenInstitutfuürMediechnikundSoftwareEngineringD-47048杜伊斯堡，德国JeanineSouqui`eres3LORIA - University Nancy 2，Campus ScientiFiqueBP239，F54506Vandoeuvre-l`es-NancyCedex，France摘要我们使用形式化方法B来描述软件组件的接口。 每个组件接口配备了一个合适的数据模型，用于定义接口操作签名中出现的所有类型。此外，必须为所有接口操作提供前置条件和后置条件。两个组件之间的互操作性通过使用接口规范的适配之间的细化关系来证明。关键词：构件互操作性，B方法。1介绍近年来，面向组件的范式[9，19]在软件工程中变得越来越它的基本思想是开发软件系统不是从零开始，而是通过组装预制部件，就像其他工程学科一样。面向组件是从面向对象发展而来的，但是部署的单元通常比简单的单元更复杂1电子邮件：Samir. loria.fr2电子邮件：maritta. uni-duisburg-essen.de3电子邮件：Jeanine. loria.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.021158S. Chouali等人理论计算机科学电子笔记160（2006）157对象在面向对象中，组件是封装的，它们的服务只能通过接口和它们的操作访问。为了真正利用面向组件的思想，必须有可能获得由第三方开发的组件，并以这样一种方式组装它们，这种方法导致以下要求：(i) 描述（即，组件的规格）必须包含足够的信息，以决定是否需要将其集成到新的软件系统中。首先，这个要求涉及到对组件源代码的访问，为了保护组件生产者的利益，可能不授予访问权限此外，组件消费者不应该被迫阅读组件的源代码来决定它是否对他们的目的有用。因此，源代码不应被视为属于组件规范。第二，它不能描述组件提供的接口（下面称为提供的接口通常，组件需要其他组件来提供其全部功能。因此，所需的接口也必须是组件规范的一部分。(ii) 对于不同的组件进行互操作，它们必须就它们之间交换的数据格式达成一致。因此，组件的每个接口都必须配备一个数据模型，用于描述组件接受和产生的数据格式它不应该只给出接口操作的签名（例如，操作foo采用两个整数并产生一个整数作为其结果），这在当前接口描述语言中是常见的。还需要描述接口操作具有什么效果（例如，操作foo采用两个整数并产生它们的和作为结果）。为了满足上述要求，组件接口规范必须包含以下信息：• 与组件的每个所需和所提供的接口相关联的数据模型（接口数据模型），• 每个接口操作的前置条件和后置条件，例如契约式设计[13]这是可能的。我们使用UML类图[4]来表示接口数据模型和形式化符号B [1]。基于这些成分，我们证明了两个组件之间的互操作性，通过使用它们的接口规范的适应之间的细化关系。组件接口之间的互操作性概念的一部分是基于规范匹配方法[24]。我们选择使用B方法，因为它的机器和精炼的基本概念与组件及其互操作性很好地吻合，并且因为该方法配备了强大的工具支持。因此，我们可以利用现有的技术来证明组件的互操作性。例如，使用对象约束语言OCL并从头开始生成验证条件将更加繁琐。请注意，我们的方法只考虑了组件的功能方面S. Chouali等人理论计算机科学电子笔记160（2006）157159nents。安全性和性能等非功能性方面当然也很重要，我们的目标是在未来的工作中处理这些问题论文的其余部分组织如下：在第2节中，我们讨论了相关的工作。然后，我们在第3节中概述了B方法。我们将在第4节中介绍组件接口的规范。两个组件之间的互操作性的概念在第5节中定义，它的验证使用了细化的概念，因为它是为B定义的。一个酒店预订系统的案例研究可以说明我们的方法。本文在第6节中以一些结论性意见结束。2相关工作在早期的论文中，我们研究了组分模型在组分指定中的作用[10]。组件模型的规格化使得可以获得单个组件的更简洁的规格化，因为这些可能涉及组件模型的规格化对于符合所讨论的组件模型的每个单独组件，无需重复组件模型规范在本文中，我们研究了组件规范必须具有的必要成分，以便对组件的软件系统的组装有用这些成分与混凝土组分模型无关已经提出了几个关于组件规格的建议。它们的共同点是，它们没有我们的接口数据模型的对应物，并且它们不考虑互操作性问题，而只考虑单个组件的规范一个基于“通用信息单元库”（GES ell S ch a ftfu？r Inform a tik，G I）的工作组已经为业务组件定义了一个该结构包括七个层次，即营销，任务，术语，质量，协调，行为和接口。我们的规范结构涵盖了术语层、协调层、行为层和接口层，并提出了具体的方法来指定这些层。GI提案的其他层与组件的非功能性方面有关。Beugnard等人[3]建议定义组件的契约。他们区分了四个层次的合同：句法，行为，同步和服务质量语法层仅指定操作签名，行为层包含前置和后置条件，同步层对应于用户协议，服务质量层处理非功能方面。Beugnard等人没有为他们的接口引入数据模型。如果两个组件可以组合，则不容易检查。Lau和Ornaghi [11]的组件指定方法更接近我们的方法，因为在那里，每个组件都有一个对应于我们的接口数据模型的上下文上下文是一种代数规范，由签名、公理和约束组成相比之下，我们认为更合适的是允许组件接口的数据模型的这使得可以考虑操作的副作用，并使用继承，160S. Chouali等人理论计算机科学电子笔记160（2006）157在实践中经常使用。Cheesman和Daniels [6]提出了一个过程来指定基于组件的软件。这个过程从一个非正式的需求描述开始，并产生一个体系结构，显示要开发或重用的组件，它们的接口和依赖关系。对于每个接口操作，开发了一个规范，由一个前提条件，一个后置条件和可能的不变量组成。这种方法遵循合同设计原则[13]。我们对组件接口的规范受到Cheesman和Daniels工作的启发，因为该工作清楚地表明，对于每个接口，数据模型是必要的。然而，Cheesman和Daniels并没有考虑到已经存在的具有可能不同数据模型的组件必须组合的情况，因此他们没有定义互操作性的概念。Canal等人[5]仅在协议级别使用多元π演算的子集来处理组件互操作性。π演算非常适合描述组件的相互作用。这种方法的局限性在于对所用语言的低层次描述及其最简语义。Bastide等人[2]使用Petri网来指定CORBA对象的行为，包括操作语义和协议。与我们的方法不同的是，我们考虑了界面规范的不变量Zaremski和Wing [24]提出了一种比较两个软件组件的有趣方法。确定一个组件是否可以替代另一个组件。他们使用形式规范来建模组件的行为，并使用Larch证明器来证明组件的规范匹配其他人[8，21]也提出通过提供签名、语义和协议级别的信息来丰富组件接口规范。尽管有这些增强，我们认为，除此之外，还需要一个数据模型来执行接口兼容性的正式验证。使用B定义组件接口的思想已经在早期的论文中介绍过[7]。3B方法B方法[1]是一种正式的软件开发方法，允许为关键系统开发软件。它涵盖了从抽象规范到实现的整个开发过程。它的基础是集合论。基本构建块是抽象机，类似于面向对象开发中的模块或类。一个B规范由一个或多个抽象机组成（B机的例子在第4节中给出）。它们中的每一个都描述了一组变量，引用这些变量的不变性属性（也称为安全属性），初始化，这是初始化变量的谓词，以及操作列表。一个操作的规范由一个前提部分和一个主体部分组成。前提条件表示每当调用操作时必须满足的要求。身体表达了手术的效果。特定系统的状态只能通过必须保持S. Chouali等人理论计算机科学电子笔记160（2006）157161def它的不变量。一个B操作OP被定义为：OP= PREP THENS END，其中P是一个前提条件，S是身体部位，表示为一个广义替换。S可以例如采用以下形状：• ssignmemtstatement：Sd=efx：=EwhichrexisavaalaeanddEisanexpression，• 多重采样：Sd=efx， . . . ， y：=E， . . ， F，• IFstatemet：Sd=efIFPJTENSJELSETJEND，其中PJ是预先定义的，SJ和TJ是置换。公式[S]Post（其中S是替换，Post是谓词）被称为S实现Post的最弱前提。它表示对任何初始状态为真的谓词，从该谓词保证S的执行达到Post。B方法提供结构化原语，允许以各种方式组合机器。大型系统可以以模块化的方式和基于对象的方式进行指定[14，12]。一个系统是通过细化来开发的，用于将抽象的规范逐步转化为更具体的规范。对于每一个细化步骤，我们必须证明细化的具体化相对于更抽象的具体化是正确的。最后，我们得到了一个实现，它细化了它的抽象规范。验证可以用B定理证明器Atelier B [18]来完成。4组件接口我们的目标是提出一种将组件指定为黑盒的方法，以便组件使用者可以在不知道其内部细节的情况下部署它们。因此，组件接口规范扮演着重要的角色，因为接口是组件的唯一访问点4.1定义组件规范必须包含所有必要的信息，以决定组件是否可以在给定的上下文中使用。这涉及组件使用的数据以及组件对其环境可见的行为。这种行为是通过服务来实现的，这些服务可以被其他组件或软件系统使用。这些服务收集在提供的接口中。但是，在许多情况下，组件依赖于其他组件提供的服务。在这种情况下，组件只有在其他组件提供所需服务的情况下才能正常工作组件所需的服务收集在所需的接口中。所需的接口是组件规范的重要组成部分，因为如果不知道还必须获得哪些其他组件，就不可能在基于组件的系统中使用该组件。接口规范由以下部分组成(1) 接口数据模型的规范，该规范规定了（i）接口中使用的类型，（ii）表示效果所需的数据状态162S. Chouali等人理论计算机科学电子笔记160（2006）157<<公司简介预订系统IHotelMgt IHotelHandling...<<客房配置>>酒店客房客户服务预订...iTakeUp预订Fig. 1. 酒店预订系统的操作，以及（iii）该数据状态的不变量。在下文中，我们使用UML类图[4]来表达数据模型，以提高可读性。然后这个类图被自动转换成B规范[14]。其他语言，如Object-Z [17]，也适用于指定接口数据模型（见[10]）。(2) 一套操作规范。操作规范由其签名组成（即，它的输入和输出参数的类型）、它的前提条件（表示在什么情况下可以调用操作）以及它的后条件（表示操作的结果）。前置条件和后置条件都将引用接口数据模型。对于每个组件接口，定义一个B机，它包含接口数据模型和操作的规范。4.2为例我们通过考虑一个酒店预订系统来说明我们的方法，这是Cheesman和Daniels [6]使用的案例研究的一个变体。使用组件的全球预订系统的体系结构在图中描述。1使 用 UML 2 表 示 法 [15] 。 它 有 两 个 提 供 的 接 口 IM akeReservation 和 ITakeReservation，以及两个必需的接口IHotelHandling和ICustomer-Handling.其中一个使用的组件是HotelManager及其导出接口IHotelMgt。在下文中，我们将更详细地考虑接口IHotelHandling和IHotel-Mgt，以证明组件HotelHandling及其接口IHotelMgt满足接口IHotelHandling的需求。4.2.1接口IHotelHandling图2显示了接口数据模型，用类图表示。相应的B规范是通过以下方式在UML类图上应用系统转换规则获得的。由于在B中所有变量必须有不同的名称，我们使用命名约定，所有变量名称都以它们所属类的 名 称 缩 写 为 前 缀 。 例 如 ， 类 ReservationDetails 的 属 性 hotel 在 B 机 器IHotelHandling中变成变量RD hotel。班 正如我们在图3中看到的，接口数据模型和它们的属性的类型被表示为集合。属性被定义为函数的变量。系统中存在的对象集，如客户，酒店和房间也被定义为变量。例如，cust被声明为集合Customer的子集。S. Chouali等人理论计算机科学电子笔记160（2006）1571631*1* 十一..** 0.. 1available（during：DateRange）：BooleanstayPrice（for：DateRange）：Currencynumber：字符串id：HotelIdname：StringresRef：验证日期：DateRange声明：BooleanID：CustId房间酒店保留客户预订详情hotel：HotelId日期：DateRange酒店详情id：HotelIdname：String分配图二. IHotelHandling接口数据模型阶级之间的联系。它们被指定为变量，其类型是对相关类进行建模的集合之间的函数或关系（取决于关联的多重性）。图4显示了B类之间的关联：Reservation和Customer，Reservation和Hotel，Reservation和Room。完整性限制。它们在B机器的INVARIANT子句中被指定为谓词。例如，表示当且仅当房间被分配给它时才要求保留的约束被表示为：（re）. （（re∈res）（（RES claimed（re）=T RU E）惠（re∈dom（asquiry Allocation）课堂操作。Room类的操作R availabale和R stayPrice被指定为变量，其类型是B机器的INVARIANT子句中表示的函数，如下所示：可用R ∈房间×日期范围→BOOLR stay价格∈房间×日期范围→货币运营它们在B机器的OPERATIONS子句中指定。图5给出了两个操作示例：getHotelDetails在其结果中产生一个酒店详细信息的集合，其中酒店名称必须与输入参数匹配-termatch;makeReservation创建一个预订，给定一些客户和一些预订细节。它的前提是预订细节中包含的酒店实际存在。 符号“||“表示并行分配。所有这些信息都被收集在一个抽象的B机器中，称为IHotelHandling可在http://www.loria.fr/~ chouali/specB获得。4.2.2接口IHotelMgt我们假设有一个组件HotelManager，可以管理不同类型的房间。图6显示了其提供的接口IHotelMgt的接口数据模型。164S. Chouali等人理论计算机科学电子笔记160（2006）157变量.ascurrentResCust、ascurrentResHot、ascurrentAllocationINVARIANT.. .assumpResCust ∈ Reservation → Customer酒店预订→酒店预订Assoc分配<$预订/→房间机器IHotelHandlingSETSReservationDetails;HotelId;DateRange;HotelDetails;Customer;CustID;Reservation;Hotel;Room;Currency变量RD hotel，RD dates，HD id，HD name，C id，cust，RES resRef，RES dates，RESclaimed，RES number，Hotel id，Hotel name，hotels，res，R number，R可用，R停留价格，客房不变/classReservationDetails/RD hotel ∈ ReservationDetails → HotelId∧RD日期∈ReservationDetails →DateRange/分类酒店详细信息/HDid ∈ HotelDetails → HotelId∧HDname ∈酒店详情→字符串/分类预订/RESresRef ∈保留→整数∧RES日期∈预订→日期范围<$RESclaimed ∈ Reservation → BOOL∧RESnumber ∈ INTEGER <$酒店介绍Hotel id ∈ Hotel → HotelId<$酒店名称<$酒店→STRING/州的系统/客户<：客户酒店预订<：酒店预订<：预订房间<：Room . . .图三. BIHotelHandling见图4。 B类之间关联的具体化接口IHotelHandling和接口IHotelMgt之间的差异是由于IHotelMgt中的新类RoomType将不同类型的房间纳入帐户。IHotelHandling的接口数据模型中存在的所有类也存在于IHotelMgt的接口数据模型中。但是，类ReservationDetails和HotelDetails现在多了一个与RoomType相关的属性。在下文中，我们仅显示接口的B规范的一部分表示与IHotelHandling相比的更改的IHotelMgt。RoomType类及其关联。图7给出了类RoomType的指定、它的属性以及类Room和Roomtype、Reservation和RoomType之间的关联。不变性质。 操作必须遵守两个重要的不变属性：S. Chouali等人理论计算机科学电子笔记160（2006）157165预订详情hotel：HotelId日期：日期范围房间类型：字符串酒店详情id：HotelIdname：StringroomTypes：String[]客户保留酒店房间ID：1个resRef：*声称：布尔联系我们1name：String1number：字符*dates：日期范围1. *available（during：DateRange）：Boolean stayPrice（for：***分配0.. 11RoomTypename：String1操作.. .hotdetts←getHotelDetalils（match）=PREmatch∈STRINGTHEN hotdets：={hdx|hdx∈HotelDetails酒店详细信息（（ho∈Hotel）HDid（ho）=HD id（hdx）（HD name（ho）=HD name（hdx））（matches（match，HD name（hdx））=TRUE））}结束语：resref<$makeReservation（pres，cus）=nPRE pres∈ReservationDetails∧cus∈CustID你好（ho∈hotels∧HD id（ho）=RD hotel（pres））THENANY HO WHERE（ho∈hotelsH id（ho）=RD hotel（pres））THEN ANYnres WHERE nres∈Reservationnres/∈resnres/∈ dom（asscore分配）nes/∈dom（asres：= resnres||ascurrentResHot（nres）：= ho|| Cid（ascurrentResCust（nres））：= cus|| resref：= RES编号+1 ||RES resRef（nres）：= RES编号+1|| RES日期（nres）：=RD日期（pres）||请求的RES（nres）：=终止图五. B操作规范见图6。 IHotelMgt接口数据模型• 对于与类Hotel的对象相关联的类ReservationDetails的每个对象，其变量RDroomType的值是与属于该酒店的房间相关联的RoomType类型的对象的属性名称（pres，ho）. （pres∈ReservationDetails<$ho∈hotelsHD id（ho）=RD hotel（pres）RDromType（pres）∈{rtn|rtn∈STRING（rty，ro）. （（rty∈RoomType）<$ro∈ Room<$ro∈assocResHot−1[{ho}]<$aslogRoomRt（ro）=rty（rtyRT name（rty）=rtn）}）• 对于与酒店相关联的HotelDetails类的每个对象，166S. Chouali等人理论计算机科学电子笔记160（2006）157操作.. .resref<$makeReservation（pres，cus）=nPRE pres∈ReservationDetails∧cus∈CustID∧你好（ho∈hotels∧H id（ho）=RD hotel（pres））THENANY HO WHERE（ho∈hotelsHD id（ho）=RD hotel（pres））THENANY romt，ro WHERE romt ∈ RoomTypeRT name（romt）= RD roomType（pres）−1ro ∈roomsro ∈asRHot[{ho}]ascurrentRoomRt（ro）=romt然后任何nres其中nres ∈预订。. . （见图5）|| assumption ResRt（nres）：= romtEND END端机器IHotelMgtSETS.. .RoomType变量.RT名称、RD房间类型、HD房间类型不变性.../房间类型/RT name∈RoomType →STRING RINGRING roomType ∈ReservationDetails →STRING RINGHD房间类型∈酒店详情→ POW（STRING）/联系我们/assumption RoomRt ∈ Room → RoomType客房预订→房间类型.见图7。 B在IHotelMgt中指定RoomT type类是与属于酒店的房间相关联的类RoomType的对象的属性名称的集合：（hdx，ho）. （hdx∈酒店详情 阿罗霍酒店HD id（ho）=HD id（hdx）RDromTypes（h dx）={rtn|rtn∈STRING（rty，ro）.（（rty∈RoomType）<$ro∈ Room<$ro∈assocResHot−1[{ho}]<$aslogRoomRt（ro）=rty（rtyRT name（rty）=rtn）}）运营接口IHotelMgt用于处理与接口IHotelHandling中同名的操作。然而，由于RoomType类的原因，操作makeReservation的规范与IHotelHandling中相同操作的规范不同（见图11）。8）。见图8。 在IHotelMgt预订5组件之间的互操作性互操作性是指两个或多个组件之间进行通信和协作的能力，尽管它们的实现语言、执行环境或模型抽象存在差异[22]。互操作性分为三个主要层次：（一）签名层次（操作签名）;这一层次包括：S. Chouali等人理论计算机科学电子笔记160（2006）157167消除了组件互操作的静态方面（ii）语义层（操作的意义）;这一层涵盖了组件互操作的行为方面(iii)协议级别：这个级别处理组件期望其方法被调用的顺序在本文中，我们只处理组件的互操作性在签名和语义级别的验证。 协议级的互操作性在[7]中进行了处理。检查组件互操作性对于基于组件的软件开发和修改至关重要，因为它允许系统设计者和实现者确定两个组件是否可以互操作，或者一个组件是否可以被另一个组件替换由于组件是由它们的接口描述的，因此必须在组件接口级别上验证组件的互操作性因此，为了验证两个组件是否互操作，有必要验证它们的接口是否兼容。为了充分利用基于组件的方法的优势，必须能够仅依赖于它们的规范而忽略实现细节来检查两个接口的兼容性。我们在第4节中给出的指定组件接口的方法是以这样一种方式设计的，即兼容性的概念可以直接基于它。5.1定义我们首先在第5.1.1节和第5.1.2节中对组件接口兼容性进行直观描述。然后，我们展示了这个直观概念如何映射到B中的精化（5.1.3节）。如果它们的接口数据模型和它们的操作是相同的，则组件CJ的所提供的接口PI可以扮演组件C的所是兼容的。5.1.1接口数据模型接口数据模型之间兼容的基本思想是RI的接口数据模型（IDM）不比PI的接口数据模型更具限制性。只有在这种情况下，PI的IDM才能代替RI的IDM。 特别是，每种类型或类别的RI必须有一个对应的PI，但不一定反之亦然。这意味着PI可能包含实现RI不需要的数据。必须区分以下情况：• 如果基本类型具有相同的名称，或者存在明确的规则声明这两种类型兼容，则它们是兼容的。• 对于类，必须满足以下条件(i) 对于RI的IDM的每个类classr，在PI的IDM中存在类classp，使得· 对于类r的每个属性，存在类p的属性，其具有兼容类型· 对于类r的每个操作opr，存在类p的操作opp，使得对于opr的签名的每个类型，168S. Chouali等人理论计算机科学电子笔记160（2006）157签名OPP。4·存在一个单射函数tr：classr→classp，它把一个r类的对象变换成一个p类的对象。 必须能够将RI对象转换为PI对象，以便将它们用作PI运营逆变换是将PI运算的输出参数转换为RI对象所必需的。对于PI中在RI中没有对应物的数据类型，不需要转换函数，因为RI可以忽略这些数据。(ii) RI的IDM中的每个关联在PI的IDM中都有对应的关联，其基数约束并不比PI的IDM中的强。(iii) PI的IDM的不变量invp意味着RI的IDM的变换不变量tr（invr）。该条件确保RI的IDM所允许的状态也被PI的IDM所允许。但是，为了显示所需的含义，这两个条件必须引用相同的数据模型。因此，出现在不变量invr（属于RI的IDM）中的数据必须由PI的IDM中的对应物替换，如函数tr所定义的。5.1.2操作的兼容性对于接口RI的每个操作opr，必须存在接口的操作oppPI使得：(i) 它们的签名是兼容的，即，对于op_r的签名的每一种类型，在op_p的签名中存在兼容类型。(ii) 变换后的opr的前提条件tr（pre（opr））蕴涵opp的前提条件。对于IDM计算所需的IDM不变量的蕴涵关系，必须对运算前提下的数据进行变换。(iii) opp的后置条件post（opp）意味着opr，tr（post（opr））.这种操作兼容性的定义对应于Zaremski和Wing [24]定义的插件匹配的概念5.1.3验证接口与B接口的兼容性在本节中，我们展示了可以在B中使用精化来证明两个组件在签名和语义级别上是兼容的。我们首先在B [1]中给出了细化的定义，然后展示了组件接口兼容性如何映射到B细化。设M和N是两个B规范。下面我们给出在M和N之间必须成立的主要条件，以证明N是M的参照。M比N更抽象，但它也可以是某些其他规范的细化;4这是签名匹配的一个简单版本。Zaremski和Wing [23]给出了代数环境中签名匹配的不同变体。 的背景下的签名匹配的讨论可以在[16]中找到。S. Chouali等人理论计算机科学电子笔记160（2006）157169我们称M为抽象的具体化。(i) 精化机的状态变量必须不同于抽象机的状态变量。(ii) 抽象规范M有一个初始化Tm，它建立了它的不变Im。一个精化规范N有一个初始化Tn和一个耦合不变量Jn。因此，如果N限定M，则Tn需要以与Tm一致（非矛盾）的方式建立Jn。形式上，Tm是Tn的一个精化，当且仅当<$[Tm]<$Jn对于从Tn可以到达的任何状态都为真。(iii) 每一个定义在M中的运算都必须定义在N中，即，所有的抽象操作都必须被细化。(iv) 如果定义在N中的运算OPn精化M中的运算OPm，则OPm和OPn必须具有相同的签名。def def(v) 设OPm= PREPm THENSm END和OPn= PREPn THENSn END分别是M和N中的两个运算。设Im是定义在M中的不变量，Jn是定义在N中的耦合不变量。当运算OPn是运算OPm的细化时，则以下条件成立：• Im<$Jn<$Pm<$[Sn]<$[Sm]<$Jn，如果运算没有输出。• 如果outm和outn分别是OPm和OPn的输出，则以下条件必须成立：Im<$Jn<$Pm<$[Sn[outn/outm]]<$[Sm]<$（Jn<$outm=outn）.• 我很高兴，这些条件表示，当操作OPm被OPn精化时，则对于Sn在Im<$Jn<$Pm成立的状态上的任何精化执行，存在Sm的抽象执行（Sm和Sn是广义子项）。 我们可以得出结论，对于任何由OPn所限定的OPm，OPm的前提条件隐含OPn的前提条件（因为限定削弱了前提条件），并且OPn的后置条件成立的状态是相关联的。其中的状态OPm的后置条件成立。现在让我们考虑这样的情况，其中M是所需接口RI的B规格，N是所提供接口PI的B规格。然后，关于初始化5和操作的M与N的B中的细化对于接口兼容性是足够的。然而，关于状态变量的不相交性的细化条件（条件（i））不能保证成立（并且对于组件接口的兼容性不是必需的）。因此，为了使用B精化来证明RI和PI之间的相容性，有必要变换PI的B精化以满足精化条件1。该转换的执行方式如下：5当把组件接口表示为B机器时，必须选择合理的初始化，例如，使用空集。170S. Chouali等人理论计算机科学电子笔记160（2006）157• PI的B规格化被转换成作为RI的细化规格化的新PI规格化，• 新PI不包含RI和PI中已经定义的集合，• 在RI和PI中定义的变量在New PI中被重命名，• New PI的不变量由PI的不变量和耦合不变量组成，PI的不变量已经应用变量重命名，耦合不变量将新引入的名称与它们在RI中的对应物相关联。在执行这些步骤之后，我们可以通过证明New PI改进RI来验证RI与PI兼容。5.2为例我们想要证明所需的接口IHotelHandling与使用B精化的所提供的接口IHotelMgt兼容图9示出了通过根据上述步骤变换IHotelMgt而获得的B规范New IHotelMgt主要变化涉及IHotelHandling中定义的变量的重命名，耦合不变量的定义以及IHotelHandling中定义的集合和不变性属性的定义。我们 使用 的 工具 Atelier B [18个国家] 到 验证 的 新的IHotelMgt酒店酒店管理。 验证结果如下。• Atelier B为B规范IHotelHandling生成了197项明显的证明义务和22项证明义务。所有这些证明义务都是自动证明的。• AtelierB产生了243个明显的证明义务和13个B规范新IHotelMgt的证明义务。12个证明义务被自动证明，1个很容易手动证明。根据这些结果，我们得出结论，新IHotelMgt细化IHotel-Handling。因此，所需的接口IHotelHandling在签名和语义级别6与所提供的接口IHotelMgt兼容。6结论和今后的工作我们已经提出了一种指定组件接口的方式，它独立于特定的组件模型。基于这一规范，我们定义了组件接口之间的兼容性概念，它允许人们检查两个组件是否我们已经证明，可以在B中使用精化来证明两个组件在签名和语义级别上是兼容的。与以前的工作相比，我们的规范包含一个数据模型，6为了转换ReservationDetails和HotelDetails类的对象（函数tr），我们使用一个名为“Standard”的默认房间类型S. Chouali等人理论计算机科学电子笔记160（2006）157171细化新IHotelMgt细化IHotelHandling设置房型变量RD hotelRef，RD datesRef，HD idRef，HD nameRef，C idRef，custRef，RESresRef Ref，RES datesRef，RES claimedRef，RES numberRef，Hotel idRef，酒店名称Ref，hotelsRef，resRef，R numberRef，R availableRef，R stayP riceRef，RTname，RD roomType，HD roomTypes，assumption RoomRt，assumption ResRt不变/n重命名变量/RD hotelRef=RD酒店IDRD日期Ref=RD日期IDHD ID Ref=HDIDHD nameRef=HDnameC idRef=C idcustRef=customRES resRef Ref=RES resRefRES日期Ref=RES日期RES claimedRef=RES claimedRES numberRef=RESnumber酒店id Ref=酒店id酒店名称Ref=酒店名称酒店Ref=酒店名称Ref/与RoomType相关的属性的类型/RT name ∈ RoomType → STRING搜索RD roomType ∈ ReservationDetails → STRING搜索HDroomTypes∈HotelDetails→POW（STRING）搜索搜索RoomRt∈Room→RoomType搜索ResRt ∈ Reservation → RoomType搜索.. .见图9。 新IHotelMgt的B规格每个组件接口。如果没有这样一个显式的接口数据模型，就不可能在不知道组件实现细节的情况下检查组件的互操作性然而，要从组件中构造一个工作系统，仅仅检查我们的兼容性条件是不够的。一旦建立了兼容性，在实际组合所讨论的组件时必须遵循所选组件模型的约定。此外，胶水代码，即，必须开发适配器，以实现所需接口数据到所提供接口数据的转换，反之亦然。在第5节给出的互操作性版本中，适配器只转换数据并调用要使用的组件的提供接口的操作。然而，可以放宽兼容性条件并使用更自由的规格匹配版本，例如，[24]第二十四话在这种情况下，适配器必须检查所提供的操作的前提条件是否成立。如果没有，它必须采取适当的操作，而不是调用提供的操作。因此，适配器的构造成为程序综合问题。对于较弱版本的规范匹配，这个问题变得更加复杂在未来，我们打算研究兼容性的替代版本以及它们到B中精化的映射，并给出相应适配器的模式172S. Chouali等人理论计算机科学电子笔记160（2006）157引用[1] J. - R.阿布里尔 《B书》 剑桥大学出版社，1996年。[2] R.巴斯蒂德岛 Sy和P. - A. 帕兰克 CORBA系统的形式化规范和原型。在ECOOPSpringer-Verlag，1999.[3] A. Beugnard，J. -M. 我也是， N。 Plouzeau和D. Watkins.M a ki ngcompone ntsco ntac arare。IEEE计算机，第38-45页， 1 9 9 9 年 7 月 。[4] G. Booch，J. Rumbaugh，and I.雅各布森《统一建模语言用户指南》艾迪生-韦斯利，1999年.[5] C.运河湖Fuentes，E. Pimentel，J-M. Troya和A.瓦莱西洛用协议扩展CORBA接口。Comput. J. ，44（5）：448[6] J·奇斯曼和J·丹尼尔斯。UML组件--一个基于UML的软件的简单过程。Addison-Wesley，2001年。[7] S. ChoualianddJ. Souqui