Automating the addition of fault tolerance with discrete controller synthesis
Automating the addition of fault tolerance with discrete controller synthesis
复制标题
通过离散控制器综合自动添加容错功能
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
É. Rutten
中科院分区：
文献类型：
--
作者：
A. Girault;É. Rutten
离散控制器合成（DCS）是一种形式的方法，基于与模型检查相同的状态空间探索算法。它的兴趣在于能够通过指定先验的构造形式属性来获得满足的自动系统。在本文中，我们的目的是证明这种方法具有容错的可行性。我们从故障不耐受程序开始，该程序以有限标记的过渡系统的同步并行组成模型。我们正式指定错误假设；我们陈述一些容错要求；而且，我们使用DC自动获得一个程序，在没有故障的情况下具有与初始故障不耐受性相同的行为，并且在故障假设下满足了错误公差要求。我们的最初贡献在于证明DC可以优雅地用于设计可容忍系统的演示，并保证获得所获得系统的关键特性，例如容错水平，定量约束的满意度等等。我们展示了从案例研究中提到的许多示例，我们的方法可以解决不同类型的故障（崩溃，价值或拜占庭），并影响各种硬件组件（处理器，通信链接，执行器或传感器）。此外，我们表明我们的方法还提供了一个最佳标准，可用于合成符合嵌入式系统（如功耗）限制的容错系统。
Discrete controller synthesis (DCS) is a formal approach, based on the same state-space exploration algorithms as model-checking. Its interest lies in the ability to obtain automatically systems satisfying by construction formal properties specified a priori. In this paper, our aim is to demonstrate the feasibility of this approach for fault tolerance. We start with a fault intolerant program, modeled as the synchronous parallel composition of finite labeled transition systems; we specify formally a fault hypothesis; we state some fault tolerance requirements; and we use DCS to obtain automatically a program, having the same behavior as the initial fault intolerant one in the absence of faults, and satisfying the fault tolerance requirements under the fault hypothesis. Our original contribution resides in the demonstration that DCS can be elegantly used to design fault tolerant systems, with guarantees on key properties of the obtained system, such as the fault tolerance level, the satisfaction of quantitative constraints, and so on. We show with numerous examples taken from case studies that our method can address different kinds of failures (crash, value, or Byzantine) affecting different kinds of hardware components (processors, communication links, actuators, or sensors). Besides, we show that our method also offers an optimality criterion very useful to synthesize fault tolerant systems compliant to the constraints of embedded systems, like power consumption.