理论计算机科学电子笔记116（2005）227-239www.elsevier.com/locate/entcs开发时间关键系统Luigi Lavazza路易吉·拉瓦扎1，2CEFRIEL和米兰理工大学电子与信息学院意大利米兰桑德罗·莫拉斯卡3文化、政治和信息科学学院意大利科莫Angelo Morzenti4米兰理工大学电子与信息学院意大利米兰摘要开发时间关键型系统需要有表现力的、严格的、易于使用的符号来描述系统的时间相关特性，以一种足够正式的方式来支持和自动化属性验证和测试用例生成等活动。我们提出了一种双语言的方法，提供了一个描述性的形式主义，除了典型的UML（和UML-RT）图指定的系统及其组件的属性。 这种描述包括一个新的逻辑公式，称为OTL（对象时态逻辑），它是OCL的扩展。该方法适用于一个案例研究来自作者关键词：时间关键系统，验证，测试，UML，OTL，OCL1感谢所有应该感谢的2 电子邮件地址：lavazza@elet.polimi.it3电子邮件：sandro. uninsubria.it4电子邮件地址：morzenti@elet.polimi.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.079228L. Lavazza等人理论计算机科学电子笔记116（2005）2271介绍时间关键型系统的开发需要具有表达性、严谨性、易用性的符号，并同时提供软件工具。时间关键软件系统通常是复杂的，需要从几个不同的角度进行建模和分析，例如它们的功能行为，它们的时间行为和它们的结构。 在过去的几年里，UML [1]已经越来越多地用于开发复杂的系统，如实时软件，即使UML最初并不是为建模实时系统而设计的直到最近，时间特性才被添加到UML符号中（例如，参见UML 2.0的提案中对时间的介绍[4]），但它们的介绍仍然是试验性的，不完整的，并且没有很好地与UML的其他方面集成。因此，UML在实时领域的实际应用受到UML缺乏一套完整的结构来表达与时间相关的约束和属性，以及缺乏形式化语义的阻碍。这些问题的一个适当的解决方案将需要向前迈出一步，并提供高度严格的语法，特别是语义定义，以及与UML符号的其余部分的高度集成和一致性。此外，还需要一个高层次的抽象，这样符号就可以用于描述系统的高层次属性的阶段，而不是它的内部功能。在本文中，我们提出了一个扩展的UML引入时间方面，以解决这些问题，通过一组经过仔细思考和平衡的时间相关的符号，集成和一致的UML符号，使他们可以使用的从业者在工业环境中以最小的开销，并可以支持合适的开发方法，时间关键的系统.我们提出的符号是集中在架构图，对应于UML-RT协作图。系统组件以及相互包含和通信的关系通过一小组基本构造进行建模：胶囊对应于组件;端口和协议模型抽象接口;连接器对应于通信关系。将复杂系统划分为一组并行组件（即，部件）产生一个组成层次结构，其中叶对应于用状态转换机以操作风格直接建模我们还提出了一个描述性的形式主义来指定系统及其组件的属性，其风格是互补的叶级胶囊状态图。这种描述由一种新逻辑OTL（ObjectTemporal Logic ） 的 公 式 组 成 ， 它 与 原 来 的 OCL （ Object ConstraintLanguage）断言描述符号完全兼容L. Lavazza等人理论计算机科学电子笔记116（2005）227229UML中的属性在我们提出的“双重语言”方法中，OTL公式和状态图在方法层面上也是互补的。OTL公式充当约束和时间关系的抽象规范，这些约束和时间关系必须在与同一胶囊相关联的状态图机器的状态、事件和信号之间保持，因此在OTL公式和状态图提供的我们的建议是基于一般概念的，这些概念似乎既符合UML和OCL的统一版本，也符合建议草案的方向[2，3，4]。本文的组织结构如下。第2节描述了OTL，第3节描述了我们的双语方法的应用案例研究，而第4节简明地比较了我们的方法与现有的文献。结论见第5节。2OTL语言OCL可以用来描述系统及其部件的行为属性然而，当处理时间依赖系统时，OCL（以其当前形式或[2]中为OCL 2.0提出的形式）需要扩展以充分说明时间方面。 不可能在单个OCL公式中引用不同的时刻，因此只能形式化不变属性，最多包括在方法执行之前或之后对属性值的引用。系统的重要时间属性，涉及事件之间的时间距离，不能被充分地具体化，因此不可能具体化对刺激的反应必须保证在某个具体的时间间隔内发生。我们建议OTL作为一个时间逻辑扩展OCL。基于一个基本的时态算子，OTL 提供了 时态逻辑 的典型的 基本时态 算子， 即， Always ，Sometimes，Until等。此外，OTL允许建模者以定量的方式推理时间。OTL与其他UML符号完全集成在一起：它只是通过添加两个新的类来扩展OCL 2.0标准库，Time和Offset（参见图1），它们直接继承自类OclAny，并且不需要更改元模型。类时间模型的时间瞬间，这是根据当前时间作为时间原点定义的。类偏移对两个时刻之间的距离进行建模。添加到Time对象的偏移量d（参见下面的Time类的其他基本的时间相关概念，如时间间隔的概念，可以很容易230L. Lavazza等人理论计算机科学电子笔记116（2005）227≤字符串OclVoid布尔偏移时间整数房OclModelElementOclStateOclTypeOclAny它是根据时间和偏移量的概念来定义的。时间和偏移这两个类的存在允许对时间进行概念上合理的定量处理，并定义涉及这两个类的对象的合理操作。例如，Time类提供了（1）一个操作类Offset在其对象之间进行求和和减法运算。图1.一、OCL标准库扩展了类型Time和O set。时间和偏移量可以是离散的，也可以是密集的，具体取决于当前的应用。从方法论的观点来看，当对本质上连续的物理实体（例如，温度或电压），其在开发中的设备或系统的外部并且必须被监视或控制。连续实体的使用是必不可少的，即使只是为了表达用户需求，更不用说在系统需求分析中分析和证明他们的满意度[6]。另一方面，离散时间将出现在与数字同步设备相对应的模型部件中，通常在与开发中设备的详细规范、设计和实现相关的采用可能密集的时间对OTL语言的语义有影响，因为OCL假设（参见[2]，附录A关于语义）量化变量的范围仅在有限集合上，并根据有限迭代来定义量化的含义，就像迭代语句一样L. Lavazza等人理论计算机科学电子笔记116（2005）227231的编程语言。 相反，在OTL语言中，时间上的量化不能基于有限迭代，而必须以与包括算术的更传统的数学逻辑相同的方式定义。我们不期望在提供这种语义OTL的任何技术困难，但我们不包括在目前的工作，主要是空间的原因，并留下它作为进一步的发展。OTL公式的评估与一个隐式的当前时间常数。为了允许在不同于当前时间的时间对谓词p方法eval接收一个OclExpression作为参数（p），并在时间t返回p的（布尔）值。这被表示为t.eval（p），或者更简洁地表示为p@t。所有其他时态运算符都可以基于方法eval定义。特别地，属性可以在类Time的对象集合上表示，即，时间间隔。例如，公式上下文C inv：Lasts（p，d）指定p在从当前时间开始持续d个时间单位的区间内成立，如表1所定义。许多运算符同样可以被定义为指代未来（例如Futr、SomF、AlwF、WithinF、Until，其直观含义和形式定义在表1中，其中inf表示无限偏移值）和过去（例如，对应的运算符Past（p，d）、SomP（p）、AlwP（p）、WithinP（p，d）和Since（p，q））。尽管它们没有增加表达能力，但人们普遍认为，引用过去的运算符可以使规范更短，更可读，更直观。对于引用时间间隔的运算符，我们添加一个suprix来明确表示是否包含区间的极值;我们使用字母3为例我们用为意大利能源委员会[11]开发的一个数字电能表规范的片段来说明我们的双语言方法，该规范使用TRIO面向对象的时序逻辑语言[7]。这个设备当然是关键的，尽管不是“安全关键的”，因为它安装在数百万个副本中，所以它的精度和可靠性是至关重要的。该仪表由一个磁传感器（以其发明者的名字命名为G Ferraris）组成，该传感器将通过线路的电能转换为圆盘的旋转。在圆盘的外围部分，透明和不透明232L. Lavazza等人理论计算机科学电子笔记116（2005）22712激活操作者直观意义形式定义持续时间（p，d）对于将来now.futrInterval（d）->forall（t：Time|t.eval（p））未来（p，d）% d未来的时间单位p@（now + d）SomF（p）有时let I：Set（Time）=now.futrInterval（inf）in I->exists（t：Time|p@t）AlwF（p）总是let I：Set（Time）=now.futrInterval（inf）in I->forall（t：Time）|p@t）F内（p，d）在% d个时间单位内let I：Set（Time）=now.futrInterval（d）in I->exists（t：Time|p@t）Until（p，q）p保持直到q发生- curs let I：Set（Time）=now.futrInterval（inf）in I->exists（t：Time| q@t和Lasts（p，t-now））表1派生运算符。部分是均匀交替的，所以磁盘的位置和速度（分别与能量和功率消耗成比例）可以通过光电管检测到，如图2（a）所示采样(a)（b）第（1）款图二. (a)转盘和光电管;（b）光电管的激活和取样。为了最大限度地减少其磨损，光电池仅在仪表总工作时间的一小部分被激活，如图2（b）所示。一旦光电管被激活，其信号以延迟δ被采样，以允许其达到稳定状态。当磁盘从透明部分移动到不透明部分或从不透明部分移动到透明部分时，检测能量量子的消耗。一个设备称为“阅读器”的问题的采样命令的光电池和检测的完整/空的位置从读的光电池信号的磁盘。另一个设备称为CostAssign，它根据当 前 时 间 、 日 期 和 由 另 外 两 个 称 为 TariAssign 的 组 件 提 供 的 适 用tariAssign来光盘读出L. Lavazza等人理论计算机科学电子笔记116（2005）227233EnergyUsedPortPhiPortVibrations端口磁盘日期端口NoisePortPricePort激活端口Pos1PortTokenPort托特波特累加器成本分配读者Pos2Port光电管2关税光电管1环境日历G_法拉利日历。 一个叫做累加器的最终设备计算周期性发送给客户的发票总额。电能表的整体结构如图3中UML-RT协作图的简化版本所示，为了可读性，我们省略了不必要的细节。我们还采用了为连接的端口对指定相同名称的惯例。能量计的环境在图3中由胶囊环境表示，该胶囊环境为能量计提供刺激，即，所使用的能量和噪声的量，它们是时间的一般函数，前提是所使用的能量是单调不减的，并且噪声的绝对值是有限的，如本文稍后正式指定的能源报告使用端口总成本端口图三. 系统的协作图该设备受到振动，这可能会导致磁盘的位置变化很小，即使没有能量被消耗，磁盘应该完全静止。阅读器设备通过第二个光电管过滤掉这些虚假的跃迁，第二个光电管与第一个光电管的角距离等于γ/2，其中γ是光盘每个不透明或透明外围区域的角度，如图4（a）所示。这确保了两个光电池中只有一个可以生成伪跃变，因此来自第二个光电池的信号可以用于确认由第一个光电池检测到的跃变：上升沿（即，从“空”到“满”信号的切换）系统的类图如图5所示。由于篇幅原因，我们省略了协议定义，读者可以很容易地推断出这些定义。法拉利旋转磁盘，使磁盘的角度总是亲，234L. Lavazza等人理论计算机科学电子笔记116（2005）227累加器成本分配+观测值2Noise（）：DoubleEnergyUsed（）：环境Phi：双振动：双<> Phi_e：Double StartedAt：Time<> k：DoublePhi（）：双振动（）：双G_法拉利On（）关闭（）Full（）：Boolean<> n：n = 10<> N：常数/ gamma：双alfa（）：Doublegamma（）：Double pos_F（）：Boolean光电池磁盘add（tar：Double）增量：Δ = 20增量_1：Δ = 25增量_2：Δ =3100nq：n = 0<> k：DoubleEnergyUsedReported（）：双令牌（）总成本读者CurrentTariff（）：DoubleCurrentTime（）关税日历第一光电管第二光电管上升沿确认上升沿下降沿确认下降沿(a)（b）第（1）款图四、（a）盘上的不透明和透明区域;（b）边缘确认图五. 系统的类图与所使用的能量成比例。它还可能产生寄生振动，已知其振幅是有限的。这种行为可以通过以下OTL语句以纯声明的方式指定：上下文G_Ferrarisinv：abs（self.Vibrations）= Phi_einv：now >= StartedAt意味着Phi=Phi@StartedAt+K* EnvironmentPort.Energy_used（）其中Phi表示盘的旋转角度，Phie是振动的最大振幅，k是Phi和所使用的能量之间的恒定比率。属性Vibrations和StartedAt表示生成的振动，L. Lavazza等人理论计算机科学电子笔记116（2005）227235法拉利被激活的时间圆盘的特征为n，圆盘透明扇区的数量;γ，每个扇区的大小（表示为角度）（见图4（a））;N，用于使圆盘位置与所考虑的仪表型号无关的系数。gamma可以定义如下（在普通OCL中）：context磁盘inv：gamma=3.14159/self.nClass Disk配备了方法alfa（），该方法计算振动、噪声和归一化角位置Phi的总和，即，光电池所观察到的。操作alfa（）可以形式化如下：context Disk：：alfa（）：Real pre：Truepost：Result = EnvironmentPort.Noise（）+ PhiPort.Phi（）/self.N + VibrationsPort.Vibrations（）pos F（）也是磁盘的一个方法：它是一个布尔函数，声明磁盘是否（即，Φ）处于将被光电管读取为满的位置，否则为假。它由以下OCL语句context Disk：：pos_F（）：Booleanpre：self.oclInState（Active）post：letX：Double = mod（alfa（），（2*gamma））in（0 = X和X gamma）且结果=真）或（gamma = X和X 2*gamma）且结果=假）其中mod是模运算。与圆盘相关的光电池的行为由图6（a）中报告的非常简单的状态图非活动激活端口。关闭激活端口。打开激活tokenPort.token（）/nq = nq+1 ^TotPort.add（DatePort.current_tariff（））(a)（b）第（1）款见图6。 光电管（a）类和成本分配（b）类的状态图。对于光电管，指定Full（）方法很重要：context Photocell：：Full（）：Boolean pre：self.oclInState（Active）post：（observed.pos_F（）and Result =True）或（not observed.pos_F（）andResult = False）只有当光电管处于活动状态时，才能要求光电管提供位置。阅读器必须完成两个主要任务：定期激活光电管，并检测从透明扇区到不透明扇区的转换，反之亦然。Reader类的行为由图7中的状态图建模，它实现了过滤虚假转换的策略设full1和empty1为谓词，表示检测第一个光电管上的不透明或透明区域（full2和empty2的定义类似）。上下文读取器def full1：Boolean= Pos1Port.Full（）活性236L. Lavazza等人理论计算机科学电子笔记116（2005）227非活动def empty1：Boolean = not Pos1Port.Full（）第一个光电管的上升沿和下降沿由以下公式中的谓词risingEdge1和fallingEdge1定义（第二个光电管的risingEdge2和fallingEdge2的定义def risingEdge1：Boolean =full1 and Since（notfull1， empty1）def fallingEdge1：Boolean = empty1 and Since（not empty1，full1）谓词confirmedRisingEdge和confirmedFallingEdge根据前面的谓词定义如下：def confirmedRisingEdge：Boolean =risingEdge2和Since（not risingEdge2，risingEdge1）def confirmed FallingEdge：Boolean =fallingEdge2和Since（not fallingEdge2，fallingEdge1）最后，能量量子的检测发生在每个“确认边缘”-无论是这在OTL中规定如下：inv：TokePort^token（）=（confirmedRisingEdge或confirmedFallingEdge）在OCL中，消息发送只能在后置条件中指示（因为事件的时间范围是操作的执行）。在OTL中，我们可以精确地定义消息发送发生的时间，因此我们不限于仅在后置条件中使用此构造。上面的OTL公式是电能表读卡器组件模型的一部分，有助于指定其行为，通过状态图实现（图7）。活性after（delta）[Pos1.GetPosition（）]后（delta）[Pos1. GetPosition（）和Pos2.GetPosition（）]在（delta）[Pos1.GetPosition（）]之后^Distrib.tokenFullAfter（delta）[Pos1.GetPosition（）]E_F后（delta）after（delta）[not Pos1.GetPosition（）]After（delta）[Pos1. GetPosition和F_E[ not Pos1. GetPosition而不是Pos2。在（delta）Pos2之后的GetPosition（）]。getPosition（）][notPos1.GetPosition（）]后（delta）[not Pos1.GetPosition（）和after（delta）[Pos1.GetPosition（）]不是Pos2.GetPosition（）]^Distrib.token（delta）后为空[不是Pos1.GetPosition（）]Hafter（delta）[not Pos1.GetPosition（）]Waiting_to_start之后（delta_2）^光电管.开之后（delta_1）^光电管.关^光电管.开见图7。 类Reader的状态图。光电池的激活可以通过OTL语句来指定L. Lavazza等人理论计算机科学电子笔记116（2005）227237如下所示（其中延迟是常数）：上下文读取器inv：ActivatePort^On（）@StartedAt+delayinv：ActivatePort^On（）@现在意味着(not ActivatePort^Off（）@现在和Lasts_ee（not（ActivatePort^On（）or ActivatePort^Off（）），delta1）andActivatePort^Off（）@now+delta1）inv ActivatePort^Off（）@现在意味着（不是ActivatePort^On（）@现在，Lasts_ee（not（ActivatePort^On（）or ActivatePort^Off（）），delta2）和ActivatePort^On（）@now+delta2）Reader向CostAssign单元提供消息令牌，CostAssign单元使用它们，如图6（b）中的状态图所指定。每次CostAssign单元接收到令牌时，它递增变量nq，变量nq表示接收到的令牌的总数，并调用累加器单元的加法操作，基于当前日期和时间指定当前令牌消耗的能量的总量通过将令牌的数量nq乘以常数k（能量“量子”）来计算。因此，累加器单元能够计算所消耗的能量的价格模型的一些全局性质也可以用OTL表示。器械报告的已用能量量单调非递减。下面的OTL语句通过单调性的通常定义来描述这个要求，其中D（间隔的长度）是在类CostAssign的上下文中定义的常数值：上下文成本分配inv：letDS = Set（Offset）=[0.. DS中的D]-> forall（d：偏移|EnergyUsedReported（）>= past（EnergyUsedReported（），d））以固定价格消耗的能量的成本与消耗的能量和价格成比例地增加。给定长度为IL的任意时间间隔，其中可应用的电价是恒定的，所消耗的能量的总成本的变化是电价与在间隔IL期间所消耗的能量的乘积：上下文累加器inv：letTS = Set（min）=[minTariff.. maxTariff] inTS-> forall（tr：|Lasted（Tariff.CurrentTariff（）=tr，IL）意味 着TotalCost - past（TotalCost，IL）= tr*（CostAssign.EnergyUsedReported（）-过去（CostAssign.EnergyUsedReported（），IL）在预定的恒定长度TSL的任何时间跨度（例如一周或一个月）内，报告的能量和实际使用的能量之间的差异（绝对值）总是小于对应于量子的能量，比如量子能量：上下文成本分配inv：abs（EnergyUsedReported（）-past（EnergyUsedReported（），TSL）-（Environment.EnergyUsed-past（Environment.EnergyUsed，TSL）<量子能量238L. Lavazza等人理论计算机科学电子笔记116（2005）227这一属性保证消费者不必支付超过到期的费用，而能源公司不会得到少于到期的费用这些全局性质以及可能附加到组分胶囊的任何性质可用于系统的分析和验证4文献复习在最近的文献中出现了一些建议，以严格、一致的方式在UML中引入计时特性。其中一些不涉及度量时间，因此我们在这里不回顾它们。在明确处理度量时间的建议中，可以考虑一些有代表性的建议Flake等人[8]为OCL提供了一个面向状态的时间扩展。引入了状态序列的形式化概念，并在此基础上定义了时间特性。语法与OCL语法保持一致。然而，作者自己注意到OCL语法可能有点笨拙，并且可以使用不同的约束语言，只要使用到OCL的翻译机制。Roubtsova等人使用了密集时间。[9]，他们的方法考虑了类图和状态图，但不考虑OCL，基于为OCL提供路径概念将超出OCL框架的想法。时间属性被表示为与形式约束相关联的所谓的规范类。一个特定的类与一个实际的类有特定的关系。一个有趣的方面是，大多数方法倾向于使用基于时态逻辑的语法，而不是类似OCL的语法。Sendall和Stroheimer [10]再次在UML状态图上引入了定时特性，并提供了五种属性来捕获时间依赖系统的时间方面，即事件可能发生的时间，活动的持续时间和状态转换的频率，因此该方法可以用于指定实时和性能属性。然而，上述方法都没有提供允许设计者在不明确引用操作模型的元素的情况下正确地描述系统需求的逻辑。OMG文档然而，似乎整个文档的构思主要是为了支持设计和实现，而不是规范。 因此，它提供了一些机制使用此配置文件，可以编写状态图，指定系统对时钟和定时器生成的事件的反应时间行为。这是描述实现的合适方式L. Lavazza等人理论计算机科学电子笔记116（2005）227239但是在不存在定时器和时钟的问题域中几乎不适用。5结论实时关键应用程序的开发需要特定的过程和严格的符号。我们提出了一个我们的建议支持系统和严格的开发，集中在明确的，可能是正式的需求规范，以及通过分析进行的需求验证和验证，可能是通过演绎方法或模型检查进行的属性证明。引用[1] OMG，网址：http://www.omg.org。[2] “Response to the UML 2.0 OCL RfP, Revised Submission,Version 1.6”, January 6, 2003, OMGDocument[3] “Unified Modeling Language: Infrastructure, version 2.0, Updated submission to OMG RFP[4] “Unified Modeling Language: Superstructure version 2.0, 3[5] “UML Profile for Schedulability, Performance, and Time Specification”, OMG Adopted[6] Gargantini，A.和Morzenti，A.，关键系统的自动演绎需求分析，ACM TOSEM，10（2001），225[7] Morzenti，A.San Pietro，P.，时间关键系统的面向对象逻辑规范，ACM TOSEM，3（1994），56[8] Flake，S. Mueller，W. 面向静态和时态状态的OCL约束的形式语义。SoSyM 2（3），2003年10月。[9] Roubtsova，E.，Van Katwijk，J.，Toetenel，W.和De Rooij，R.，Real-Time Systems：Specification of Properties in UML，in Proceedings of ASCI 2001，May 2001，188[10] Sendall，S.，和Strohmeier，A.，使用OCL和UML分析并发系统行为和时间，Proc. of UML2001，LNCS 2185，2001年10月，391[11] Morzenti，A. ，Paci，M. 和Veroni，F. “S p e c i f i c h a T R I O d e l l ' U n i t` a d i E l a b o r a z i o n e P e r i f e r i c a ” ， 1 9 9 3 年 1 月 1 9 日 ， 草 案 第 3版 ， 意 大 利 文 。
我的内容管理
展开
