离散控制器综合与安全关键嵌入式系统

理论计算机科学电子笔记133（2005）81-100www.elsevier.com/locate/entcs离散控制器综合Alain Girault，Eric Rutten1INRIARhone-Alpes，PO PART，655 avenue de摘要嵌入式系统需要基于形式化方法的安全设计方法，以及基于容错技术的安全本文提出了一种安全执行系统的安全设计方法：它使用离散控制器综合（DCS）来生成正确的重构系统。强制执行的属性涉及一致执行，功能实现（无论故障如何，在某些故障假设下）和几个优化。我们提出了一组周期性的任务，一组分布式的，异构的和故障沉默的处理器，和一个环境模型，表示潜在的故障模式的模型模式。我们概述了我们的方法的实现，使用Sigali符号DCS工具和模式自动机。关键词：离散控制器综合，容错，实时系统。1介绍1.1安全关键嵌入式系统嵌入式系统在关键应用（航天、航空、核能）中占了很大一部分。. .）以及公共领域应用（汽车、消费电子产品）。. .）.其主要特点是：• 对偶自动控制/离散事件：它们包括在采样时间内被建模为微分方程的控制律，迭代计算，以及根据模式切换对控制律进行排序的离散事件系统1电子邮件：Alain. inrialpes.fr，Eric. inrialpes.fr1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.08.05982A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81• 关键实时性：未满足的时间限制可能涉及导致灾难的系统故障;• 有限的资源：由于重量和负担、功耗（自动驾驶汽车或便携式设备）、抗辐射性（核或太空）或价格限制（消费电子产品），它们依赖于有限的计算能力和内存;• 分布式和异构体系结构：它们通常是分布式的，以提供足够的计算能力，并使计算站点靠近传感器和执行器。1.2问题陈述嵌入式系统本质上是关键的，因此必须确保它能够容忍处理器故障。这甚至可以激励其分配本身。在这种情况下，至少一个计算站点的丢失不得导致整个应用程序的丢失。我们感兴趣的是正式的方法来模拟系统的容错保证。在现有的各种形式化方法中，我们研究了离散控制器综合（DCS）的使用使用DCS的优点是所产生的系统的正确性和控制器的容易修改性（由于自动工具），即，在同一系统模型上研究和测试多个容错目标或故障假设的可能性具体而言，我们的目标是：为给定的分布式系统自动生成一个容错控制器。容错性是指在某种故障假设下，无论系统出现何种故障，系统都能保持其功能的能力为了实现这一点，我们首先需要对我们的分布式系统进行建模，其次需要根据系统的事件和状态来正式地表达一些容错目标。我们建议设计人员的方法来建模系统和研究容错解决方案的存在性，根据几个故障假设和系统当找到解决方案时，它可以用作实现的指南（如果模型是抽象的[9]）或用于具有动态故障重构功能的部署（本文）。在我们的方法中，一个系统由一组任务组成，这些任务以一种配置放置在一组处理器上。一旦发生故障，一个或多个处理器变得不可用，任务必须重新放置在另一个配置中，通过重新启动它们到另一个处理器上，以便执行可以继续。系统的这些重新配置必须根据由任务管理器强制执行的容错策略来控制。后者具体体现在A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8183关于布局约束，终止的可达性，以及成本和质量的优化我们建议使用DCS技术自动生成任务管理器，应用于所有可能配置的系统模型该模型将由多个组件组成，每个组件都建模为标记的转换系统（LTS），并并行组成; DCS将在组件之上生成属性执行层[1]。我们工作的技术背景是反应系统设计的同步方法2[4]。这一选择的动机是现有的可用结果（语言，编译器，正式工具）和技术的语料库，已经产生了工业影响。我们的方法与同步模型兼容，这使得我们在LTS和组成中以及在已经存在的DCS中的一些选择成为可能[17]。1.3相关工作容错系统设计的形式化方法大多考虑了进程代数背景下的验证问题[21，6，5]。它们验证现有的手工设计（复制品交互控制、投票器等）满足与标称功能规范的某种等效性，即使在相比之下，DCS方法[12]自动合成一个控制器，通过构造来确保这一点。其原理是将故障视为不可控事件，而容错则是指无论发生什么故障，都存在能够实现功能的行为。不确定性下的规划是另一种现有的方法[12]，到目前为止，只证明了1-容错路径。我们将自己置于反应系统、有限状态机和使用精确最宽容控制器的合成此外，我们容忍几次失败，而不仅仅是一次。标记最终状态的可达性定义了实现功能的能力，并且可以用作解存在的标准[8];我们将其作为综合目标。其他将DCS应用于实时系统的工作存在[13]，考虑到时间方面，用于生成正确的应用程序特定的编译器，但它们没有特别考虑容错。此外，我们专注于布尔模型;定时或混合系统[2]中的综合将更强大，同时保留在可判定问题中，但效率成本非常高。在进程代数中存在与合成形式相比较的结果，但是这种比较超出了我们的范围。最后，在另一个并行工作中，我们使用DCS进行分布式控制器综合，这是一个手动实现的更困难的目标[9]，2 http://www.synalp.org84A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81而这里我们合成了一个中央控制器，但是是自动的。2背景2.1容错容错在文献中已经得到了广泛的研究：[14]给出了基本概念和术语的详尽列表，[20]给出了容错和实时系统的简短调查和分类，[11]详细讨论了分布式系统中容错的特殊情况。三个基本概念是故障、失效和错误：故障是发生在某些硬件或软件组件中的缺陷或错误;错误是故障的表现;失效是系统偏离所需的服务。一个子系统的故障可以被看作是全局系统的故障因此，存在以下因果关系：··· −→故障−a−ct−iv−at−io→n传播错误−→失败因果关系−→故障−→· · ·我们假设以下故障假设：只有处理器可以失败，与故障沉默模型。也就是说，一个处理器要么是活动的，工作正常，要么是故障的，不产生任何输出。为了容忍这样的故障，我们将利用分布式架构所提供的固有硬件冗余：即，我们不希望增加额外的处理器，而只希望使用现有的处理器。我们的目标是应用错误处理技术，这样，每当一个处理器将失败，在它的活动任务将动态重新启动其他一些非故障处理器。在这样的错误处理之后达到的系统的新状态在以下意义上被降级：现在可用的处理器更少，但是由于所有任务仍在执行，所以功能被保持。2.2离散控制器综合本节简要介绍DCS。当我们采用现有的框架时，我们不会重复工具的定义或技术细节，而只是总结功能。DCS出现在80它的目的是，给定两种语言P和D，得到第三种语言C，使得P <$C <$D。这是一种反演问题，因为人们想从D和P中找到C。在这里，P被称为被控对象，D是所需的系统或目标，C是控制器。最近，几个研究小组提出了扩展和应用这种语言理论技术的标记迁移系统（LTS）。形式上，LTSA. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8185目的系统是一个元组Q，q0，I，O，T，其中Q是状态的有限集合，q0是初始状态，I是输入信号的有限集合（由环境产生），O是输出信号的有限集合（发布到环境），T是转换关系，即，是Q×Bool（I）×O<$×Q的一个子集。每个转换都有一个标签形式g/a，其中g∈B ool（I）必须为真，才能进行跃迁（g是转换的保护），而a∈O是转换发生时发出的输出的合取（a是转换的动作）。在我们的方法中，P被指定为LTS，D是受控系统要满足的目标，通常使受控系统中的状态子集不变，或者保持它始终可达。用DCS获得的控制器C是限制P的转变的约束，即，禁止那些会危及目标的行为。关键点在于输入集合I被划分为两个子集Ic和Iu，分别是可控输入集合和不可控输入集合。DCS的原理是控制器C只能约束P的那些转变，对于这些转变，保护包含至少一个可控信号，即， 在IC。如图1所示，目标是表示在系统IuOIcFig. 1.从不受控系统（左）到闭环控制（右）。还可以考虑分配给P的状态和/或输入/输出的权重，并指定一定不能达到某个上限或下限。最优控制器合成[16]然后可以用于控制过渡，以便在一个步骤中（或在有界路径上）最小化/最大化某个函数w.r.t.这些权重;即，只进入下一个具有最佳权重的状态。可以有几个权重相等的解决方案，因此优化并不一定导致决定论。可以注意到，这只给了我们一步选择，即，局部最优，而不是全局最优。对于我们的问题，这样的权重可以模拟给定任务在给定处理器上的最坏情况执行时间（WCET），它的功耗，它需要的处理器负载量，或者在这个特定的处理器上执行时的结果质量。合成操作的顺序很重要：事实上，它们的顺序不是可交换的。可达性之前不能考虑IuO控制器Ic系统86A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81不变性约束，因为后者可能会通过删除路径和破坏可达性来损害前者。相反，在不变性之后考虑可达性不会危及不变性，因为它不会导致路径离开不变集。最优化应该被认为是最后的，作为正确的解决方案中的选择;即使在可达性之后，它也只会保留一些路径，这些路径应该总是满足它。合成的结果是一个约束，由于它是自动计算的，设计者不太容易读懂或“用脑”使用在第6节中提出了这种耦合的实现。2.3性能强化层我们的方法遵循一个框架，用于自动生成属性执行层，混合命令式/声明式风格，基于DCS [1]。一个系统被设计成一组局部组件，每个局部组件由描述其相关控制状态和转换以及局部约束w.r.t.环境或其他因素。特别是，它们具有输入功能，可以控制配置之间的选择这些LTS的同步涉及多个组件的全局约束表示为该产品的逻辑属性。在缺乏对这些全局约束的管理的情况下，它们是不满足的;换句话说，产品模拟了不受控制的全局系统的行为。我们使用一般DCS技术和工具，如上所述，为了自动计算和生成一个属性执行层，当与通信并行自动机的集合相结合时，将保证满足全局约束。该控制器将为组件的可控输入提供值，以便无论其他输入的值如何，其余行为都是正确的。这种方法的优点是双重的：一方面，属性强制层是正确的，因为它是精确计算的结果。另一方面，该过程的自动化性质使得设计易于修改，无论是在组件行为中还是在声明性属性中;因此，可以为所研究的给定系统实验各种全局约束，为设计空间探索提供有效支持。在本文中，这个一般框架被具体应用于容错。组件是任务和处理器，局部模型表示配置和故障。全局约束指定容错A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8187好的我fi错误i如执行一致性和功能性的维护，在不变性和可达性方面。合成控制器管理任务重新配置，以执行所需的容错策略。3分布式系统在本节中，我们将详细说明我们的抽象模型和失效假设。同时，我们牢记我们的目标，使这些抽象模型适合DCS。因此，我们考虑由以下组成的实时系统• 分布式异构体系结构，由一组故障静默处理器组成，通过点对点通信链路完全连接，• 一组周期性任务，可以在不同的处理器上运行，具有不同的特性（质量，功率或时间成本），• 调用任务的应用程序，其可以被简单地认为是任务管理层，或者被认为是在任务之间强制执行优先约束的调度器或这种系统的实时性来自周期性任务的时间成本每个任务的时间成本都是通过WCET分析来衡量的。然后，每个任务都是周期性的，我们认为，当在处理器上执行时，它使用一些CPU负载，通过将其WCET除以其周期来计算。因此，强制执行实时约束相当于为每个处理器分配一个CPU负载最大界限，该界限永远不会被超越。3.1体系结构模型3.1.1局部处理机模型每个处理器都由图2的LTS建模，其中OKi表示处理器i运行良好，而ERRi表示它已经崩溃。我们假设只有处理者会失败，并采用一个失败-沉默模型。最近对现代处理器的研究表明，可以以合理的成本实现故障静默行为[3]。故障也是随机的，因此处理器不能从ERR返回到OK状态。要对间歇性故障进行建模，我们只需要添加这样一个转换。处理器可以以分时的方式被任务使用图2：处理器模型。所以 的 几 任务 可以 被 活性对的相同处理器同时还研究与讨论与此相关，可以考虑任务之间的排除，禁止共享同一个处理器，因为使用了一些排他的88A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81resource.此外，与权重相关，特别是功率和负载成本，单个任务权重是可加的：在给定的处理器上，全局负载是所有活动任务的负载之和。每个处理器i都有一个量化的边界bi，它指定了它的最大功率容量。3.1.2异构体系结构模型处理器嵌入在一个完全连接的点对点通信链路网络中，如图3所示。 我们记S为所有这些处理器的集合。我们假设通信链路不会失败。一个处理器专用于执行控制器P0，而只有另一个处理器-Sor可用于执行系统每个处理器必须实时检测其他处理器 这可以很容易地实现，L1。2P1P2L1。3L2。3P3S={P1，P 2，P 3}图3：分布式体系结构。S中的处理器以周期性间隔向彼此发送该模型由上述所有LTS组成在这个例子中，我们有三个，每个处理器P1、P2和P3一个，其容量边界bi为：功耗分别为5、3和6。这种分布式架构是异构的，这意味着每个任务的WCET和功耗在每个处理器上都不相同。可能有些任务无法在某些处理器上运行，例如，因为它们需要特定的硬件设备（输入传感器，专用协处理器......）。3.1.3环境或故障模型我们现在需要对系统中可能发生的故障进行建模。例如，可能发生多少次故障？它们能同时发生吗？在图2的处理器模型中，问题是fi事件如何发生？似乎自然的是，所有的fi事件都是不可控的（即， ∈Iu），因为故障是本质上不可控的事件。但这将意味着对他们没有任何限制。特别地，所有事件fi都可能发生，这意味着所有处理器都可能发生故障。当然，这将导致系统的完全故障，根本不可能确保系统的容错性。没有人期望一个系统能容忍组成它的所有处理器的故障。因此，我们需要指定在我们考虑的模式中失败发生为了对此进行建模，我们选择使用LTS对环境进行建模。其目的是从环境产生的信号ei中发出信号fiA. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8189这些信号ei将是不可控的（即，∈Iu），反映了故障可能在任何时间发生的事实，而信号fi将是局部的，即，既不在Iu中也不在Ic中，并且将仅用于构建所有LTS的同步乘积F1e1e2e3/f1Be1e2e3/f3F2e1e2e3/f 2F3e2 e3/ f2F1e2e3/f3F1、2e1e2e3/f11 2F1， 3e ee1e3/f1第一季第二集第三集B三楼一层F3e1e2e1e2/f1e3/f3第一季第二集第第一季第二集第三集F3e1e3/f3F2、3E2E1/F2e2 e3/ f2F1F1、 2e1e3/f1第一季第二集第三集Be1e3/f1e1e3/f3第一季第二F2/F第一季第二集第三集F3e1e3/f3E2E1/F2F2、3（一）（b）第（1）款（c）第（1）款见图4。故障模式：（a）只有一个故障;（b）一个或两个;（c）故障模式。图4（a）的环境模型只允许系统中发生一个故障，而图4（b）的环境模型允许两个故障发生，可能是同时发生的（如果禁止同时发生故障，则可以删除从B到F1，2、F1，3和F2，3的三个转换）。无论是在这种情况下，B是初始状态，而状态Fi，j，k. 记录事件，而不是处理器Pi，Pj，Pk..作为变型，根据关于系统的可用知识，可以通过直接给出从输入信号ei产生局部信号fi的LTS来直接指定故障模式。这比指定可能发生故障的处理器数量更有表达力。例如，图4（c）对应于最多两个处理器可能发生故障的故障模式，除了处理器P1和P3不能一起发生故障提供这样一个组件模型取决于设计师。他的选择将取决于他对系统和相关故障预防的了解。例如，如果两个故障不太可能同时发生，他将从自动机4（a）中删除从B到Fi，j的三个转换。或者，如果他想考虑恶意攻击，他会保留它们。90A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81我我K我我3.2任务模型3.2.1基本控制结构模式每个任务j由图5的LTS正式建模，假设任务可以在所考虑的架构的三个处理器上执行。它具有初始空闲状态Ij、接收到请求信号rj后的就绪状态Rj、终止状态Tj和几个活动状态Aj，代表任务机密。一个处理器，一个处理器在系统中。这里，i表示任务j在哪个处理器上是活动的;由于我们的架构有三个处理器，每个任务LTS有三个活动状态。RJ图5：任务调用模型。按照惯例，下标/上标指的是处理器/任务。 该州在处理器i上周期性地执行j任务j，直到发生事件tj：这就是我们所说的周期性任务。这样的周期性任务可以直接和容易地由模式自动机建模[15]。隐含地，每个状态都有一个附加的自循环，标记有complement- mentguard w.r.t.所有其他的输出转换。例如，状态Ij具有标记为r j的自循环，其使得LTS能够保持在Ij内直到信号rj出现。从状态Aj状态Aj代表重新配置系统通过在处理器i上停止任务j并在处理器i上重新启动它K.我们称之为迁移。它们将被决定，以保持系统在全球配置中，使其继续提供其标称服务。 特别地，迁移可以被决定为对处理器故障的反应（在这种情况下，任务当然不需要停止）。但它也可以用来平衡几个活动处理器之间的负载，或者遵守处理器的能耗限制在控制器合成方面，信号rj和tj将是不可控的（即，∈ Iu），而信号aj将是可控的（即，∈Ic）.3.2.2数量特征一些有趣的特征可以建模为与状态相关的权重[18];我们只考虑从状态到整数的简单映射执行时间是每个任务所需的CPU负载，由WCET分析测量。由于任务是周期性执行的，因此我们假设，当任务从一个处理器迁移到另一个处理器时，它的执行会重新启动RJIjRJ一个j 1一个2一个j 3一个2一个J一个j 2一个j 1一个j 3一3J的1一个J一个1不JTJTJTJA. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8191我我我我F1e1 e2 e3/ f1Be1 e2 e3/ f3F2e1e2F3E3/ F2OK1f1错误1OK2f2错误2OK3f3错误3调度器R1I11升a121 升1 升的11t1R1a1a 12 3A1A122a13a13的13t1t1T1R1R2R3I2R2I3R3一个2一个2一个2一个3一个3一个3123123一个22一个2一个33一个3一个2一个2R2一个3一个3R3一个23一个2一个33一个3t2t2t3t3T2T3见图6。一个完整的系统，包含3个处理器和3个任务，以及一个控制器。从一开始就在新的处理器上。因此，它的新处理器必须完全接受任务相对于每个处理器给出任务j的功耗CjI.它与WCET有关，但不是线性的[7]。 对于我们的例子，表1中给出了Cj的值，以及每个边界bi，它是处理器i可接受的最大消耗。质量Qj相对于每个处理器i给出任务j的它可以账户，例如，对于根据特殊协处理器的存在通过数值计算、或者通过启发式搜索中变化深度的算法的不同版本、或者通过图像处理操作产生的结果的准确性。对于我们的例子，Qj的值在表1中给出。耗电量C质量Q处理器处理器P1P2P3P1P2P3任务T1442353T2T3222334222255边界b536表1任务T j在处理器P i上的消耗C j，质量Q j，有界b i。我我3.3应用模型应用程序是建立在一组任务的调用之上的，将其视为接收请求的服务器，或者包括调度程序或程序。92A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81我我JQ.IjT2T1T1T33.3.1任务服务器如果系统由n个任务组成，则并行地存在n个相应的LTS.它们在模式自动机[1，15]中的同步组合表示所有行为，即，所有可能的配置，以响应所有可能的请求序列和终止事件。本文考虑了数量特征的组成tobeadditi ve.它清除CPU负载或电源消耗处理器Pi，其中对于任务j：Ci=Cj。关于质量，我们认为总体质量是活动任务的手段，这可以理解为提交给会议的论文获得全球标记的方式我们将使用质量来选择向下一个状态的过渡，这是最高质量;因此，我们不需要进行数据存储，也不需要仅使用此总和对于处理器i和任务j：Q=j3.3.2搜索器程序调度程序或程序可以负责以给定的顺序发出任务请求。其目的是根据用户指定的优先级图来调度任务：它必须以正确的顺序发出信号rj，以便任务以满足优先级约束的方式准备就绪（处于Rj图7：优先约束。如果我们考虑图7的例子，调度器首先发出r1，然后在接收到t1之后，它发出r2和r3，因此并行执行T2和T3，最后，一旦它接收到t2和t3，它发出r1。3.4系统模型最后，通过组合前面介绍的不同局部模型来建立多处理器、多任务系统的模型：一个用于环境模型，一个用于每个处理器，一个用于每个任务，一个用于调度器，一个用于控制器。这在图6中针对由3个处理器和3个任务组成的完整系统进行了说明调度（决定任务执行的顺序）和分配（决定它们在哪里执行）在这里是解耦的：调度器根据优先级约束来调度任务，而控制器根据容错策略来动态分配任务A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8193我我我4属性、目标和容错容错策略由一组属性和目标声明性地指定。这些属性的容错特性是双重的。一方面，它们意味着在如上所述的模型上被考虑，其中所有故障、恢复或失败行为都被表示。另一方面，它们描述了失败的国家（例如，一致的放置约束表征系统不可行的状态）以及容差，这意味着无论故障如何都要填充功能的概念。4.1性能4.1.1确保一致的执行Property %1（故障处理器上没有活动任务）<$（AjErri）.J I当任务Tj在处理器P i上活动时，属性1是矛盾的（即，在状态Aj）中，而Pi在Erri中。综合的目的是使它不变地为真。如果系统，如设计者所建模的，是这样的，在每个状态中存在到安全状态的转换（即，其中性质1成立），则合成将成功，并且受控系统将总是能够通过移动到安全状态来对处理器故障作出反应。否则，综合将失败，这向设计者表明她/他的系统不能容错。属性2（活动任务在处理器容量范围内）其中，Ci≤ bi.当给定处理器上所有活动任务的累积成本超过其容量界限时，属性2同样，综合的目标是使它不变地为真。通常情况下，此目标可能会产生以下效果抑制从Rj到任何活跃状态Aj对于任务j，如果采取这种转换意味着在没有边界问题的情况下，将不能容忍在环境模型中指定的稍后的处理器故障。在这里，DCS计算最允许的控制器，以确保所有故障都被容忍，而没有边界问题。一个终止的任务可以释放另一个等待的任务。4.1.2保险功能前面的属性只是简单的状态属性，用于避免不一致的配置。离散控制器可以无限期地抑制94A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81如果存在唯一剩余的处理器对它的限制太低的可能性（在其他处理器失败之后），则开始任务。在这种情况下，没有确保功能的解决方案，这里定义为达到终止。换句话说，任务只有在“路径清晰且足够宽”时才会被激活属性3（功能已完成）从所有可达状态中，终端配置使得iT i是可达的。属性3指出，无论环境模型中指定的故障如何，以任何顺序和可能的并发性，对于任何传入任务请求和终止的发生和顺序，都可以达到终端配置。该属性有助于表征容错，因为它排除了所有活动都将冻结在等待状态的行为，以避免危及属性1和2。它可以用来检测那些没有能力（逻辑或定量）实际容忍故障，同时继续提供其标称功能的系统。它与以前的性质不同，因为它不仅考虑了当前状态，而且考虑了系统的轨迹，要求它们能够到达终点。4.2优化成本和质量这是一个采用策略的问题，通过仅切换到下一个配置，使得它们：• 当任务质量随处理器而变化时，最大化总体质量;• 最小化全局消耗，它可以定义为处理器上任务的成本之和。此外，具有这种质量的概念（在非活动状态为零，在活动状态为正）提供了一种向受控系统强加进展的方式，其中无休止地保持在等待状态的选项被移除;因此，推进到活动，并接近完成。另一种更独立的方法是对等待成本进行单独的加权，并将其最小化[1]。4.3讨论嵌入式系统的容错可以分为静态和动态两类。在静态方法中，添加了任务冗余，使得在执行期间可以容忍任何失败的发生;缺点是这是昂贵的，因为必须支付A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8195即使在没有故障的情况下也具有冗余性;优点是可以在系统部署之前计算系统反应时间的界限，并保证无论执行期间发生什么故障，该界限都将保持不变。在动态方法中，将机制添加到系统中，使得系统将能够动态地对执行期间的任何故障的发生做出反应;缺点是不能对系统的反应时间进行计算，因为这取决于不可预测的故障的发生;优点是在没有故障的情况下不必支付开销;也就是说，直到故障发生，容错系统的执行成本与相应的非容错系统的执行成本（几乎相同）。我们相信，我们的方法是有趣的，因为当DCS实际上成功地产生控制器时，我们获得了一个配备有动态重建机制来处理故障的系统（即，控制器），具有静态保证，即在执行期间将容忍所有指定的故障，并且具有系统反应时间的已知界限。换句话说，我们拥有这两种方法的优势。但请记住，只有当DCS成功时，这才是真的。如果它失败了，由于DCS工具探索了它的所有状态空间（象征性地），这意味着不存在可以容忍这些失败的解决方案，并且限制了处理器5说明性的解释5.1特性1：一致执行在我们的示例中，如图8所示，如果P2出现故障（事件e2，状态ERR2），则没有任务应该在其上活动（状态A1，A2和A3）。的2 2 2P1和P3也是如此。显然，对于所有处理器可能失败，没有控制器可以找到满足的目标：它不能启动一个任务，而不冒着所有处理器在其终止之前失败的风险，因此，行为将保持在所有请求的任务的就绪状态同样，具有放置约束的任务会使系统更难控制：实际上，一旦在处理器Pi上活动，就必须总是有另一个处理器能够在Pi故障的情况下托管它们。5.2性质2：有界容量为了举例，我们考虑一个全局配置，其中我们有T1到 P1（4≤5），T2到 P2（2≤3），T3到P3（4≤6）（因此不考虑图7的优先约束）。然后，如果P2崩溃，T2被迫迁移到P1或P3上. 但是没有一96A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81质量3+2+5=10功率4≤52≤34 ≤6{e2，a1，a2，a3}{e2，a1}{e2}{e2，a2}{e2，a2，a3}2+2+3=731123+2+5=103 113+2+5=102 + 2≤5 2 ≤ 64 ≤52 ≤34 ≤62≤5 2+4 ≤63+2+5=10不一致（错误2）1一个3一个2312 + 4> 5 4≤ 6不一致（b1）3+5+5=13的1一个331一个234≤ 5 3+ 4> 6不一致（b3）见图8。状态示例（仅显示配置）和转换控制。这两个选择满足处理器最大利用率界限的约束事实上，T1和T2在P1上的成本之和将是2+ 4> 5，而T2和T3在P3上的成本之和将是3+ 4> 6。因此，控制器强制更多的迁移，例如， T1到P3，T2到P1. 在P1（2 ≤ 5）和P3（2 + 4 ≤ 6）上都将满足对边界的时间约束。当其他处理器出现环境模型所述的故障后，剩余的具有最小容量的处理器仍然能够托管所有活动任务时，可以找到解决方案。这个约束也会阻塞处于就绪状态的系统，因为路径对于执行来说不够清晰和宽。这里，以及对于先前的目标，环境模型可以具有确定性：如果它排除了病理性故障模式，则可以找到解决方案。此外，一个任务模型不可能让控制等待在就绪状态，直到达到一个有利的配置，允许较少的解决方案。在这种情况下，拥有程序或调度程序可能会产生影响，因为只有某些任务子集可以并行激活这需要比任务服务器更少的处理器容量另一方面，对于具有等待状态的任务，实际排序在控制器的控制下，并且可以存在一个解决方案，该解决方案一个接一个地顺序进行任务。对于这样的任务，考虑一个程序或调度程序，因此是没有用的控制解决方案的搜索5.3属性3：功能性结果因环境模型而异：• 对于一个故障模型（图4-a），由于容量充足，因此一切工作正常的1一个2一个31231的1一个331的1一个2一个3123一个2一个331的13A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8197在任何两个剩余处理器的组上;• 对于两个故障模型（图4-b），P2的容量不足以容纳任务T1，因此，无论故障和请求的顺序如何，没有控制器能够确保功能性• 对于故障模式示例（图4-c），可以找到解决方案，因为不考虑病态处理器配置（仅P2幸存者）可以注意到，如果P2的容量界稍高一些，则两故障模型将存在一个解：改变界允许我们获得不同的可控性解。如果找不到解决方案，用户必须放松系统的一些约束：环境模型或功耗限制。. .当找到一个解决方案时，这意味着我们有一个控制器，它将动态地将任务分配到活动处理器上，同时保证所有处理器故障都是可以容忍的，并且累积功耗始终保持小于每个处理器上的界限。5.4优化这使我们能够进一步限制行为，使用表1中的值，以最大限度地提高质量（并可能强制迁移只是为了实现这一点），然后最小化功耗成本。如2.2节所述，可能有几个权重相等的解。图8中的示例显示了剩下的两个配置，质量为7（左）和10（右）对于所研究的同一系统，这些标准可以发挥作用：首先可以应用最小消耗，然后再最大限度地提高剩余解决方案的质量。6执行正如我们在开始时提到的，我们正在使用现有的同步和DCS技术，因此在这个有限的空间内，其他地方有详细信息MATOU3[15]用于编写模型，我们的系统是模式自动机的集合，而符号模型检查器和DCS工具SIGALI4[17]成功用于从高级规范自动合成容错系统，然后使用SIGALSIMU对系统和控制器进行联合仿真，如图9所示。3http：//www-veri ma g. 我妈。fr/~m ara ni n x/MA T4http://www.irisa.fr/vertecs/Logiciels/sigali.html98A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）81西加利模式自动机西加尔·西穆互动仿真系统模型组件z3z编码控制器性能权重见图9。 使用的工具我们首先考虑简单的任务和一致的执行目标，然后通过功能实现和优化扩展我们的目标。我们的方法受到现有DCS工具的技术状态的限制，基本上与模型检查工具相同的限制。鉴于目前在这一领域的趋势（符号状态空间探索，抽象解释，扩大运营商…），我们相信区域供冷系统日后的改善工具将使其成为工业规模问题的有效解决方案。7结论我们已经展示了如何对实时分布式系统、其异构体系结构及其环境进行建模，以便自动生成执行容错的控制器。它通过根据容错策略迁移任务来对故障的发生做出反应。为此，我们将DCS应用于整个系统的LTS模型，目标是一致执行，功能实现和优化。从容错的角度来看，我们的方法是有趣的，在这个意义上，当DCS实际上成功地产生一个控制器，我们得到一个系统配备了一个动态reconfiguring机制来处理故障，与静态保证，所有指定的故障将被容忍在执行过程中，并与一个已知的约束系统有趣的观点涉及：• -任务模型 的变体，例如具有几种模式以考虑动态电压缩放（DVS），其中较慢的速度在功率方面更便宜，或者具有用于相同功能的降级模式• 其他感兴趣的逻辑属性是任务之间的排除和使用观察器的排序约束;其他感兴趣的定量属性是设备（传感器、协处理器）的使用、管理存储器使用、迁移成本的界限、最低质量水平等。• 控制，以优化转换成本，例如对迁移任务的成本进行建模，或在重要状态集之间的路径上累积，如开始和结束状态，• 同一个系统有时可以在不同的环境中重复使用：A. Girault，E.Rutten/Electronic Notes in Theoretical Computer Science 133（2005）8199例如，片上系统中的图像处理编码器/解码器子系统可以嵌入到不同的设备中，例如，家用DVD播放器，电源根本不是问题，或者手机或摄像机，电源确实是至关重要的;在基于平台的设计的框架中，重新使用提交给不同综合目标的相同模型打开了这些技术的进一步应用的前景。引用[1] K. Altisen，A. Clodic，F. Maraninchi和E. 拉顿 使用合成技术来构建属性执行层。《欧洲方案规划研讨会论文集》'03，波兰华沙，2003年4月[2] R.阿尔布尔岛O. Bournez，T.天啊，奥。Maler，和A.普努埃利线性系统切换控制器之有效综合。Proc. of the IEEE，88：1011[3] M. Baleani，A.费拉里湖Mangeruca，M. Peri，S. Pezzini和A.桑吉瓦尼-文森泰利用于汽车安全关键应用的容错平台。 2003年11月在美国圣何塞举行的嵌入式系统的架构、集成和集成国际会议上ACM。[4] A. Benveniste，P. Caspi，S.A. Edwards，N. Halbwachs，P. Le Guernic，and R.德·西蒙尼。十二年后的同步语言。Proc. of the IEEE，91（1）：64-83，January 2003. 嵌入式系统的特殊问题。[5] C. Bernardeschi，A. Fantechi和L.西蒙奇尼正式验证容错系统设计。计算机杂志，43（3），2000年。[6] G.布伦斯和我。萨瑟兰模型检查和容错。第六届国际代数学方法和软件技术会议论文集，AMAST'9 7 ， 悉尼 ， 澳 大利 亚， 19 9 7 年。[7] A.P. Chandrakasan，S. Sheng和R.W. Broderson低功耗CMOS数字设计。IEEE Journal ofSolid-State Circuits，27（4）：473[8] K.- H.周和J T.林自动化制造系统容错监控器之综合：以光印制程为例。IEEE Trans. onRobotics and Automation，14（2）：348[9] E. Dumit