饮料自动售货机的面向对象规格说明

理论计算机科学电子笔记102（2004）155-173www.elsevier.com/locate/entcs应用Fondue指定饮料自动售货机Alfred Strohmeier，Thomas Baar1软件工程实验室瑞士洛桑联邦理工学院（EPFL）CH-1015 Lausanne，SwitzerlandShane Sendall2日内瓦大学计算机科学系软件建模与验证实验室24，rueduG'en'eral-Dufour，CH-1211Gen'eve4，Switzerland摘要本文的目的是提出我们的方法，在分析过程中指定系统的行为，火锅软件开发方法的一部分。 该方法以案例研究为例，饮料自动售货机（DVM）它基于操作模式和协议模型。协议模型通过UML协议语句机描述了系统操作的时序。操作模式通过前置条件和后置条件描述系统操作的功能;它们是用对象约束语言（OCL）编写的，有一些修改和扩展。我们的方法在用例的非正式描述和UML中面向解决方案的对象交互模型之间提供了一个中间地带。我们相信，声明式行为规范技术，如本文中提出的技术，可以让人们对软件的质量更加自信，因为它们允许人们对系统属性进行推理关键词：面向对象软件开发;软件开发方法;软件规格说明;形式规格说明;统一建模语言（UML）;对象约束语言（OCL）;火锅软件开发方法。1电子邮件：[阿尔弗雷德.施特罗迈尔|电子邮件：epfl.ch2电子邮件：Shane. cui.unige.ch1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.09.008156A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-1介绍UML与OCLUML [7]是一种非正式建立的语言，它提供了一组丰富的符号，用于对开发中的面向对象系统的静态和动态方面进行建模。目前在工业中，许多被松散地归类为系统规范的内容都是通过用例来执行的[2]。用例是捕获软件系统行为需求的一个很好的工具它们是非正式的描述，几乎总是用自然语言编写的，因此它们缺乏严谨性和推理系统属性的基础另一方面，Z [12]和VDM [5]等形式化规范方法通过前置条件和后置条件提出了系统行为的声明性规范。它们提供了对系统特性进行推理的能力，并促进了严谨性和精确性。他们通过在概念模型上陈述系统的变化来定义系统行为。另一方面，用例定义了系统和外部参与者之间的交互，包括参与者目标、利益相关者关注点和系统责任。正式规范通常也需要高水平的数学成熟度来阅读和理解，因此不像用例那样主要针对利益相关者的理解。像Z和VDM这样的形式化方法存在这样的问题，即它们引入软件开发环境的成本非常高，因为它们对用户的数学成熟度有很高的要求。另一方面，作为UML [7]的一部分，OCL的优势在于它是一种面向开发人员的相对OCL简单的秘密之一是它使用导航和操作符来操作集合而不是关系。而且，OCL的创建是为了导航UML模型的独特和唯一的目的，使其成为在使用UML建模系统时描述约束和表达谓词的理想工具。火锅Fondue是洛桑联邦理工学院软件工程实验室开发的一种面向对象的软件开发方法。Fondue以一致的方法涵盖了从需求获取和分析到设计到实现的所有阶段。正如我们将看到的，它使用OCL编写的前置条件和后置条件，从基于用例的需求引导到系统操作规范Fondue方法首先在[10]中描述，然后通过添加需求启发活动来增强[11]。火锅分析-A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-157需求模型分析模型行为模型设计运营模式概念模型协议模型环境模型案例模型域模型姐妹阶段，以及更先进的，有点投机，材料被记录在一个博士。论文[9]。Fondue起源于著名的Fusion方法[3];它采用了它的过程，但使用了UML符号。除了融合，用例被提议用于需求获取，并在分析阶段被考虑在内。Fondue方法不仅提供了类模型的内部视图和单个类的行为，而且还包括系统范围功能的建模和一个逐步的过程，该过程引导开发团队从初始需求文档到面向对象软件系统的实现。Fondue定义了许多可交付成果，其中之一定义了系统行为的规范。该规范包括三个主要观点[10]，见图。1.一、A依赖于B：B的变化引起A的变化Fig. 1.火锅规格型号• 操作模型：操作模型由操作方案组成操作模式通过OCL编写的前置和后置断言描述操作执行对系统状态和系统输出消息的影响• 协议模型：UML状态图的一种受限形式，定义了操作的允许时间顺序;• 概念模型：使用UML类图158A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-表示法，它定义了描述操作模式中操作执行结果所需的系统状态。底层系统模型本质上是反应式的，与环境的所有通信都是通过发送消息来实现的。收到消息后，会触发一个异步事件，该事件最终可能会触发系统操作。环境模型消息签名，更重要的是，与属于系统周围环境的参与者的消息交换显示在一个辅助模型中，称为环境模型。概念模型概念模型是一种特殊用途的类模型，用于描述系统的所有概念和关系部分，以及环境中存在的所有参与者。因此，我们在这里定义的类模型不是设计类模型。类和关联对问题域的概念建模，而不是对软件组件建模。对象和关联链接保存系统状态。类没有行为;将操作或方法分配给类的决定被推迟到设计时。运营模式操作模式描述了操作对系统的抽象状态表示的影响以及发送给外部世界的消息。它以声明的形式编写，从系统内部的对象交互中抽象出来，最终实现操作。它通过前置条件描述假设的初始状态，通过后置条件描述操作执行后系统状态的变化。操作模式使用UML的OCL形式主义，其构建的目的是让开发人员可以读写我们在这里定义的操作模式指定了被假定为原子地和瞬时地执行的所有系统操作都由输入事件触发，通常与触发消息和触发的操作同名。由操作执行引起的状态变化是根据对象、属性和关联链接来描述的，这些都在概念模型中描述。系统操作的后置条件可以断言对象被创建，属性值被更改，关联链接被添加或删除，以及某些消息被发送到外部参与者。A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-159对象之间的关联链接就像一个网络，保证可以导航到操作所需的任何状态信息协议模型一个协议模型是一个UML协议状态机，它只关注系统操作的时间顺序，因此UML状态图符号的使用是非常具体的，只有有限的使用是由符号。操作模式描述了系统提供的服务，而协议模型描述了这些服务的允许顺序。行为模型操作模型和协议模型都是从用例中提炼出来的，它们结合起来定义了系统行为的精确规范，即行为模型。在[11]中已经提出了一种将用例映射到操作模式的方法为了了解这项工作如何适合软件开发分析活动，读者可以参考[10]。为例将在饮料自动售货机上展示使用火锅方法指定系统这台机器相当于一个典型的，但简单的，反应系统。它由一个控制器和若干外围硬件设备组成，控制器的软件有待开发。这些设备通过交换异步消息与软件系统交互。消息的排序约束由协议模型指定，而接收消息的效果由操作模式指定。本文结构我们从第2节开始，非正式地提出问题，即饮料自动售货机。这种机器的典型用法在第3节的用例中描述。 在第4节中，我们通过对饮料自动售货机的环境进行建模，开始详细说明相应的火锅规范。第5节给出了它的概念模型。第6节中的协议模型显示了在饮料自动售货机上执行的允许操作顺序。第7节的操作模型完成了规范。第8节陈述了所吸取的教训并得出了一些结论。160A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-2原始问题陈述使用自动售货机时，通常需要采取以下步骤(i) 消费者将硬币放入机器中，(ii) 他/她选择想要的饮料，(iii) 分配器通过底部抽屉供应饮料我们必须区分三个层次：物理机器、控制器和人机交互。物理机器由几个组件组成：一个存钱罐、饮料架、一个信息面板、饮料选择按钮和一个弹出硬币按钮。控制器是一个程序，它通过接收来自系统组件的消息和向它们发送命令来协调系统组件的活动。消费者或服务人员与系统组件之间发生人机交互，例如，消费者按下饮料选择按钮或服务人员打开货架。钱箱由两个不同的硬币收集器组成：第一个收集器保存硬币，直到消费者按下弹出按钮或选择饮料;在后一种情况下，硬币由第一个收集器释放到第二个收集器。饮料存放在架子上。每个货架与饮料种类和价格相关联。服务人员将饮料添加到货架上。最初，有没有饮料。 该系统有一些限制：• 消费者只能投入硬币直到大于最高饮料价格的一定限度;任何额外的硬币将由第一收集器立即释放（以便强制消费者选择饮料或按下弹出按钮），• 储钱盒（第二收集器）具有有限的容量，• 机器拥有的架子的数量是固定的（即，在系统的整个寿命中是恒定的• 每个搁架被细分为槽，• 每个槽最多只能喝一杯，• 所有盘架都具有相同数量的插槽，并且在系统的使用寿命内，插槽数量是固定的。3用例图2所示的用例图非常简单。基本信息保存在用例描述中。描述用例的Fondue格式类似于Cockburn [2]提出的格式A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-161饮料自动售货机买饮料消费者服务DVM服务人员图二. 饮料自动售货机用例图像往常一样，在分析过程中发现问题陈述，包括用例，是不精确和不完整的。我们在这里提供一些额外的规则：(i) 当钱盒（第二收集器）是满的，然后DVM得到了秩序。(ii) 只要DVM没有出故障，它就能够收集购买饮料所需的钱。换句话说，钱盒（第二收集器）要么是满的，要么它有足够的容量收集另一杯酒的钱。(iii) 当一个架子上的最后一杯饮料送来时，它报告说它已经空了。(iv) DVM没有一个聪明的货币系统。例如，人们可以此外，它是那么容易返回的硬币是太多的价格相比3.1购买饮料使用案例：购买饮料经营范围：饮料自动售货机级别：用户目标，黑盒情境中的意图消费者的意图是从机器中购买饮料这涉及到用一定数量的钱换一杯饮料。主要参与者：消费者前提条件：系统必须初始化（其中货架具有已知价格）。主要成功场景：1. 消费者将一枚硬币放入机器。步骤1可以根据消费者的意愿重复多次2. 消费者选择饮料。162A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-3. 系统验证是否有足够的资金用于选择，收取指定金额的钱（将多余的钱返还给消费者）* 并分发饮料。4. 消费者从机器中获取饮料。扩展：1a. DVM出故障了：1a.1. 系统释放插入的硬币;1a.2. 消费者收钱;用例以失败（1-2）a.消费者要求退款：（1-2）a.1.系统回收资金。（1-2）a.2. 消费者收钱;用例以失败告终。3a.系统确定购买资金不足：3a.1.系统通知消费者;用例在步骤1或2继续。3b.系统确定该类别中没有剩余的饮料：3b.1。系统通知消费者;用例在步骤1或2继续。4 你好 钱箱通知系统它已满：4.系统通知消费者系统出现故障 **;用例结束。注：* 我们需要注意的是，消费者不是在选择饮料后要求弹出钱，而是在系统接收钱之前，即，这样消费者就不能成功地拿回他/她的钱和饮料。** 系统保持故障状态，直到服务人员重置。3.2服务DVM用例：服务DVM范围：饮料自动售货机级别：用户目标，黑盒上下文意图：服务人员的意图是通过确保机器有饮料可用并收集所赚的钱来维护系统主要演员：服务人员主要成功场景：1. 服务人员将饮料添加到架子上。2. 服务人员设置或更改货架上饮料的价格。以任意顺序对每个搁板重复步骤1和23. 服务人员收取机器赚的钱。A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-163DVMController扩展：–注：步骤1和2构成系统的初始化4环境模型退出货币~~~insertMoneyboxIsFullboxIsNotFull- -一种~弹出Btnreturn货币获取货币释放货币钱盒*选择饮料~~~setPriceOfShelf- -一种ShelfSelectBtn*已补充显示货币保险基金饮料不可用outOfService价格面板~~-物理货架giveDrink信息面板图三. DVMController的环境模型用例提供了系统行为的结构化但非正式的描述。为了得到一个正式的行为描述，我们首先必须识别系统的子组件以及它们之间的通信方式。作为下一步，火锅因此提出了一个环境模型的发展，如图。3 .第三章。环境模型识别系统发送到环境和从环境接收的所有消息。环境是由演员塑造的。请注意，Fondue允许（与官方UML相反）用一颗星（PhysicalShelf、ShelfSelectBtn）。这表明参与者的多个实例可以与系统交互在环境模型和用例图中有不同的参与者可能是一个惊喜。一旦意识到我们主要对饮料自动售货机的软件部分感兴趣，这种困惑就消失了，即协调系统组件活动的控制器。通过在控制器和组件之间发送消息来实现协调。从控制器的角度来看，系统的组件属于环境。可能会出现以下问 题 ： 如 果 系 统 的 组 件 构 成 了 环 境 ， 那 么 用 例 中 使 用 的 参 与 者Consumer和Service Person属于哪里？但在这一点上，他们没有发挥任何作用。它们通过按下164A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-弹出按钮、将钱插入钱箱等。然而，对于DVMController，如何执行人与系统组件的交互（即消费者如何按下按钮）并不相关。控制器的相关性仅具有交互的结果，例如按钮被按下的事实。图3中给出的环境模型缺少一些在接下来的开发步骤中既必要又有用的信息。为了简洁起见，图中不显示消息的参数。下表列出了这些信息以及对参与者和信息的非正式描述。该详细描述有助于理解下一节中的弹出BtnejectMoney（）一个按钮，用于弹出当前插入到第一个钱箱收集器中的所有硬币已按ShelfSelectBtnselectDrink（）用于选择饮料架的按钮;每个ShelfSelectBtn对应于一个PhysicalShelf（参见第5节中的概念模型）选择按钮已被按下物理货架isEmpty（）isReplenished（）giveDrink（）物理饮料架;分为插槽和存储饮料所有插槽都是空的;假设：isEmpty（）发生在最后一个可用的饮料被分配货架已被补充，且不再是空，DVMController请求分配一杯饮料MoneyBox由两个收集器和一个返钱器组成。当第一个收集器装满时，额外的硬币会掉落;当第二个收集器的容量超过时，DVM等待服务人员耗尽第二个收集器insertMoney（m：Money）投入一枚m的硬币（第一个收集器未满）A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-165boxIsFull（）第二个收集器已满，即没有ca-（在为一杯酒的钱收好之后）boxIsNotFull（）第二个收集器再次具有足够的容量，对于另一个饮料; boxIsNotFull（）在服务人员用完第二个收集器return Money（m：Money）来自DVMController的请求，以将指定的金额m弹出给消费者takeMoney（）请求从DVMController释放所有当前插入第一个收款机的钱到第二个收款机releaseMoney（）请求DVMController弹出所有货币当前插入第一个收集器服务人员用于为每个货架设置的PricePanel面板饮料的价格setPriceOfShelf（s：Shelf，price：Money）s货架上饮料的价格被设定为显示状态信息的InformationPanel组件;不同可以显示多种信息（例如文本、图形、灯光等）display Money（m：Money）来自DVMController的请求，显示m作为当前插入到第一个收集器中的货币量insu funcientFunds（on：Boolean）如果on=true：来自DVMController的请求，以显示一个文本，说明当前插入到第一收集器中的 钱 不 足 以 支 付 所 选 择 的 饮 料 ， 如 果on=false：来自DVMController的请求，以擦除这种较早的文本drinkNotAvailable（on：Boolean）类似于保险基金;所选饮料的货架是空的166A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-11钱盒1outOfService（on：Boolean）类似于InsurencientFunds;系统出现故障，等待服务人员进行维护5概念模型一旦消息被识别，下一个目标是描述系统在接收和发送输入消息后的行为。然而，行为取决于DVMController的内部状态，因此我们首先需要描述DVMController的内部结构。图中的概念模型4通过类图提供了这样的描述1价格面板1物理货架见图4。 DVMController的概念模型信息面板属性“已注册”使DVMController能够跟踪当前插入到第一个收款机中的货币。属性collectingMoney和outOfOrder记录DVMController的当前状态（另请参见第6节中的协议模型）。组件类Shelf是组件PhysicalShelf的逻辑表示，它有两个具有明显含义的属性。PhysicalShelf、ShelfSelectBtn和Shelf之间的两个关联以及所选的多重性确保每个ShelfSelectBtn恰好属于一个PhysicalShelf。id构造型意味着系统可以从属于系统的对象开始识别参与者，例如，给定一个shelfs ， 我 们 可 以 找 到 它 对 应 的 物 理 shelf ， 在 OCL 中 表 示 为s.physicalShelf。的原因ID刻板的关联是系统只能向可以识别的参与者发送消息。 识别系统内部的外部参与者形式将是id定型关联的唯一用途1弹出Btn11*1ShelfSelectBtnID1ID1*11系统DVMController已注册：Money=0collectingMoney：Boolean outOfOrder：Boolean产品展示isEmpty：BooleandrinkPrice：Money111A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-167isEmptyisReplenishedsetPriceOfShelfinsertMoney准备insertMoney选择Drink收款boxIsFullejectMoney选择DrinkisEmptyisReplenishedsetPriceOfShelfinsertMoneyboxIsNotFullOutOfOrderDVMController6协议模型图五. DVMController的协议模型协议模型定义了系统操作的时间顺序。来自环境的DVM的每个输入消息引用异步操作调用和相应的事件。消息、事件和被调用的系统操作通常具有相同的名称。一个协议模型是用UML状态图来描述的，它没有保护。通常，只有当系统处于分派状态时，协议模型中的转换才由输入事件触发，即，存在具有输入事件的名称的弧。如果不是，则忽略输入事件。从一个状态到另一个状态的转换导致执行与输入事件同名的系统操作。我们只对图5中状态的含义作一个简短的非正式解释。就绪状态表示允许消费者和服务人员与系统交互的情况。第一个收款机中没有钱，信息面板上也不显示任何状态信息一旦事件insertMoney被分派，状态就离开了。目标是筹集资金。由于事件insertMoney触发了从CollectingMoney到CollectingMoney的自转换，因此可以将更多的硬币插入第一个收集器。请注意，一旦它是完整的第一个收集器将拒绝额外的硬币自动不发送insertMoney消息168A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-到DVMController。这样，第一个收集器的容量问题就由演员MoneyBox本身“机械地”解决了在 CollectingMoney 状 态 下 调 度 事 件 ejectMoney 会 导 致 转 换 为Ready。在发送状态为Collecting-Money的selectDrink事件后，触发的转换是不确定的。控制器可以将其状态更改为就绪状态，也可以保持在CollectingMoney状态，具体取决于插入的货币数量和饮料的可用性。在协议模型中允许不确定的状态变化，因为一旦考虑到操作行为，不确定性通常会消失在状态Ready中，忽略事件selectDrink和ejectMoney 这是合理的，因为在就绪状态下，第一个收集器中没有钱来支付选定的饮料，也没有钱 把 它 还 给 消 费 者 。 注 意 ， 状 态 OutOfOrder 中 的 情 况 与 事 件insertMoney 不同。尽管DVM 在处于OutOfOrder 状态时等待ServicePerson进行维护，但此处不能忽略事件insertMoneyInsertMoney由于要求而属于不可验证事件组。回想一下，insertMoney发生在消费者成功地将一枚硬币引入第一个收藏家之后，即消费者已经支付并期望得到一杯饮料或至少拿回钱。请注意，为了防止消费者在机器故障时投入硬币，我们需要进一步的假设，例如。第一个收集器被锁定。在状态Ready中，可以分派事件isEmpty以及boxIsFull，从而分别导致 状 态 转 换 为 Ready 和 OutOfOrder 。 这 两 个 事 件 isReplenished 和setPriceOfShelf在状态Ready或OutOfOrder下分发时会导致自转换。在就绪状态下，将忽略事件boxIsNotFull。当在状态OutOfOrder下调度时，它会导致状态转换为Ready。6.1同步问题假设UML状态图的标准语义，上面给出的协议模型仍然是不正确的。为了解决以下问题，需要对同步消息处理进行额外的假设：一旦检测到储物架为空或储钱箱（第二收集器）已超出其容量，就会发送isEmpty和boxIsFull消息。为了使DVM正确工作，有必要假设所有其他稍后发送的消息也将在稍后处理。但是，如果假设UML状态图的当前语义，则不能保证假设，除了isEmpty和boxIsFull之外，在DVM的输入队列中还有另一个事件，比如- sertMoney。可以在isEmpty和boxIsFull之前调度insertMoney，尽管它是在它们之后提出的。A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-169^一旦DVM处理了insertMoney，它就处于CollectingMoney状态，其中isEmpty和boxIsFull将被简单地忽略。这显然会导致不正确的行为。所描述的效果是基于消息的异步系统的固有问题7运营模式到目前为止，并非系统行为的所有方面都在协议模型中表达，例如：我们希望指定，通过将货币插入第一收集器，货币显示也被更新。幸运的是，丢失的信息可以通过OCL约束以一种优雅的形式表示操作模型包含所有输入消息的效果的详细行为规范。由于输入消息仅仅是操作调用，因此每个输入消息都有一个对应的操作，通常具有相同的名称。具体化主要由OCL前置/后置条件给出。为了简洁起见，一般框架假设被认为是理所当然的后置条件的语义。规范的框架是可以通过操作[6]改变的所有变量的列表。 规范的后置条件描述了框架变量的所有变化，由于规范是声明性的，后置条件还必须声明所有保持不变的框架变量。避免这种额外工作的一种方法是暗示“.“没有什么可以改变这意味着指定意味着框架变量根据后置条件而改变，而未提及的框架变量保持不变。这种方法减少了规范的大小，从而增加了它的可读性，并使编写规范的活动更少出错。大多数操作产生输出消息，这些消息被发送给参与者。因此，该规范利用了最近整合到OCL中的消息构造。表达式接收器消息只能出现在操作的后置条件中，并指示在操作执行期间消息消息已被发送到对象接收器。详细说明见[8，2.7节]。我们规范的另一个特点是使用了关键字sender。这个关键字不是OCL标准的一部分，但在我们的规范中已经被证明是非常有用的。 关键字sender指的是调用操作的参与者。回想一下，Fondue中的每个操作只有在分派了具有相同名称的消息关键字170A. Strohmeier et al. / Electronic Notes in Theoretical Computer Science 102（2004）155-BBBBBBBBBBBBBBBBself.collectingMoney=falsesender允许在OCL表达式中访问已分发消息的发送方。它类似于关键字self，它提供对已调用操作的对象的访问。操作：DVM：：ejectMoney（）使用案例：购买饮料消息：InformationPanel：：{DisplayMoney，Insu PancientFunds，DrinkNotAvailable}MoneyBox：：{ReleaseMoney}上一页：Post：self.moneyBox releaseMoney（）和self.informationPanel显示Money（0）和self.informationPanel保险资金（false）和self.informationPanel饮料不可用（false）和self.collectingMoney =false操作：DVM：：selectDrink（）使用案例：购买饮料消息：InformationPanel：：{DisplayMoney，Insu PancientFunds，DrinkNotAvailable}MoneyBox：：{ReturnMoney， TakeMoney上一页：PhysicalShelf：：{GiveDrink}Post：if sender.shelf.isEmpty thenself.informationPanel drinkNotAvailable（true）和self.informationPanel保险资金（false）和self.collectingMoney=trueelsif self.shelf. drink registered sender.shelf. drink price thenself.informationPanel insufficientFunds（true）and

下载后可阅读完整内容，剩余1页未读，立即下载